diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean
index e3c70c0706..186ac75972 100644
--- a/doc/examples/bintree.lean
+++ b/doc/examples/bintree.lean
@@ -282,7 +282,7 @@ theorem BinTree.find_insert_of_ne (b : BinTree β) (ne : k ≠ k') (v : β)
   let ⟨t, h⟩ := b; simp
   induction t with simp
   | leaf =>
-    intros le
+    intro le
     exact Nat.lt_of_le_of_ne le ne
   | node left key value right ihl ihr =>
     let .node hl hr bl br := h
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index ad615d0ad2..a412ac8ca0 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -312,7 +312,7 @@ theorem eq_push_pop_back!_of_size_ne_zero [Inhabited α] {xs : Array α} (h : xs
     xs = xs.pop.push xs.back! := by
   apply ext
   · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
-  · intros i h h'
+  · intro i h h'
     if hlt : i < xs.pop.size then
       rw [getElem_push_lt (h:=hlt), getElem_pop]
     else
@@ -2955,7 +2955,7 @@ theorem getElem?_extract {xs : Array α} {start stop : Nat} :
   apply List.ext_getElem
   · simp only [length_toList, size_extract, List.length_take, List.length_drop]
     omega
-  · intros n h₁ h₂
+  · intro n h₁ h₂
     simp
 
 @[simp] theorem extract_size {xs : Array α} : xs.extract 0 xs.size = xs := by
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index d9128c7461..a1b4d8a103 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -338,11 +338,11 @@ theorem add_eq_or_of_and_eq_zero {w : Nat} (x y : BitVec w)
   · rfl
   · simp only [adcb, atLeastTwo, Bool.and_false, Bool.or_false, bne_false,
     Prod.mk.injEq, and_eq_false_imp]
-    intros i
+    intro i
     replace h : (x &&& y).getLsbD i = (0#w).getLsbD i := by rw [h]
     simp only [getLsbD_and, getLsbD_zero, and_eq_false_imp] at h
     constructor
-    · intros hx
+    · intro hx
       simp_all
     · by_cases hx : x.getLsbD i <;> simp_all
 
@@ -1666,7 +1666,7 @@ private theorem neg_udiv_eq_intMin_iff_eq_intMin_eq_one_of_msb_eq_true
     {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = false) :
     -x / y = intMin w ↔ (x = intMin w ∧ y = 1#w) := by
   constructor
-  · intros h
+  · intro h
     rcases w with _ | w; decide +revert
     have : (-x / y).msb = true := by simp [h, msb_intMin]
     rw [msb_udiv] at this
@@ -1742,7 +1742,7 @@ theorem msb_sdiv_eq_decide {x y : BitVec w} :
         Bool.and_self, ne_zero_of_msb_true, decide_false, Bool.and_true, Bool.true_and, Bool.not_true,
         Bool.false_and, Bool.or_false, bool_to_prop]
       have : x / -y ≠ intMin (w + 1) := by
-        intros h
+        intro h
         have : (x / -y).msb = (intMin (w + 1)).msb := by simp only [h]
         simp only [msb_udiv, msb_intMin, show 0 < w + 1 by omega, decide_true, and_eq_true, beq_iff_eq] at this
         obtain ⟨hcontra, _⟩ := this
@@ -1871,7 +1871,7 @@ theorem toInt_dvd_toInt_iff {x y : BitVec w} :
     y.toInt ∣ x.toInt ↔ (if x.msb then -x else x) % (if y.msb then -y else y) = 0#w := by
   constructor
   <;> by_cases hxmsb : x.msb <;> by_cases hymsb: y.msb
-  <;> intros h
+  <;> intro h
   <;> simp only [hxmsb, hymsb, reduceIte, false_eq_true, toNat_eq, toNat_umod, toNat_ofNat,
         zero_mod, toInt_eq_neg_toNat_neg_of_msb_true, Int.dvd_neg, Int.neg_dvd,
         toInt_eq_toNat_of_msb] at h
@@ -2141,7 +2141,7 @@ theorem add_shiftLeft_eq_or_shiftLeft {x y : BitVec w} :
   ext i hi
   simp only [shiftLeft_eq', getElem_and, getElem_shiftLeft, getElem_zero, and_eq_false_imp,
     not_eq_eq_eq_not, Bool.not_true, decide_eq_false_iff_not, Nat.not_lt]
-  intros hxi hxval
+  intro hxi hxval
   have : 2^i ≤ x.toNat := two_pow_le_toNat_of_getElem_eq_true hi hxi
   have : i < 2^i := by exact Nat.lt_two_pow_self
   omega
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 5d1b5268db..d0b75e50d9 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -241,11 +241,11 @@ theorem eq_of_getLsbD_eq_iff {w : Nat} {x y : BitVec w} :
     x = y ↔ ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i := by
   have iff := @BitVec.eq_of_getElem_eq_iff w x y
   constructor
-  · intros heq i lt
+  · intro heq i lt
     have hext := iff.mp heq i lt
     simp only [← getLsbD_eq_getElem] at hext
     exact hext
-  · intros heq
+  · intro heq
     exact iff.mpr heq
 
 theorem eq_of_getMsbD_eq {x y : BitVec w}
@@ -821,14 +821,14 @@ its most significant bit is true.
 theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by
   have := toInt_eq_msb_cond x
   constructor
-  · intros h
+  · intro h
     apply Classical.byContradiction
-    intros hmsb
+    intro hmsb
     simp only [Bool.not_eq_true] at hmsb
     simp only [hmsb, Bool.false_eq_true, ↓reduceIte] at this
     simp only [BitVec.slt, toInt_zero, decide_eq_true_eq] at h
     omega /- Can't have `x.toInt` which is equal to `x.toNat` be strictly less than zero -/
-  · intros h
+  · intro h
     simp only [h, ↓reduceIte] at this
     simp only [BitVec.slt, this, toInt_zero, decide_eq_true_eq]
     omega
@@ -2097,7 +2097,7 @@ theorem toInt_ushiftRight_of_lt {x : BitVec w} {n : Nat} (hn : 0 < n) :
     (x >>> n).toInt = x.toNat >>> n := by
   rw [toInt_eq_toNat_cond]
   simp only [toNat_ushiftRight, ite_eq_left_iff, Nat.not_lt]
-  intros h
+  intro h
   by_cases hn : n ≤ w
   · have h1 := Nat.mul_lt_mul_of_pos_left (toNat_ushiftRight_lt x n hn) Nat.two_pos
     simp only [toNat_ushiftRight, Nat.zero_lt_succ, Nat.mul_lt_mul_left] at h1
@@ -2235,7 +2235,7 @@ theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) :
       omega
     · simp only [hi, decide_false, Bool.not_false, Bool.true_and, Bool.eq_and_self,
         decide_eq_true_eq]
-      intros hlsb
+      intro hlsb
       apply BitVec.lt_of_getLsbD hlsb
   · by_cases hi : i ≥ w
     · simp [hi]
@@ -2289,7 +2289,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
   · simp [hw₀]
   · simp only [show ¬(w ≤ w - 1) by omega, decide_false, Bool.not_false, Bool.true_and,
       ite_eq_right_iff]
-    intros h
+    intro h
     simp [show n = 0 by omega]
 
 @[simp] theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x := by
@@ -2777,7 +2777,7 @@ theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ 0#m).toInt = (2 ^ m) * x.toInt := by
   simp only [toInt_append, beq_iff_eq, toInt_zero, toNat_ofNat, Nat.zero_mod, Int.cast_ofNat_Int, Int.add_zero,
     ite_eq_right_iff]
-  intros h
+  intro h
   subst h
   simp [BitVec.eq_nil x]
 
@@ -2961,7 +2961,7 @@ theorem extractLsb'_append_extractLsb'_eq_extractLsb' {x : BitVec w} (h : start
   ext i h
   simp only [getElem_append, getElem_extractLsb', dite_eq_ite, getElem_cast, ite_eq_left_iff,
     Nat.not_lt]
-  intros hi
+  intro hi
   congr 1
   omega
 
@@ -2988,7 +2988,7 @@ theorem signExtend_eq_append_extractLsb' {w v : Nat} {x : BitVec w} :
   · simp only [hx, signExtend_eq_setWidth_of_msb_false, getElem_setWidth, Bool.false_eq_true,
       ↓reduceIte, getElem_append, getElem_extractLsb', Nat.zero_add, getElem_zero, dite_eq_ite,
       Bool.if_false_right, Bool.eq_and_self, decide_eq_true_eq]
-    intros hi
+    intro hi
     have hw : i < w := lt_of_getLsbD hi
     omega
   · simp [signExtend_eq_not_setWidth_not_of_msb_true hx, getElem_append, Nat.lt_min, hi]
@@ -3036,7 +3036,7 @@ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start
     · simp only [hlen, ↓reduceDIte]
       ext i hi
       simp only [getElem_extractLsb', getLsbD_append, ite_eq_left_iff, Nat.not_lt]
-      intros hcontra
+      intro hcontra
       omega
     · simp only [hlen, ↓reduceDIte]
       ext i hi
@@ -3483,7 +3483,7 @@ theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
     have := two_mul_toInt_lt (x := y)
     simp only [Nat.add_one_sub_one]
     constructor
-    · intros h
+    · intro h
       rw_mod_cast [← Int.add_bmod_right, Int.bmod_eq_of_le]
       <;> omega
     · have := Int.bmod_neg_iff (x := x.toInt - y.toInt) (m := 2 ^ (w + 1))
@@ -3499,7 +3499,7 @@ theorem twoPow_le_toInt_sub_toInt_iff {x y : BitVec w} :
     have := le_two_mul_toInt (x := y); have := two_mul_toInt_lt (x := y)
     simp only [Nat.add_one_sub_one]
     constructor
-    · intros h
+    · intro h
       simp only [show 0 ≤ x.toInt by omega, show y.toInt < 0 by omega, _root_.true_and]
       rw_mod_cast [← Int.sub_bmod_right, Int.bmod_eq_of_le (by omega) (by omega)]
       omega
diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean
index c78ffe56ca..0843fc2cc0 100644
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -361,10 +361,10 @@ theorem negSucc_coe' (n : Nat) : -[n+1] = -↑n - 1 := by
 
 protected theorem subNatNat_eq_coe {m n : Nat} : subNatNat m n = ↑m - ↑n := by
   apply subNatNat_elim m n fun m n i => i = m - n
-  · intros i n
+  · intro i n
     rw [Int.natCast_add, Int.sub_eq_add_neg, Int.add_assoc, Int.add_left_comm,
       Int.add_right_neg, Int.add_zero]
-  · intros i n
+  · intro i n
     simp only [negSucc_eq, natCast_add, ofNat_one, Int.sub_eq_add_neg, Int.neg_add, ← Int.add_assoc]
     rw [Int.add_neg_eq_sub (a := n), ← ofNat_sub, Nat.sub_self, ofNat_zero, Int.zero_add]
     apply Nat.le_refl
diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 07b9e8ceb2..15f2a56c1f 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -1280,7 +1280,7 @@ noncomputable def diseq_eq_subst_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p
 theorem eq_diseq_subst (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
     : diseq_eq_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≠ 0 → p₃.denote' ctx ≠ 0 := by
   simp [diseq_eq_subst_cert]
-  intros _ _; subst p₃
+  intro _ _; subst p₃
   intro h₁ h₂
   simp [*]
 
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index 4b1ce1edf4..567c5ed82b 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -123,7 +123,7 @@ theorem attachWith_congr {l₁ l₂ : List α} (w : l₁ = l₂) {P : α → Pro
       ⟨x, mem_cons_self⟩ :: xs.attach.map fun ⟨y, h⟩ => ⟨y, mem_cons_of_mem x h⟩ := by
   simp only [attach, attachWith, pmap, map_pmap, cons.injEq, true_and]
   apply pmap_congr_left
-  intros a _ m' _
+  intro a _ m' _
   rfl
 
 @[simp, grind =]
diff --git a/src/Init/Data/List/Erase.lean b/src/Init/Data/List/Erase.lean
index 751ee00d77..79446b4b03 100644
--- a/src/Init/Data/List/Erase.lean
+++ b/src/Init/Data/List/Erase.lean
@@ -427,7 +427,7 @@ theorem erase_append_left [LawfulBEq α] {l₁ : List α} (l₂) (h : a ∈ l₁
 theorem erase_append_right [LawfulBEq α] {a : α} {l₁ : List α} (l₂ : List α) (h : a ∉ l₁) :
     (l₁ ++ l₂).erase a = (l₁ ++ l₂.erase a) := by
   rw [erase_eq_eraseP, erase_eq_eraseP, eraseP_append_right]
-  intros b h' h''; rw [eq_of_beq h''] at h; exact h h'
+  intro b h' h''; rw [eq_of_beq h''] at h; exact h h'
 
 @[grind =]
 theorem erase_append [LawfulBEq α] {a : α} {l₁ l₂ : List α} :
diff --git a/src/Init/Data/List/Nat/Pairwise.lean b/src/Init/Data/List/Nat/Pairwise.lean
index a8fd296cf6..5f14ffb088 100644
--- a/src/Init/Data/List/Nat/Pairwise.lean
+++ b/src/Init/Data/List/Nat/Pairwise.lean
@@ -61,10 +61,10 @@ theorem pairwise_iff_getElem {l : List α} : Pairwise R l ↔
     ∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j), R l[i] l[j] := by
   rw [pairwise_iff_forall_sublist]
   constructor <;> intro h
-  · intros i j hi hj h'
+  · intro i j hi hj h'
     apply h
     simpa [h'] using map_getElem_sublist (is := [⟨i, hi⟩, ⟨j, hj⟩])
-  · intros a b h'
+  · intro a b h'
     have ⟨is, h', hij⟩ := sublist_eq_map_getElem h'
     rcases is with ⟨⟩ | ⟨a', ⟨⟩ | ⟨b', ⟨⟩⟩⟩ <;> simp at h'
     rcases h' with ⟨rfl, rfl⟩
diff --git a/src/Init/Data/List/Nat/Range.lean b/src/Init/Data/List/Nat/Range.lean
index 6083dfa87d..e506911d4b 100644
--- a/src/Init/Data/List/Nat/Range.lean
+++ b/src/Init/Data/List/Nat/Range.lean
@@ -58,7 +58,7 @@ theorem pairwise_lt_range' {s n} (step := 1) (pos : 0 < step := by simp) :
   | s, n + 1, step, pos => by
     simp only [range'_succ, pairwise_cons]
     constructor
-    · intros n m
+    · intro n m
       rw [mem_range'] at m
       omega
     · exact pairwise_lt_range' (s := s + step) step pos
@@ -70,7 +70,7 @@ theorem pairwise_le_range' {s n} (step := 1) :
   | s, n + 1, step => by
     simp only [range'_succ, pairwise_cons]
     constructor
-    · intros n m
+    · intro n m
       rw [mem_range'] at m
       omega
     · exact pairwise_le_range' (s := s + step) step
diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean
index 9e3e5f5d95..05f1f4e154 100644
--- a/src/Init/Data/List/Sort/Lemmas.lean
+++ b/src/Init/Data/List/Sort/Lemmas.lean
@@ -352,7 +352,7 @@ where go : ∀ (i : Nat) (l : List α),
     rw [merge_stable]
     · rw [go, go]
     · simp only [mem_mergeSort, Prod.forall]
-      intros j x k y mx my
+      intro j x k y mx my
       have := mem_zipIdx mx
       have := mem_zipIdx my
       simp_all
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index 52c44644ae..3a3b7519bd 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -1164,7 +1164,7 @@ protected theorem pow_le_pow_iff_right {a n m : Nat} (h : 1 < a) :
     a ^ n ≤ a ^ m ↔ n ≤ m := by
   constructor
   · apply Decidable.by_contra
-    intros w
+    intro w
     simp at w
     apply Nat.lt_irrefl (a ^ n)
     exact Nat.lt_of_le_of_lt w.1 (Nat.pow_lt_pow_of_lt h w.2)
@@ -1177,7 +1177,7 @@ protected theorem pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) :
     a ^ n < a ^ m ↔ n < m := by
   constructor
   · apply Decidable.by_contra
-    intros w
+    intro w
     simp at w
     apply Nat.lt_irrefl (a ^ n)
     exact Nat.lt_of_lt_of_le w.1 (Nat.pow_le_pow_of_le h w.2)
diff --git a/src/Init/Grind/Ring/OfSemiring.lean b/src/Init/Grind/Ring/OfSemiring.lean
index 87212be4f0..e797e38765 100644
--- a/src/Init/Grind/Ring/OfSemiring.lean
+++ b/src/Init/Grind/Ring/OfSemiring.lean
@@ -205,7 +205,7 @@ theorem Poly.denoteS_combine {α} [CommSemiring α] (ctx : Context α) (p₁ p
   unfold combine; generalize hugeFuel = fuel
   fun_induction combine.go
   case case1 => intros; apply denoteS_concat <;> assumption
-  case case2 => intros h₁ h₂; cases h₁; cases h₂; simp [denoteS, Int.toNat_add, natCast_add, *]
+  case case2 => intro h₁ h₂; cases h₁; cases h₂; simp [denoteS, Int.toNat_add, natCast_add, *]
   case case3 => intro h₁ h₂; cases h₁; simp [denoteS, denoteS_addConst, add_comm, *]
   case case4 => intro h₁ h₂; cases h₂; simp [denoteS, denoteS_addConst, *]
   case case5 k₁ _ _ k₂ _ _ hg _ h ih =>
diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean
index 031add5239..4ef3dbbfcc 100644
--- a/src/Init/Internal/Order/Basic.lean
+++ b/src/Init/Internal/Order/Basic.lean
@@ -356,7 +356,7 @@ inductive iterates (f : α → α) : α → Prop where
   | sup {c : α → Prop} (hc : chain c) (hi : ∀ x, c x → iterates f x) : iterates f (csup c)
 
 theorem chain_iterates {f : α → α} (hf : monotone f) : chain (iterates f) := by
-  intros x y hx hy
+  intro x y hx hy
   induction hx generalizing y
   case step x hx ih =>
     induction hy
@@ -921,7 +921,7 @@ instance ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseIm
       exact l
       exact cy
     case mpr =>
-      intros h y cy ccy
+      intro h y cy ccy
       apply h
       exact ccy
       exact y
diff --git a/src/Init/Internal/Order/Lemmas.lean b/src/Init/Internal/Order/Lemmas.lean
index 9b1b6cb3bf..d82c12a482 100644
--- a/src/Init/Internal/Order/Lemmas.lean
+++ b/src/Init/Internal/Order/Lemmas.lean
@@ -453,7 +453,7 @@ theorem monotone_foldrM
 theorem monotone_mapM (xs : Array α) (f : γ → α → m β) (hmono : monotone f) :
     monotone (fun x => xs.mapM (f x)) := by
   suffices ∀ i r, monotone (fun x => Array.mapM.map (f x) xs i r) by apply this
-  intros i r
+  intro i r
   induction i, r using Array.mapM.map.induct xs
   case case1 ih =>
     unfold Array.mapM.map
@@ -473,7 +473,7 @@ theorem monotone_mapM (xs : Array α) (f : γ → α → m β) (hmono : monotone
 theorem monotone_mapFinIdxM (xs : Array α) (f : γ → (i : Nat) → α → i < xs.size → m β)
     (hmono : monotone f) : monotone (fun x => xs.mapFinIdxM (f x)) := by
   suffices ∀ i j (h : i + j = xs.size) r, monotone (fun x => Array.mapFinIdxM.map xs (f x) i j h r) by apply this
-  intros i j h r
+  intro i j h r
   induction i, j, h, r using Array.mapFinIdxM.map.induct xs
   case case1 =>
     apply monotone_const
@@ -597,7 +597,7 @@ theorem monotone_findSomeRevM?
     monotone (fun x => xs.findSomeRevM? (f x)) := by
   unfold Array.findSomeRevM?
   suffices ∀ i (h : i ≤ xs.size), monotone (fun x => Array.findSomeRevM?.find (f x) xs i h) by apply this
-  intros i h
+  intro i h
   induction i, h using Array.findSomeRevM?.find.induct with
   | case1 =>
     unfold Array.findSomeRevM?.find
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index b4c747f810..7c463e9dfa 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -53,55 +53,28 @@ be a `let` or function type.
 syntax (name := intro) "intro" notFollowedBy("|") (ppSpace colGt term:max)* : tactic
 
 /--
-Introduces zero or more hypotheses, optionally naming them.
+`intros` repeatedly applies `intro` to introduce zero or more hypotheses
+until the goal is no longer a *binding expression*
+(i.e., a universal quantifier, function type, implication, or `have`/`let`),
+without performing any definitional reductions (no unfolding, beta, eta, etc.).
+The introduced hypotheses receive inaccessible (hygienic) names.
 
-- `intros` is equivalent to repeatedly applying `intro`
-  until the goal is not an obvious candidate for `intro`, which is to say
-  that so long as the goal is a `let` or a pi type (e.g. an implication, function, or universal quantifier),
-  the `intros` tactic will introduce an anonymous hypothesis.
-  This tactic does not unfold definitions.
+`intros x y z` is equivalent to `intro x y z` and exists only for historical reasons.
+The `intro` tactic should be preferred in this case.
 
-- `intros x y ...` is equivalent to `intro x y ...`,
-  introducing hypotheses for each supplied argument and unfolding definitions as necessary.
-  Each argument can be either an identifier or a `_`.
-  An identifier indicates a name to use for the corresponding introduced hypothesis,
-  and a `_` indicates that the hypotheses should be introduced anonymously.
+## Properties and relations
+
+- `intros` succeeds even when it introduces no hypotheses.
+
+- `repeat intro` is like `intros`, but it performs definitional reductions
+  to expose binders, and as such it may introduce more hypotheses than `intros`.
+
+- `intros` is equivalent to `intro _ _ … _`,
+  with the fewest trailing `_` placeholders needed so that the goal is no longer a binding expression.
+  The trailing introductions do not perform any definitional reductions.
 
 ## Examples
 
-Basic properties:
-```lean
-def AllEven (f : Nat → Nat) := ∀ n, f n % 2 = 0
-
--- Introduces the two obvious hypotheses automatically
-example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by
-  intros
-  /- Tactic state
-     f✝ : Nat → Nat
-     a✝ : AllEven f✝
-     ⊢ AllEven fun k => f✝ (k + 1) -/
-  sorry
-
--- Introduces exactly two hypotheses, naming only the first
-example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by
-  intros g _
-  /- Tactic state
-     g : Nat → Nat
-     a✝ : AllEven g
-     ⊢ AllEven fun k => g (k + 1) -/
-  sorry
-
--- Introduces exactly three hypotheses, which requires unfolding `AllEven`
-example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by
-  intros f h n
-  /- Tactic state
-     f : Nat → Nat
-     h : AllEven f
-     n : Nat
-     ⊢ (fun k => f (k + 1)) n % 2 = 0 -/
-  apply h
-```
-
 Implications:
 ```lean
 example (p q : Prop) : p → q → p := by
@@ -113,7 +86,7 @@ example (p q : Prop) : p → q → p := by
   assumption
 ```
 
-Let bindings:
+Let-bindings:
 ```lean
 example : let n := 1; let k := 2; n + k = 3 := by
   intros
@@ -122,6 +95,19 @@ example : let n := 1; let k := 2; n + k = 3 := by
      ⊢ n✝ + k✝ = 3 -/
   rfl
 ```
+
+Does not unfold definitions:
+```lean
+def AllEven (f : Nat → Nat) := ∀ n, f n % 2 = 0
+
+example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by
+  intros
+  /- Tactic state
+     f✝ : Nat → Nat
+     a✝ : AllEven f✝
+     ⊢ AllEven fun k => f✝ (k + 1) -/
+  sorry
+```
 -/
 syntax (name := intros) "intros" (ppSpace colGt (ident <|> hole))* : tactic
 
diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
index 41520c66de..ae2ffdf859 100644
--- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
@@ -163,7 +163,7 @@ theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} {l : AssocLis
   suffices ∀ l l', Perm (filterMap.go f l l').toList
       (l.toList ++ l'.toList.filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) by
     simpa using this .nil l
-  intros l l'
+  intro l l'
   induction l' generalizing l
   · simp [filterMap.go]
   next k v t ih =>
@@ -181,7 +181,7 @@ theorem toList_map {f : (a : α) → β a → γ a} {l : AssocList α β} :
   suffices ∀ l l', Perm (map.go f l l').toList
       (l.toList ++ l'.toList.map fun p => ⟨p.1, f p.1 p.2⟩) by
     simpa using this .nil l
-  intros l l'
+  intro l l'
   induction l' generalizing l
   · simp [map.go]
   next k v t ih =>
@@ -195,7 +195,7 @@ theorem toList_filter {f : (a : α) → β a → Bool} {l : AssocList α β} :
   suffices ∀ l l', Perm (filter.go f l l').toList
       (l.toList ++ l'.toList.filter fun p => f p.1 p.2) by
     simpa using this .nil l
-  intros l l'
+  intro l l'
   induction l' generalizing l
   · simp [filter.go]
   next k v t ih =>
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
index fc215f16b1..0a541a1bee 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
@@ -66,13 +66,13 @@ protected theorem Liff.refl {α : Type u} {σ : Type v} [Entails α σ] (f : σ)
 protected theorem Liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [Entails α σ1] [Entails α σ2]
     (f1 : σ1) (f2 : σ2) :
     Liff α f1 f2 → Liff α f2 f1 := by
-  intros h p
+  intro h p
   rw [h p]
 
 protected theorem Liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [Entails α σ1]
     [Entails α σ2] [Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) :
     Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3 := by
-  intros f1_eq_f2 f2_eq_f3 a
+  intro f1_eq_f2 f2_eq_f3 a
   rw [f1_eq_f2 a, f2_eq_f3 a]
 
 protected theorem Limplies.refl {α : Type u} {σ : Type v} [Entails α σ] (f : σ) : Limplies α f f :=
@@ -81,7 +81,7 @@ protected theorem Limplies.refl {α : Type u} {σ : Type v} [Entails α σ] (f :
 protected theorem Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x}
     [Entails α σ1] [Entails α σ2] [Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) :
     Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3 := by
-  intros f1_implies_f2 f2_implies_f3 a a_entails_f1
+  intro f1_implies_f2 f2_implies_f3 a a_entails_f1
   exact f2_implies_f3 a <| f1_implies_f2 a a_entails_f1
 
 theorem liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1]
@@ -98,7 +98,7 @@ theorem liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1]
 theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2]
     (f1 : σ1) (f2 : σ2) (h : Limplies α f2 f1) :
     Unsatisfiable α f1 → Unsatisfiable α f2 := by
-  intros f1_unsat a a_entails_f2
+  intro f1_unsat a a_entails_f2
   exact f1_unsat a <| h a a_entails_f2
 
 theorem incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2]
diff --git a/tests/lean/1079.lean b/tests/lean/1079.lean
index 6458a07d8b..0e58e0eabd 100644
--- a/tests/lean/1079.lean
+++ b/tests/lean/1079.lean
@@ -1,12 +1,12 @@
 theorem bad : ∀ (m n : Nat), (if m = n then Ordering.eq else Ordering.gt) = Ordering.lt → False := by
-  intros m n
+  intro m n
   cases (Nat.decEq m n) with -- an error as expected: "Alternative `isFalse` has not bee provided"
   | isTrue h =>
     set_option trace.Meta.Tactic.simp.rewrite true in
     simp [h]
 
 theorem bad' : ∀ (m n : Nat), (if m = n then Ordering.eq else Ordering.gt) = Ordering.lt → False := by
-  intros m n
+  intro m n
   cases (Nat.decEq m n) with
   | isTrue h =>
     simp [h]
diff --git a/tests/lean/grind/experiments/bitvec.lean b/tests/lean/grind/experiments/bitvec.lean
index ac2a1c491d..ca8f571077 100644
--- a/tests/lean/grind/experiments/bitvec.lean
+++ b/tests/lean/grind/experiments/bitvec.lean
@@ -199,11 +199,11 @@ theorem eq_of_getLsbD_eq_iff {w : Nat} {x y : BitVec w} :
     x = y ↔ ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i := by
   have iff := @BitVec.eq_of_getElem_eq_iff w x y
   constructor
-  · intros heq i lt
+  · intro heq i lt
     have hext := iff.mp heq i lt
     simp only [← getLsbD_eq_getElem] at hext
     exact hext
-  · intros heq
+  · intro heq
     exact iff.mpr heq
 
 theorem eq_of_getMsbD_eq {x y : BitVec w}
@@ -755,14 +755,14 @@ its most significant bit is true.
 theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by
   have := toInt_eq_msb_cond x
   constructor
-  · intros h
+  · intro h
     apply Classical.byContradiction
-    intros hmsb
+    intro hmsb
     simp only [Bool.not_eq_true] at hmsb
     simp only [hmsb, Bool.false_eq_true, ↓reduceIte] at this
     simp only [BitVec.slt, toInt_zero, decide_eq_true_eq] at h
     omega /- Can't have `x.toInt` which is equal to `x.toNat` be strictly less than zero -/
-  · intros h
+  · intro h
     simp only [h, ↓reduceIte] at this
     simp only [BitVec.slt, this, toInt_zero, decide_eq_true_eq]
     omega
@@ -1972,7 +1972,7 @@ theorem toInt_ushiftRight_of_lt {x : BitVec w} {n : Nat} (hn : 0 < n) :
     (x >>> n).toInt = x.toNat >>> n := by
   rw [toInt_eq_toNat_cond]
   simp only [toNat_ushiftRight, ite_eq_left_iff, Nat.not_lt]
-  intros h
+  intro h
   by_cases hn : n ≤ w
   · have h1 := Nat.mul_lt_mul_of_pos_left (toNat_ushiftRight_lt x n hn) Nat.two_pos
     simp only [toNat_ushiftRight, Nat.zero_lt_succ, Nat.mul_lt_mul_left] at h1
@@ -2107,7 +2107,7 @@ theorem getLsbD_sshiftRight (x : BitVec w) (s i : Nat) :
       omega
     · simp only [hi, decide_false, Bool.not_false, Bool.true_and, Bool.eq_and_self,
         decide_eq_true_eq]
-      intros hlsb
+      intro hlsb
       apply BitVec.lt_of_getLsbD hlsb
   · by_cases hi : i ≥ w
     · simp [hi]
@@ -2159,7 +2159,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
   · simp [hw₀]
   · simp only [show ¬(w ≤ w - 1) by omega, decide_false, Bool.not_false, Bool.true_and,
       ite_eq_right_iff]
-    intros h
+    intro h
     simp [show n = 0 by omega]
 
 @[simp] theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x := by
@@ -2641,7 +2641,7 @@ theorem toInt_append {x : BitVec n} {y : BitVec m} :
     (x ++ 0#m).toInt = (2 ^ m) * x.toInt := by
   simp only [toInt_append, beq_iff_eq, toInt_zero, toNat_ofNat, Nat.zero_mod, Int.cast_ofNat_Int, Int.add_zero,
     ite_eq_right_iff]
-  intros h
+  intro h
   subst h
   simp [BitVec.eq_nil x]
 
@@ -2825,7 +2825,7 @@ theorem extractLsb'_append_extractLsb'_eq_extractLsb' {x : BitVec w} (h : start
   ext i h
   simp only [getElem_append, getElem_extractLsb', dite_eq_ite, getElem_cast, ite_eq_left_iff,
     Nat.not_lt]
-  intros hi
+  intro hi
   congr 1
   omega
 
@@ -2852,7 +2852,7 @@ theorem signExtend_eq_append_extractLsb' {w v : Nat} {x : BitVec w} :
   · simp only [hx, signExtend_eq_setWidth_of_msb_false, getElem_setWidth, Bool.false_eq_true,
       ↓reduceIte, getElem_append, getElem_extractLsb', Nat.zero_add, getElem_zero, dite_eq_ite,
       Bool.if_false_right, Bool.eq_and_self, decide_eq_true_eq]
-    intros hi
+    intro hi
     have hw : i < w := lt_of_getLsbD hi
     omega
   · simp [signExtend_eq_not_setWidth_not_of_msb_true hx, getElem_append, Nat.lt_min, hi]
@@ -2899,7 +2899,7 @@ theorem extractLsb'_append_eq_ite {v w} {xhi : BitVec v} {xlo : BitVec w} {start
     · simp only [hlen, ↓reduceDIte]
       ext i hi
       simp only [getElem_extractLsb', getLsbD_append, ite_eq_left_iff, Nat.not_lt]
-      intros hcontra
+      intro hcontra
       omega
     · simp only [hlen, ↓reduceDIte]
       ext i hi
@@ -3303,7 +3303,7 @@ theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
     have := two_mul_toInt_lt (x := y)
     simp only [Nat.add_one_sub_one]
     constructor
-    · intros h
+    · intro h
       rw_mod_cast [← Int.add_bmod_right, Int.bmod_eq_of_le]
       <;> omega
     · have := Int.bmod_neg_iff (x := x.toInt - y.toInt) (m := 2 ^ (w + 1))
@@ -3319,7 +3319,7 @@ theorem twoPow_le_toInt_sub_toInt_iff {x y : BitVec w} :
     have := le_two_mul_toInt (x := y); have := two_mul_toInt_lt (x := y)
     simp only [Nat.add_one_sub_one]
     constructor
-    · intros h
+    · intro h
       simp only [show 0 ≤ x.toInt by omega, show y.toInt < 0 by omega, _root_.true_and]
       rw_mod_cast [← Int.sub_bmod_right, Int.bmod_eq_of_le (by omega) (by omega)]
       omega
diff --git a/tests/lean/run/1787.lean b/tests/lean/run/1787.lean
index f09506a9ec..ade657de19 100644
--- a/tests/lean/run/1787.lean
+++ b/tests/lean/run/1787.lean
@@ -9,5 +9,5 @@ example {α : Type u}
     ∀ ⦃s t : Set (Sigma f)⦄,
         g s = g t → cast hU (g s).snd = cast hU (g t).snd :=
 by
-  intros g s t h
+  intro g s t h
   congr -- reduces to `(g s).snd = (g t).snd`, not `g s = g t`
diff --git a/tests/lean/run/4381.lean b/tests/lean/run/4381.lean
index 0a6ed99d33..affefecc8c 100644
--- a/tests/lean/run/4381.lean
+++ b/tests/lean/run/4381.lean
@@ -11,7 +11,7 @@ H1 : d = g
 -/
 #guard_msgs in
 example : ∀ d g, d = g → exists x : Nat, x = d := by
-  intros d g H1
+  intro d g H1
   constructor
   rewrite [H1,←H1,H1,←H1,H1]
   trace_state
diff --git a/tests/lean/run/aStructPerfIssue.lean b/tests/lean/run/aStructPerfIssue.lean
index 742f2fcee1..3c8b45ffe4 100644
--- a/tests/lean/run/aStructPerfIssue.lean
+++ b/tests/lean/run/aStructPerfIssue.lean
@@ -158,7 +158,7 @@ axiom funext {A : Type u} {B : A → Type v} {f g : ∀ x, B x} (p : f ~ g) : f
 
 def propIsSet {A : Type u} (r : prop A) : hset A :=
 by {
-  intros x y p q; have g := r x; apply Id.trans;
+  intro x y p q; have g := r x; apply Id.trans;
   apply Id.symm; apply rewriteComp;
   exact (apd g p)⁻¹ ⬝ transportComposition p (g x);
   induction q; apply invComp
@@ -181,7 +181,7 @@ def ntypeIsProp : ∀ (n : hlevel) {A : Type u}, prop (is-n-type A)
 
 def propIsProp {A : Type u} : prop (prop A) :=
 by {
-  intros f g;
+  intro f g;
   apply funext; intro;
   apply funext; intro;
   apply propIsSet; assumption
@@ -190,8 +190,8 @@ by {
 def minusOneEqvProp {A : Type u} : (is-(−1)-type A) ≃ prop A :=
 by {
   apply propEquivLemma; apply ntypeIsProp; apply propIsProp;
-  { intros H a b; exact (H a b).1 };
-  { intros H a b; exists H a b; apply propIsSet H }
+  { intro H a b; exact (H a b).1 };
+  { intro H a b; exists H a b; apply propIsSet H }
 }
 
 def equivFunext {A : Type u} {η μ : A → Type v}
diff --git a/tests/lean/run/autoboundIssues.lean b/tests/lean/run/autoboundIssues.lean
index ae5a1e96ca..3d825fe323 100644
--- a/tests/lean/run/autoboundIssues.lean
+++ b/tests/lean/run/autoboundIssues.lean
@@ -8,7 +8,7 @@ set_option pp.mvars false
 Auto-bound implicit appears in dot notation in the type, for a variable that appears later.
 -/
 example : n.succ = 1 → n = 0 := by
-  intros h; injection h
+  intro h; injection h
 
 /-!
 Auto-bound implicit appears in dot notation in a binder, for a variable that appears later.
diff --git a/tests/lean/run/casesAnyTypeIssue.lean b/tests/lean/run/casesAnyTypeIssue.lean
index 8e76165419..e384a66794 100644
--- a/tests/lean/run/casesAnyTypeIssue.lean
+++ b/tests/lean/run/casesAnyTypeIssue.lean
@@ -11,7 +11,7 @@ def symm {A : Type u} {a b : A} (p : a = b) : b = a :=
 by { induction p; exact Id.refl }
 
 def transportconst {A B : Type u} : A = B → A → B :=
-by { intros p x; induction p; exact x }
+by { intro p x; induction p; exact x }
 
 def transportconstInv {A B : Type u} (e : A = B) : B → A :=
 transportconst (symm e)
diff --git a/tests/lean/run/coinductive_predicates.lean b/tests/lean/run/coinductive_predicates.lean
index 765c358042..bc3fb76a24 100644
--- a/tests/lean/run/coinductive_predicates.lean
+++ b/tests/lean/run/coinductive_predicates.lean
@@ -62,13 +62,13 @@ theorem star_implies_star' (R : α → α → Prop) : ∀ a b : α, star R a b 
 
 -- More elaborate example from Xavier Leroy's compiler verification course
 theorem star_one (R : α → α → Prop)  : ∀ a b : α, R a b → star R a b := by
-  intros a b Rab
+  intro a b Rab
   apply star.star_step
   exact Rab
   apply star.star_refl
 
 theorem star_trans {α} (R : α → α → Prop) : ∀ (a b : α), star R a b → ∀ c : α, star R b c → star R a c := by
-  intros a b sab
+  intro a b sab
   intro c
   intro sbc
   induction sab
diff --git a/tests/lean/run/funind_proof.lean b/tests/lean/run/funind_proof.lean
index 0949527249..faf7c41daa 100644
--- a/tests/lean/run/funind_proof.lean
+++ b/tests/lean/run/funind_proof.lean
@@ -47,7 +47,7 @@ theorem numConsts_replaceConst (a b : String) (e : Term) : numConsts (replaceCon
   case case1 => intro c h; guard_hyp h :ₛ (a == c) = true; simp [replaceConst, numConsts, *]
   case case2 => intro c h; guard_hyp h :ₛ ¬(a == c) = true; simp [replaceConst, numConsts, *]
   case case3 =>
-    intros f cs ih
+    intro f cs ih
     guard_hyp ih :ₛnumConstsLst (replaceConstLst a b cs) = numConstsLst cs
     simp [replaceConst, numConsts, *]
   case case4 => simp [replaceConstLst, numConstsLst, *]
diff --git a/tests/lean/run/funind_unfolding.lean b/tests/lean/run/funind_unfolding.lean
index d66d6f9294..fb926f8d25 100644
--- a/tests/lean/run/funind_unfolding.lean
+++ b/tests/lean/run/funind_unfolding.lean
@@ -119,7 +119,7 @@ theorem filter_filter :
   refine filter.induct_unfolding p (motive := fun xs r => filter q r = filter (fun x => p x && q x) xs) ?case1 ?case2 ?case3 xs
   case case1 => rfl
   case case2 =>
-    intros x xs hp ih
+    intro x xs hp ih
     by_cases hq : q x
     case pos => simp [*, filter]
     case neg => simp [*, filter]
diff --git a/tests/lean/run/grind_bitvec2.lean b/tests/lean/run/grind_bitvec2.lean
index 26bf1d54b8..202f3e97c9 100644
--- a/tests/lean/run/grind_bitvec2.lean
+++ b/tests/lean/run/grind_bitvec2.lean
@@ -662,14 +662,14 @@ its most significant bit is true.
 theorem slt_zero_iff_msb_cond {x : BitVec w} : x.slt 0#w ↔ x.msb = true := by
   have := toInt_eq_msb_cond x
   constructor
-  · intros h
+  · intro h
     apply Classical.byContradiction
-    intros hmsb
+    intro hmsb
     simp only [Bool.not_eq_true] at hmsb
     simp only [hmsb, Bool.false_eq_true, ↓reduceIte] at this
     simp only [BitVec.slt, toInt_zero, decide_eq_true_eq] at h
     omega /- Can't have `x.toInt` which is equal to `x.toNat` be strictly less than zero -/
-  · intros h
+  · intro h
     simp only [h, ↓reduceIte] at this
     simp only [BitVec.slt, this, toInt_zero, decide_eq_true_eq]
     omega
@@ -1603,7 +1603,7 @@ theorem toInt_ushiftRight_of_lt {x : BitVec w} {n : Nat} (hn : 0 < n) :
     (x >>> n).toInt = x.toNat >>> n := by
   rw [toInt_eq_toNat_cond]
   simp only [toNat_ushiftRight, ite_eq_left_iff, Nat.not_lt]
-  intros h
+  intro h
   by_cases hn : n ≤ w
   · have h1 := Nat.mul_lt_mul_of_pos_left (toNat_ushiftRight_lt x n hn) Nat.two_pos
     simp only [toNat_ushiftRight, Nat.zero_lt_succ, Nat.mul_lt_mul_left] at h1
@@ -2073,7 +2073,7 @@ theorem toInt_append_zero {n m : Nat} {x : BitVec n} :
   -- FIXME: `grind` fails because of a reduction failure in`Lean.Grind.CommRing.Stepwise.d_step1_cert`.
   -- Something needs `@[expose]`, but what?
   -- grind only [two_mul_toInt_lt, le_two_mul_toInt, = toInt_zero_length]
-  intros h
+  intro h
   subst h
   simp [BitVec.eq_nil x]
 
@@ -2555,7 +2555,7 @@ theorem toInt_sub_toInt_lt_twoPow_iff {x y : BitVec w} :
     have := two_mul_toInt_lt (x := y)
     simp only [Nat.add_one_sub_one]
     constructor
-    · intros h
+    · intro h
       rw_mod_cast [← Int.add_bmod_right, Int.bmod_eq_of_le]
       <;> omega
     · have := Int.bmod_neg_iff (x := x.toInt - y.toInt) (m := 2 ^ (w + 1))
@@ -2571,7 +2571,7 @@ theorem twoPow_le_toInt_sub_toInt_iff {x y : BitVec w} :
     have := le_two_mul_toInt (x := y); have := two_mul_toInt_lt (x := y)
     simp only [Nat.add_one_sub_one]
     constructor
-    · intros h
+    · intro h
       simp only [show 0 ≤ x.toInt by omega, show y.toInt < 0 by omega, _root_.true_and]
       rw_mod_cast [← Int.sub_bmod_right, Int.bmod_eq_of_le (by omega) (by omega)]
       omega
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index f7f7279c1f..a0e08eb5da 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -107,7 +107,7 @@ case post => exact h1
 case pre => exact h3
 
 theorem simple9 (x y z : Nat) : y = z → x = x → x = y → x = z := by
-intros h1 _ h3
+intro h1 _ h3
 trace_state
 focus
   refine' Eq.trans ?pre ?post
@@ -119,7 +119,7 @@ focus
       assumption
 
 theorem simple9b (x y z : Nat) : y = z → x = x → x = y → x = z := by
-intros h1 _ h3
+intro h1 _ h3
 trace_state
 focus
   refine' Eq.trans ?pre ?post
@@ -129,14 +129,14 @@ focus
   assumption
 
 theorem simple9c (x y z : Nat) : y = z → x = x → x = y → x = z := by
-  intros h1 _ h3
+  intro h1 _ h3
   solve
     | exact h1
     | refine' Eq.trans ?pre ?post; exact y; exact h3; assumption
     | exact h3
 
 theorem simple9d (x y z : Nat) : y = z → x = x → x = y → x = z := by
-  intros h1 _ h3
+  intro h1 _ h3
   refine' Eq.trans ?pre ?post
   solve
     | exact h1
@@ -185,7 +185,7 @@ by {
 }
 
 theorem simple13 (x y z : Nat) : y = z → x = x → x = y → x = z := by
-intros h1 h2 h3
+intro h1 h2 h3
 trace_state
 apply @Eq.trans
 case b => exact y
@@ -193,7 +193,7 @@ trace_state
 repeat assumption
 
 theorem simple13b (x y z : Nat) : y = z → x = x → x = y → x = z := by {
-intros h1 h2 h3;
+intro h1 h2 h3;
 trace_state;
 apply @Eq.trans;
 case b => exact y;
@@ -209,9 +209,9 @@ repeat assumption
 
 theorem simple15 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
-  intros h1 h2 h3;
+  intro h1 h2 h3;
   revert y;
-  intros y h1 h3;
+  intro y h1 h3;
   apply Eq.trans;
   exact h3;
   exact h1
@@ -219,7 +219,7 @@ by {
 
 theorem simple16 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
-  intros h1 h2 h3;
+  intro h1 h2 h3;
   try clear x; -- should fail
   clear h2;
   trace_state;
@@ -369,7 +369,7 @@ def tst4 : {α : Type} → {β : Type} → α → β → α × β :=
 function α β a b => (a, b)
 
 theorem simple20 (x y z : Nat) : y = z → x = x → x = y → x = z :=
-by intros h1 h2 h3;
+by intro h1 h2 h3;
    try clear x; -- should fail
    clear h2;
    trace_state;
diff --git a/tests/lean/run/partial_fixpoint_probability.lean b/tests/lean/run/partial_fixpoint_probability.lean
index a50e12bb11..4bef5dcd8f 100644
--- a/tests/lean/run/partial_fixpoint_probability.lean
+++ b/tests/lean/run/partial_fixpoint_probability.lean
@@ -69,7 +69,7 @@ noncomputable instance : PartialOrder (Distr α) where
 noncomputable instance : CCPO (Distr α) where
   csup c x := ENNReal.sup fun (Distr : Subtype c) => Distr.val x
   csup_spec := by
-    intros d₁ c hchain
+    intro d₁ c hchain
     constructor
     next =>
       intro h d₂ hd₂ x
@@ -79,7 +79,7 @@ noncomputable instance : CCPO (Distr α) where
     next =>
       intro h x
       apply ENNReal.sup_le
-      intros Distr
+      intro Distr
       apply h Distr.1 Distr.2 x
 
 noncomputable instance : MonoBind Distr where
diff --git a/tests/lean/run/revert1.lean b/tests/lean/run/revert1.lean
index d40e1ffc74..af136a6b3b 100644
--- a/tests/lean/run/revert1.lean
+++ b/tests/lean/run/revert1.lean
@@ -2,7 +2,7 @@
 
 theorem tst1 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
-  intros h1 h2 h3;
+  intro h1 h2 h3;
   revert h2;
   intro h2;
   exact Eq.trans h3 h1
@@ -10,9 +10,9 @@ by {
 
 theorem tst2 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
-  intros h1 h2 h3;
+  intro h1 h2 h3;
   revert y;
-  intros y hb ha;
+  intro y hb ha;
   exact Eq.trans ha hb
 }
 
diff --git a/tests/lean/run/rewrites.lean b/tests/lean/run/rewrites.lean
index 14a2d26e15..388cfcc61a 100644
--- a/tests/lean/run/rewrites.lean
+++ b/tests/lean/run/rewrites.lean
@@ -26,7 +26,7 @@ example (h : Int) (hyp : g * 1 = h) : g = h := by
 
 #guard_msgs(drop info) in
 example : ∀ (x y : Nat), x ≤ y := by
-  intros x y
+  intro x y
   rw? -- Used to be an error here https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/panic.20and.20error.20with.20rw.3F/near/370495531
   exact test_sorry
 
diff --git a/tests/lean/run/state8.lean b/tests/lean/run/state8.lean
index 99d93a13aa..fdbd2073d8 100644
--- a/tests/lean/run/state8.lean
+++ b/tests/lean/run/state8.lean
@@ -67,5 +67,5 @@ def f : States → States → States
 | s7, s7 => s0
 set_option maxHeartbeats 0
 example : ∀ x y z, f (f (f s0 x) y) z = f (f x z) (f y z) := by
- intros x y z
+ intro x y z
  cases x <;> cases y <;> cases z <;> rfl
diff --git a/tests/lean/run/subst1.lean b/tests/lean/run/subst1.lean
index ef0d4d9720..d9f1365101 100644
--- a/tests/lean/run/subst1.lean
+++ b/tests/lean/run/subst1.lean
@@ -3,12 +3,12 @@
 set_option trace.Meta.Tactic.subst true
 
 theorem tst1 (x y z : Nat) : y = z → x = x → x = y → x = z := by
-  intros h1 h2 h3
+  intro h1 h2 h3
   subst x
   assumption
 
 theorem tst2 (x y z : Nat) : y = z → x = z + y → x = z + z := by
-  intros h1 h2
+  intro h1 h2
   subst h1
   subst h2
   exact rfl
diff --git a/tests/lean/run/tacticExtOverlap.lean b/tests/lean/run/tacticExtOverlap.lean
index ebee3f77b4..44c6ca022c 100644
--- a/tests/lean/run/tacticExtOverlap.lean
+++ b/tests/lean/run/tacticExtOverlap.lean
@@ -1,25 +1,25 @@
 open Lean
 
-syntax (name := myintro) "intros" sepBy(ident, ",") : tactic
+syntax (name := myintro) "intro" sepBy(ident, ",") : tactic
 
 macro_rules (kind := myintro)
-| `(tactic| intros $x,*) => pure $ mkNode `Lean.Parser.Tactic.intros #[mkAtom "intros", mkNullNode x]
+| `(tactic| intro $x,*) => pure $ mkNode `Lean.Parser.Tactic.intro #[mkAtom "intro", mkNullNode x]
 
 theorem tst1 {p q : Prop} : p → q → p :=
 by {
-  intros h1, h2;
+  intro h1, h2;
   assumption
 }
 
 theorem tst2 {p q : Prop} : p → q → p :=
 by {
-  intros h1; -- the builtin and myintro overlap here.
-  intros h2; -- the builtin and myintro overlap here.
+  intro h1; -- the builtin and myintro overlap here.
+  intro h2; -- the builtin and myintro overlap here.
   assumption
 }
 
 theorem tst3 {p q : Prop} : p → q → p :=
 by {
-  intros h1 h2;
+  intro h1 h2;
   assumption
 }
diff --git a/tests/lean/run/tacticTests.lean b/tests/lean/run/tacticTests.lean
index 5f1659b59d..bbde57a388 100644
--- a/tests/lean/run/tacticTests.lean
+++ b/tests/lean/run/tacticTests.lean
@@ -36,12 +36,12 @@ theorem ex6 {m n : Nat} : Le m.succ n.succ → Le m n := by
   revert m
   induction n with
   | zero =>
-    intros m h;
+    intro m h;
     cases h with
     | base => apply Le.base
     | succ n h => exact absurd h (ex4 _)
   | succ n ih =>
-    intros m h
+    intro m h
     have aux := ih (m := m)
     cases ex5 h with
     | inl h =>
diff --git a/tests/playground/pge.lean b/tests/playground/pge.lean
index c14f53c8ec..be82cfbbc0 100644
--- a/tests/playground/pge.lean
+++ b/tests/playground/pge.lean
@@ -52,13 +52,13 @@ theorem lt_or_eq_of_succ {i j:Nat} (lt : i < Nat.succ j) : i < j ∨ i = j :=
 theorem strong_induction_on {p : Nat → Prop} (n:Nat)
   (h:∀n, (∀ m, m < n → p m) → p n) : p n := by
     suffices ∀n m, m < n → p m from this (succ n) n (Nat.lt_succ_self _)
-    intros n
+    intro n
     induction n with
     | zero =>
-      intros m h
+      intro m h
       contradiction
     | succ i ind =>
-      intros m h1
+      intro m h1
       cases Nat.lt_or_eq_of_succ h1 with
       | inl is_lt =>
         apply ind _ is_lt
@@ -77,9 +77,9 @@ theorem Fin.strong_induction_on {P : Fin w → Prop} (i:Fin w)
    | mk i i_lt =>
      revert i_lt
      apply @Nat.strong_induction_on (λi => ∀ (i_lt : i < w), P { val := i, isLt := i_lt })
-     intros j p j_lt_w
+     intro j p j_lt_w
      apply ind ⟨j, j_lt_w⟩
-     intros z z_lt_j
+     intro z z_lt_j
      apply p _ z_lt_j
 
 namespace PEG
@@ -247,7 +247,7 @@ theorem is_deterministic
       (p i).leftnonterminal = (q j).leftnonterminal
       → (p i).position      = (q j).position
       → (p i).record_result = (q j).record_result := by
-  intros p q i0
+  intro p q i0
   induction i0 using Fin.strong_induction_on with
   | ind i ind =>
   intro j eq_nt p_pos_eq_q_pos