move deprecations to Init/Notation

doc/lean3changes.md

@@ -193,7 +193,7 @@ Ellipsis are also useful when explicit argument can be automatically inferred by
 to avoid a sequence of `_`s.
 ```lean
 example (f : Nat → Nat) (a b c : Nat) : f (a + b + c) = f (a + (b + c)) :=
-  congrArg f (Nat.add_assoc ..)
+  congr_arg f (Nat.add_assoc ..)
 ```
 
 In Lean 4, writing `f(x)` in place of `f x` is no longer allowed, you must use whitespace between the function and its arguments (e.g., `f (x)`).

doc/syntax_highlight_in_latex.md

@@ -28,7 +28,7 @@ Save [`lstlean.tex`](https://raw.githubusercontent.com/leanprover/lean4/master/d
 \begin{lstlisting}
 theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by
   show extfunApp (Quotient.mk f₁) = extfunApp (Quotient.mk f₂)
-  apply congrArg
+  apply congr_arg
   apply Quotient.sound
   exact h
 \end{lstlisting}
@@ -60,7 +60,7 @@ First [install Pygments](https://pygments.org/download/). Then save [`lean4.py`]
 \begin{leancode}
 theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by
   show extfunApp (Quotient.mk' f₁) = extfunApp (Quotient.mk' f₂)
-  apply congrArg
+  apply congr_arg
   apply Quotient.sound
   exact h
 \end{leancode}

src/Init/Core.lean

@@ -841,7 +841,7 @@ abbrev noConfusionEnum {α : Sort u} {β : Sort v} [inst : DecidableEq β] (f :
   Decidable.casesOn
     (motive := fun (inst : Decidable (f x = f y)) => Decidable.casesOn (motive := fun _ => Sort w) inst (fun _ => P) (fun _ => P → P))
     (inst (f x) (f y))
-    (fun h' => False.elim (h' (congrArg f h)))
+    (fun h' => False.elim (h' (congr_arg f h)))
     (fun _ => fun x => x)
 
 /-! # Inhabited -/
@@ -1560,7 +1560,7 @@ theorem funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
       (fun (f : ∀ (x : α), β x) => f x)
       (fun _ _ h => h x)
   show extfunApp (Quot.mk eqv f) = extfunApp (Quot.mk eqv g)
-  exact congrArg extfunApp (Quot.sound h)
+  exact congr_arg extfunApp (Quot.sound h)
 
 instance {α : Sort u} {β : α → Sort v} [∀ a, Subsingleton (β a)] : Subsingleton (∀ a, β a) where
   allEq f g := funext fun a => Subsingleton.elim (f a) (g a)

src/Init/Data/AC.lean

@@ -315,7 +315,7 @@ theorem Context.eval_norm (ctx : Context α) (e : Expr) : evalList α ctx (norm
   simp_all [evalList_removeNeutrals, eval_toList, toList_nonEmpty, evalList_mergeIdem, evalList_sort]
 
 theorem Context.eq_of_norm (ctx : Context α) (a b : Expr) (h : norm ctx a == norm ctx b) : eval α ctx a = eval α ctx b := by
-  have h := congrArg (evalList α ctx) (eq_of_beq h)
+  have h := congr_arg (evalList α ctx) (eq_of_beq h)
   rw [eval_norm, eval_norm] at h
   assumption
 

src/Init/Data/Array/Basic.lean

@@ -605,7 +605,7 @@ theorem ext (a b : Array α)
         have tailEq : as = bs := ih bs h₁' h₂'
         rw [headEq, tailEq]
   cases a; cases b
-  apply congrArg
+  apply congr_arg
   apply extAux
   assumption
   assumption

src/Init/Data/List/BasicAux.lean

@@ -143,8 +143,8 @@ theorem append_cancel_left {as bs cs : List α} (h : as ++ bs = as ++ cs) : bs =
 theorem append_cancel_right {as bs cs : List α} (h : as ++ bs = cs ++ bs) : as = cs := by
   match as, cs with
   | [], []       => rfl
-  | [], c::cs    => have aux := congrArg length h; simp_arith at aux
-  | a::as, []    => have aux := congrArg length h; simp_arith at aux
+  | [], c::cs    => have aux := congr_arg length h; simp_arith at aux
+  | a::as, []    => have aux := congr_arg length h; simp_arith at aux
   | a::as, c::cs => injection h with h₁ h₂; subst h₁; rw [append_cancel_right h₂]
 
 @[simp] theorem append_cancel_left_eq (as bs cs : List α) : (as ++ bs = as ++ cs) = (bs = cs) := by

src/Init/Data/Nat/Basic.lean

@@ -113,11 +113,11 @@ instance : LawfulBEq Nat where
 
 @[simp] protected theorem zero_add : ∀ (n : Nat), 0 + n = n
   | 0   => rfl
-  | n+1 => congrArg succ (Nat.zero_add n)
+  | n+1 => congr_arg succ (Nat.zero_add n)
 
 theorem succ_add : ∀ (n m : Nat), (succ n) + m = succ (n + m)
   | _, 0   => rfl
-  | n, m+1 => congrArg succ (succ_add n m)
+  | n, m+1 => congr_arg succ (succ_add n m)
 
 theorem add_succ (n m : Nat) : n + succ m = succ (n + m) :=
   rfl
@@ -131,13 +131,13 @@ theorem succ_eq_add_one (n : Nat) : succ n = n + 1 :=
 protected theorem add_comm : ∀ (n m : Nat), n + m = m + n
   | n, 0   => Eq.symm (Nat.zero_add n)
   | n, m+1 => by
-    have : succ (n + m) = succ (m + n) := by apply congrArg; apply Nat.add_comm
+    have : succ (n + m) = succ (m + n) := by apply congr_arg; apply Nat.add_comm
     rw [succ_add m n]
     apply this
 
 protected theorem add_assoc : ∀ (n m k : Nat), (n + m) + k = n + (m + k)
   | _, _, 0      => rfl
-  | n, m, succ k => congrArg succ (Nat.add_assoc n m k)
+  | n, m, succ k => congr_arg succ (Nat.add_assoc n m k)
 
 protected theorem add_left_comm (n m k : Nat) : n + (m + k) = m + (n + k) := by
   rw [← Nat.add_assoc, Nat.add_comm n m, Nat.add_assoc]
@@ -184,7 +184,7 @@ protected theorem mul_comm : ∀ (n m : Nat), n * m = m * n
 protected theorem left_distrib (n m k : Nat) : n * (m + k) = n * m + n * k := by
   induction n generalizing m k with
   | zero      => repeat rw [Nat.zero_mul]
-  | succ n ih => simp [succ_mul, ih]; rw [Nat.add_assoc, Nat.add_assoc (n*m)]; apply congrArg; apply Nat.add_left_comm
+  | succ n ih => simp [succ_mul, ih]; rw [Nat.add_assoc, Nat.add_assoc (n*m)]; apply congr_arg; apply Nat.add_left_comm
 
 protected theorem right_distrib (n m k : Nat) : (n + m) * k = n * k + m * k := by
   rw [Nat.mul_comm, Nat.left_distrib]; simp [Nat.mul_comm]
@@ -218,7 +218,7 @@ theorem lt_succ_of_le {n m : Nat} : n ≤ m → n < succ m :=
 theorem succ_sub_succ_eq_sub (n m : Nat) : succ n - succ m = n - m := by
   induction m with
   | zero      => exact rfl
-  | succ m ih => apply congrArg pred ih
+  | succ m ih => apply congr_arg pred ih
 
 theorem pred_le : ∀ (n : Nat), pred n ≤ n
   | zero   => Nat.le.refl
@@ -384,7 +384,7 @@ protected theorem add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) : k + n
   match le.dest h with
   | ⟨w, hw⟩ =>
     have h₁ : k + n + w = k + (n + w) := Nat.add_assoc ..
-    have h₂ : k + (n + w) = k + m     := congrArg _ hw
+    have h₂ : k + (n + w) = k + m     := congr_arg _ hw
     le.intro <| h₁.trans h₂
 
 protected theorem add_le_add_right {n m : Nat} (h : n ≤ m) (k : Nat) : n + k ≤ m + k := by

src/Init/Data/Nat/Linear.lean

@@ -532,7 +532,7 @@ attribute [local simp] Expr.denote_toPoly
 
 theorem Expr.eq_of_toNormPoly (ctx : Context) (a b : Expr) (h : a.toNormPoly = b.toNormPoly) : a.denote ctx = b.denote ctx := by
   simp [toNormPoly, Poly.norm] at h
-  have h := congrArg (Poly.denote ctx) h
+  have h := congr_arg (Poly.denote ctx) h
   simp at h
   assumption
 
@@ -711,12 +711,12 @@ theorem Poly.denote_toExpr (ctx : Context) (p : Poly) : p.toExpr.denote ctx = p.
   | (k, v) :: p => simp [toExpr, Expr.denote, Poly.denote]
 
 theorem ExprCnstr.eq_of_toNormPoly_eq (ctx : Context) (c d : ExprCnstr) (h : c.toNormPoly == d.toPoly) : c.denote ctx = d.denote ctx := by
-  have h := congrArg (PolyCnstr.denote ctx) (eq_of_beq h)
+  have h := congr_arg (PolyCnstr.denote ctx) (eq_of_beq h)
   simp at h
   assumption
 
 theorem Expr.eq_of_toNormPoly_eq (ctx : Context) (e e' : Expr) (h : e.toNormPoly == e'.toPoly) : e.denote ctx = e'.denote ctx := by
-  have h := congrArg (Poly.denote ctx) (eq_of_beq h)
+  have h := congr_arg (Poly.denote ctx) (eq_of_beq h)
   simp [Expr.toNormPoly, Poly.norm] at h
   assumption
 

src/Init/Data/Nat/SOM.lean

@@ -178,7 +178,7 @@ theorem Expr.toPoly_denote (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e.
   | mul a b => simp! [Poly.mul_denote, *]
 
 theorem Expr.eq_of_toPoly_eq (ctx : Context) (a b : Expr) (h : a.toPoly == b.toPoly) : a.denote ctx = b.denote ctx := by
-  have h := congrArg (Poly.denote ctx) (eq_of_beq h)
+  have h := congr_arg (Poly.denote ctx) (eq_of_beq h)
   simp [toPoly_denote] at h
   assumption
 

src/Init/Data/Option/Instances.lean

@@ -12,7 +12,7 @@ theorem Option.eq_of_eq_some {α : Type u} : ∀ {x y : Option α}, (∀z, x = s
   | none,   none,   _ => rfl
   | none,   some z, h => Option.noConfusion ((h z).2 rfl)
   | some z, none,   h => Option.noConfusion ((h z).1 rfl)
-  | some _, some w, h => Option.noConfusion ((h w).2 rfl) (congrArg some)
+  | some _, some w, h => Option.noConfusion ((h w).2 rfl) (congr_arg some)
 
 theorem Option.eq_none_of_isNone {α : Type u} : ∀ {o : Option α}, o.isNone → o = none
   | none, _ => rfl

src/Init/Data/Prod.lean

@@ -9,5 +9,5 @@ import Init.SimpLemmas
 instance [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β] : LawfulBEq (α × β) where
   eq_of_beq {a b} (h : a.1 == b.1 && a.2 == b.2) := by
     cases a; cases b
-    refine congr (congrArg _ (eq_of_beq ?_)) (eq_of_beq ?_) <;> simp_all
+    refine congr (congr_arg _ (eq_of_beq ?_)) (eq_of_beq ?_) <;> simp_all
   rfl {a} := by cases a; simp [BEq.beq, LawfulBEq.rfl]

src/Init/Data/String/Basic.lean

@@ -141,7 +141,7 @@ theorem utf8PrevAux_lt_of_pos : ∀ (cs : List Char) (i p : Pos), p ≠ 0 →
     (utf8PrevAux cs i p).1 < p.1
   | [], i, p, h =>
     Nat.lt_of_le_of_lt (Nat.zero_le _)
-      (Nat.zero_lt_of_ne_zero (mt (congrArg Pos.mk) h))
+      (Nat.zero_lt_of_ne_zero (mt (congr_arg Pos.mk) h))
   | c::cs, i, p, h => by
     simp [utf8PrevAux]
     apply iteInduction (motive := (Pos.byteIdx · < _)) <;> intro h'
@@ -386,7 +386,7 @@ termination_by _ => stopPos.1 - i.1
 
 @[specialize] def foldrAux {α : Type u} (f : Char → α → α) (a : α) (s : String) (i begPos : Pos) : α :=
   if h : begPos < i then
-    have := String.prev_lt_of_pos s i <| mt (congrArg String.Pos.byteIdx) <|
+    have := String.prev_lt_of_pos s i <| mt (congr_arg String.Pos.byteIdx) <|
       Ne.symm <| Nat.ne_of_lt <| Nat.lt_of_le_of_lt (Nat.zero_le _) h
     let i := s.prev i
     let a := f (s.get i) a
@@ -418,7 +418,7 @@ s.any (fun a => a == c)
 theorem utf8SetAux_of_gt (c' : Char) : ∀ (cs : List Char) {i p : Pos}, i > p → utf8SetAux c' cs i p = cs
   | [],    _, _, _ => rfl
   | c::cs, i, p, h => by
-    rw [utf8SetAux, if_neg (mt (congrArg (·.1)) (Ne.symm <| Nat.ne_of_lt h)), utf8SetAux_of_gt c' cs]
+    rw [utf8SetAux, if_neg (mt (congr_arg (·.1)) (Ne.symm <| Nat.ne_of_lt h)), utf8SetAux_of_gt c' cs]
     exact Nat.lt_of_lt_of_le h (Nat.le_add_right ..)
 
 theorem set_next_add (s : String) (i : Pos) (c : Char) (b₁ b₂)
@@ -543,7 +543,7 @@ theorem lt_next (s : Substring) (i : String.Pos) (h : i.1 < s.bsize) :
     i.1 < (s.next i).1 := by
   simp [next]; rw [if_neg ?a]
   case a =>
-    refine mt (congrArg String.Pos.byteIdx) (Nat.ne_of_lt ?_)
+    refine mt (congr_arg String.Pos.byteIdx) (Nat.ne_of_lt ?_)
     exact (Nat.add_comm .. ▸ Nat.add_lt_of_lt_sub h :)
   apply Nat.lt_sub_of_add_lt
   rw [Nat.add_comm]; apply String.lt_next
@@ -654,7 +654,7 @@ termination_by _ => stopPos.1 - i.1
 
 @[specialize] def takeRightWhileAux (s : String) (begPos : String.Pos) (p : Char → Bool) (i : String.Pos) : String.Pos :=
   if h : begPos < i then
-    have := String.prev_lt_of_pos s i <| mt (congrArg String.Pos.byteIdx) <|
+    have := String.prev_lt_of_pos s i <| mt (congr_arg String.Pos.byteIdx) <|
       Ne.symm <| Nat.ne_of_lt <| Nat.lt_of_le_of_lt (Nat.zero_le _) h
     let i' := s.prev i
     let c  := s.get i'

src/Init/Notation.lean

@@ -490,3 +490,18 @@ a string literal with the contents of the file at `"parent_dir" / "path" / "to"
 file cannot be read, elaboration fails.
 -/
 syntax (name := includeStr) "include_str " term : term
+
+-- The following deprecations are have their replacements defined in earlier files,
+-- and as `deprecated` can not be applied to imported declarations,
+-- we have moved the old versions here.
+
+/-- Deprecated synyonym for `congr_arg`. -/
+@[deprecated congr_arg]
+theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
+  h ▸ rfl
+
+
+/-- Deprecated synyonym for `congr_fun`. -/
+@[deprecated congr_fun]
+theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : Eq f g) (a : α) : Eq (f a) (g a) :=
+  h ▸ rfl

src/Init/Prelude.lean

@@ -359,7 +359,7 @@ subterms.
 
 For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
-theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
+theorem congr_arg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
   h ▸ rfl
 
 /--
@@ -373,7 +373,7 @@ theorem congr {α : Sort u} {β : Sort v} {f₁ f₂ : α → β} {a₁ a₂ :
   h₁ ▸ h₂ ▸ rfl
 
 /-- Congruence in the function part of an application: If `f = g` then `f a = g a`. -/
-theorem congrFun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : Eq f g) (a : α) : Eq (f a) (g a) :=
+theorem congr_fun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : Eq f g) (a : α) : Eq (f a) (g a) :=
   h ▸ rfl
 
 /-!
@@ -2358,7 +2358,7 @@ This function is overridden with a native implementation.
 def String.decEq (s₁ s₂ : @& String) : Decidable (Eq s₁ s₂) :=
   match s₁, s₂ with
   | ⟨s₁⟩, ⟨s₂⟩ =>
-    dite (Eq s₁ s₂) (fun h => isTrue (congrArg _ h)) (fun h => isFalse (fun h' => String.noConfusion h' (fun h' => absurd h' h)))
+    dite (Eq s₁ s₂) (fun h => isTrue (congr rfl h)) (fun h => isFalse (fun h' => String.noConfusion h' (fun h' => absurd h' h)))
 
 instance : DecidableEq String := String.decEq
 

src/Lean/Elab/Deriving/DecEq.lean

@@ -179,7 +179,7 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do
       fun x y =>
         if h : x.toCtorIdx = y.toCtorIdx then
           -- We use `rfl` in the following proof because the first script fails for unit-like datatypes due to etaStruct.
-          isTrue (by first | have aux := congrArg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
+          isTrue (by first | have aux := congr_arg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl)
         else
           isFalse fun h => by subst h; contradiction
   )

src/Lean/Meta/AppBuilder.lean

@@ -175,9 +175,9 @@ def mkCongrArg (f h : Expr) : MetaM Expr := do
     | some (α, β), some (_, a, b) =>
       let u ← getLevel α
       let v ← getLevel β
-      return mkApp6 (mkConst ``congrArg [u, v]) α β a b f h
-    | none, _ => throwAppBuilderException ``congrArg ("non-dependent function expected" ++ hasTypeMsg f fType)
-    | _, none => throwAppBuilderException ``congrArg ("equality proof expected" ++ hasTypeMsg h hType)
+      return mkApp6 (mkConst ``congr_arg [u, v]) α β a b f h
+    | none, _ => throwAppBuilderException ``congr_arg ("non-dependent function expected" ++ hasTypeMsg f fType)
+    | _, none => throwAppBuilderException ``congr_arg ("equality proof expected" ++ hasTypeMsg h hType)
 
 /-- Given `h : f = g` and `a : α`, returns a proof of `f a = g a`.-/
 def mkCongrFun (h a : Expr) : MetaM Expr := do
@@ -193,9 +193,9 @@ def mkCongrFun (h a : Expr) : MetaM Expr := do
         let β' := Lean.mkLambda n BinderInfo.default α β
         let u ← getLevel α
         let v ← getLevel (mkApp β' a)
-        return mkApp6 (mkConst ``congrFun [u, v]) α β' f g h a
-      | _ => throwAppBuilderException ``congrFun ("equality proof between functions expected" ++ hasTypeMsg h hType)
-    | _ => throwAppBuilderException ``congrFun ("equality proof expected" ++ hasTypeMsg h hType)
+        return mkApp6 (mkConst ``congr_fun [u, v]) α β' f g h a
+      | _ => throwAppBuilderException ``congr_fun ("equality proof between functions expected" ++ hasTypeMsg h hType)
+    | _ => throwAppBuilderException ``congr_fun ("equality proof expected" ++ hasTypeMsg h hType)
 
 /-- Given `h₁ : f = g` and `h₂ : a = b`, returns a proof of `f a = g b`. -/
 def mkCongr (h₁ h₂ : Expr) : MetaM Expr := do

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -225,7 +225,7 @@ where
 
 /--
 Given a simplified function result `r` and arguments `args`, simplify arguments using `simp` and `dsimp`.
-The resulting proof is built using `congr` and `congrFun` theorems.
+The resulting proof is built using `congr` and `congr_fun` theorems.
 -/
 def congrArgs (r : Result) (args : Array Expr) : SimpM Result := do
   if args.isEmpty then
@@ -249,7 +249,7 @@ def congrArgs (r : Result) (args : Array Expr) : SimpM Result := do
 Retrieve auto-generated congruence lemma for `f`.
 
 Remark: If all argument kinds are `fixed` or `eq`, it returns `none` because
-using simple congruence theorems `congr`, `congrArg`, and `congrFun` produces a more compact proof.
+using simple congruence theorems `congr`, `congr_arg`, and `congr_fun` produces a more compact proof.
 -/
 def mkCongrSimp? (f : Expr) : SimpM (Option CongrTheorem) := do
   if f.isConst then if (← isMatcher f.constName!) then

src/library/constants.cpp

@@ -153,7 +153,7 @@ void initialize_constants() {
     mark_persistent(g_cast->raw());
     g_char = new name{"Char"};
     mark_persistent(g_char->raw());
-    g_congr_arg = new name{"congrArg"};
+    g_congr_arg = new name{"congr_arg"};
     mark_persistent(g_congr_arg->raw());
     g_decidable = new name{"Decidable"};
     mark_persistent(g_decidable->raw());

src/library/constants.txt

@@ -20,7 +20,7 @@ Bool.true
 Bool.casesOn
 cast
 Char
-congrArg
+congr_arg
 Decidable
 Decidable.isTrue
 Decidable.isFalse

tests/lean/1870.lean

@@ -17,15 +17,15 @@ instance One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α where
   one := 1
 
 theorem ex1 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
-  refine' congrArg _ (congrArg _ _)
+  refine' congr_arg _ (congr_arg _ _)
   rfl
 
 example : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
-  apply congrArg
-  apply congrArg
+  apply congr_arg
+  apply congr_arg
   apply rfl
 
 theorem ex2 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by
-  apply congrArg
-  apply congrArg
+  apply congr_arg
+  apply congr_arg
   apply rfl

tests/lean/1870.lean.expected.out

@@ -1,15 +1,15 @@
 1870.lean:20:2-20:35: error: type mismatch
-  congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?m)
+  congr_arg (@OfNat.ofNat Nat 0) (congr_arg (@Zero.toOfNat0 Nat) ?m)
 has type
   OfNat.ofNat 0 = OfNat.ofNat 0 : Prop
 but is expected to have type
   OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
-1870.lean:24:2-24:16: error: tactic 'apply' failed, failed to unify
+1870.lean:24:2-24:17: error: tactic 'apply' failed, failed to unify
   ?f ?a₁ = ?f ?a₂
 with
   OfNat.ofNat 0 = OfNat.ofNat 1
 ⊢ OfNat.ofNat 0 = OfNat.ofNat 1
-1870.lean:29:2-29:16: error: tactic 'apply' failed, failed to unify
+1870.lean:29:2-29:17: error: tactic 'apply' failed, failed to unify
   ?f ?a₁ = ?f ?a₂
 with
   OfNat.ofNat 0 = OfNat.ofNat 1

tests/lean/Reformat.lean.expected.out

@@ -104,7 +104,7 @@ theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
 def cast {α β : Sort u} (h : Eq α β) (a : α) : β :=
   Eq.rec (motive := fun α _ => α) a h
 
-theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
+theorem congr_arg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
   h ▸ rfl
 
 /-

tests/lean/Reformat/Input.lean

@@ -86,7 +86,7 @@ theorem Eq.symm {α : Sort u} {a b : α} (h : Eq a b) : Eq b a :=
 @[macro_inline] def cast {α β : Sort u} (h : Eq α β) (a : α) : β :=
   Eq.rec (motive := fun α _ => α) a h
 
-theorem congrArg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
+theorem congr_arg {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β) (h : Eq a₁ a₂) : Eq (f a₁) (f a₂) :=
   h ▸ rfl
 
 /-

tests/lean/elabAsElim.lean

@@ -50,7 +50,7 @@ structure Point where
 theorem PointExt_lean4 (p : Point) : forall (q : Point) (h1 : Point.x p = Point.x q), p = q :=
   Point.recOn p <|
    fun z1 q => Point.recOn q $
-   fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congrArg Point.mk hA
+   fun z2 (hA : Point.x (Point.mk z1) = Point.x (Point.mk z2)) => congr_arg Point.mk hA
 
 inductive pos_num : Type
   | one  : pos_num

tests/lean/run/1311.lean

@@ -1,6 +1,6 @@
 instance : DecidableEq ByteArray
   | ⟨a⟩, ⟨b⟩ => match decEq a b with
-    | isTrue h₁  => isTrue $ congrArg ByteArray.mk h₁
+    | isTrue h₁  => isTrue $ congr_arg ByteArray.mk h₁
     | isFalse h₂ => isFalse $ fun h => by cases h; cases (h₂ rfl)
 
 #eval ByteArray.empty = ByteArray.empty

tests/lean/run/1426.lean

@@ -12,6 +12,6 @@ theorem ex2 : a * 2 = 2 * a := by
     rfl
   conv at h =>
     lhs; intro x y; rw [Nat.mul_comm]
-  exact congrFun (congrFun h 2) a
+  exact congr_fun (congr_fun h 2) a
 
 #print ex2

tests/lean/run/1436.lean

@@ -2,15 +2,15 @@ import Lean
 open List Lean
 
 example (l : List α) (h : length l = length l) : length (a::l) = length (a::l) :=
-  congrArg (·+1) h
+  congr_arg (·+1) h
 
 elab:max "(" tm:term ":)" : term => Elab.Term.elabTerm tm none
 
 example (l : List α) (h : length l = length l) : length (a::l) = length (a::l) :=
-  (congrArg (·+1) h :)
+  (congr_arg (·+1) h :)
 
 example (l : List α) (h : length l = length l) : length (a::l) = length (a::l) :=
-  have := congrArg (·+1) h; this
+  have := congr_arg (·+1) h; this
 
 example (l : List α) (h : length l = length l) : length (a::l) = length (a::l) := by
-  have := congrArg (·+1) h; exact this
+  have := congr_arg (·+1) h; exact this

tests/lean/run/270.lean

@@ -6,7 +6,7 @@ open CommAddSemigroup
 
 theorem addComm3 [CommAddSemigroup α] {a b c : α} : a + b + c = a + c + b := by {
     have h : b + c = c + b := addComm;
-    have h' := congrArg (a + ·) h;
+    have h' := congr_arg (a + ·) h;
     simp at h';
     rw [←addAssoc] at h';
     rw [←addAssoc (a := a)] at h';
@@ -20,7 +20,7 @@ theorem addComm4 [CommAddSemigroup α] {a b c : α} : a + b + c = a + c + b := b
 
 theorem addComm5 [CommAddSemigroup α] {a b c : α} : a + b + c = a + c + b := by {
     have h : b + c = c + b := addComm;
-    have h' := congrArg (a + ·) h;
+    have h' := congr_arg (a + ·) h;
     simp at h';
     rw [←addAssoc] at h';
     rw [←@addAssoc (a := a)] at h';
@@ -29,7 +29,7 @@ theorem addComm5 [CommAddSemigroup α] {a b c : α} : a + b + c = a + c + b := b
 
 theorem addComm6 [CommAddSemigroup α] {a b c : α} : a + b + c = a + c + b := by {
     have h : b + c = c + b := addComm;
-    have h' := congrArg (a + ·) h;
+    have h' := congr_arg (a + ·) h;
     simp at h';
     rw [←addAssoc] at h';
     rw [←addAssoc] at h';

tests/lean/run/KyleAlg.lean

@@ -155,7 +155,7 @@ theorem addIdemIffZero [AddGroup α] {a : α} : a + a = a ↔ a = 0 := by
     apply Iff.intro
     focus
         intro h
-        have h' := congrArg (λ x => x + -a) h
+        have h' := congr_arg (λ x => x + -a) h
         simp at h'
         rw [addAssoc, addNeg, addZero] at h'
         exact h'

tests/lean/run/KyleAlgAbbrev.lean

@@ -132,7 +132,7 @@ theorem addIdemIffZero [AddGroup α] {a : α} : a + a = a ↔ a = 0 := by
     apply Iff.intro
     focus
         intro h
-        have h' := congrArg (λ x => x + -a) h
+        have h' := congr_arg (λ x => x + -a) h
         simp at h'
         rw [addAssoc, addNeg, addZero] at h'
         exact h'

tests/lean/run/ac_expr.lean

@@ -44,7 +44,7 @@ theorem Expr.denote_flat (ctx : Context α) (e : Expr) : denote ctx (flat e) = d
   | op a b ih₁ ih₂ => simp [flat, denote, denote_concat, ih₁, ih₂]
 
 theorem Expr.eq_of_flat (ctx : Context α) (a b : Expr) (h : flat a = flat b) : denote ctx a = denote ctx b := by
-  have h := congrArg (denote ctx) h
+  have h := congr_arg (denote ctx) h
   simp [denote_flat] at h
   assumption
 
@@ -127,7 +127,7 @@ where
       | _ => rfl
 
 theorem Expr.eq_of_sort_flat (ctx : Context α) (a b : Expr) (h : sort (flat a) = sort (flat b)) : denote ctx a = denote ctx b := by
-  have h := congrArg (denote ctx) h
+  have h := congr_arg (denote ctx) h
   simp [denote_flat, denote_sort] at h
   assumption
 

tests/lean/run/ac_rfl.lean

@@ -17,7 +17,7 @@ instance : IsNeutral HMul.hMul 1 := ⟨Nat.one_mul, Nat.mul_one⟩
 set_option linter.unusedVariables false in
 theorem le_ext : ∀ {x y : Nat} (h : ∀ z, z ≤ x ↔ z ≤ y), x = y
   | 0, 0, _ => rfl
-  | x+1, y+1, h => congrArg (· + 1) <| le_ext fun z => have := h (z + 1); by simp_all
+  | x+1, y+1, h => congr_arg (· + 1) <| le_ext fun z => have := h (z + 1); by simp_all
   | 0, y+1, h => have := h 1; by simp_all
   | x+1, 0, h => have := h 1; by simp_all
 

tests/lean/run/decClassical.lean

@@ -3,7 +3,7 @@ open Classical
 theorem ex : if (fun x => x + 1) = (fun x => x + 2) then False else True := by
   have : (fun x => x + 1) ≠ (fun x => x + 2) := by
     intro h
-    have : 1 = 2 := congrFun h 0
+    have : 1 = 2 := congr_fun h 0
     contradiction
   rw [if_neg this]
   exact True.intro

tests/lean/run/injective.lean

@@ -24,8 +24,8 @@ def foo : InjectiveFunction Bool (Nat → Nat) where
    | false, a => a
   inj a b h := by
     cases a
-    cases b; rfl; injection (congrFun h 0)
-    cases b; injection (congrFun h 0); rfl
+    cases b; rfl; injection (congr_fun h 0)
+    cases b; injection (congr_fun h 0); rfl
 
 theorem ex1 (x : Nat) : foo true x = x + 1 :=
   rfl

tests/lean/run/openTermTactic.lean

@@ -18,7 +18,7 @@ def h' (x : Nat) := succ x
 
 theorem ex (x y : Nat) (h : x = y) : x + 1 = y + 1 := by
   open Nat in show succ x = succ y
-  apply congrArg
+  apply congr_arg
   assumption
 
 

tests/lean/run/subst1.lean

@@ -16,10 +16,10 @@ theorem tst2 (x y z : Nat) : y = z → x = z + y → x = z + z := by
 
 def BV (n : Nat) : Type := { a : Array Bool // a.size = n }
 
-theorem tst3 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1.symm) w := by
+theorem tst3 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congr_arg BV h1.symm) w := by
 subst h1
 apply h2
 
-theorem tst4 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congrArg BV h1.symm) w := by
+theorem tst4 (n m : Nat) (v : BV n) (w : BV m) (h1 : n = m) (h2 : forall (v1 v2 : BV n), v1 = v2) : v = cast (congr_arg BV h1.symm) w := by
 subst n
 apply h2

tests/lean/simpZetaFalse.lean.expected.out

@@ -11,10 +11,10 @@ theorem ex1 : ∀ (x : Nat),
 fun x h =>
   Eq.mpr
     (id
-      (congrFun
-        (congrArg Eq
+      (congr_fun
+        (congr_arg Eq
           (let_congr (Eq.refl (x * x)) fun y =>
-            ite_congr (Eq.trans (congrFun (congrArg Eq h) x) (eq_self x)) (fun a => Eq.refl 1) fun a =>
+            ite_congr (Eq.trans (congr_fun (congr_arg Eq h) x) (eq_self x)) (fun a => Eq.refl 1) fun a =>
               Eq.refl (y + 1)))
         1))
     (of_eq_true (eq_self 1))
@@ -31,8 +31,8 @@ theorem ex2 : ∀ (x z : Nat),
         y) =
         z :=
 fun x z h h' =>
-  Eq.mpr (id (congrFun (congrArg Eq (let_val_congr (fun y => y) h)) z))
-    (of_eq_true (Eq.trans (congrArg (Eq x) h') (eq_self x)))
+  Eq.mpr (id (congr_fun (congr_arg Eq (let_val_congr (fun y => y) h)) z))
+    (of_eq_true (Eq.trans (congr_arg (Eq x) h') (eq_self x)))
 x z : Nat
 ⊢ (let α := Nat;
     fun x => 0 + x) =
@@ -48,5 +48,5 @@ theorem ex4 : ∀ (p : Prop),
       fun x => x = x) =
       fun z => p :=
 fun p h =>
-  Eq.mpr (id (congrFun (congrArg Eq (let_body_congr 10 fun n => funext fun x => eq_self x)) fun z => p))
-    (of_eq_true (Eq.trans (congrArg (Eq fun x => True) (funext fun z => eq_true h)) (eq_self fun x => True)))
+  Eq.mpr (id (congr_fun (congr_arg Eq (let_body_congr 10 fun n => funext fun x => eq_self x)) fun z => p))
+    (of_eq_true (Eq.trans (congr_arg (Eq fun x => True) (funext fun z => eq_true h)) (eq_self fun x => True)))

tests/playground/pge.lean

@@ -236,7 +236,7 @@ theorem proof_get_to_getD (r:ProofRecord nt) (p:Proof g s) (i:Fin p.size)  :
   p i = p.val.getD i.val r := by
   have isLt : i.val < Array.size p.val := i.isLt
   simp [Proof.get, Array.get, Array.getD, isLt ]
-  apply congrArg
+  apply congr_arg
   apply Fin.eq_of_val_eq
   trivial
 

tests/playground/som.lean

@@ -235,7 +235,7 @@ theorem Expr.toPoly_denote (ctx : Context α) (e : Expr) : e.toPoly.denote ctx =
   | sub a b => simp! [Poly.add_denote, *, sub_def, Poly.neg_denote, mul_one, mul_comm]
 
 theorem Expr.eq_of_toPoly_eq (ctx : Context α) (a b : Expr) (h : a.toPoly == b.toPoly) : a.denote ctx = b.denote ctx := by
-  have h := congrArg (Poly.denote ctx) (eq_of_beq h)
+  have h := congr_arg (Poly.denote ctx) (eq_of_beq h)
   simp [toPoly_denote] at h
   assumption