feat: fix norm num with arguments (#6600)

`norm_num` was passing the wrong syntax node to `elabSimpArgs` when elaborating, which essentially had the effect of ignoring all arguments it was passed, i.e. `norm_num [add_comm]` would not try to commute addition in the simp step.
The fix itself is very simple (though not obvious to debug!), probably using TSyntax more would help avoid such issues in future.

Due to this bug many `norm_num [blah]` became `rw [blah]; norm_num` or similar, sometimes with porting notes, sometimes not, we fix these porting notes and other regressions during the port also.

Interestingly `cancel_denoms` uses `norm_num [<- mul_assoc]` internally, so  `cancel_denoms` also got stronger with this change.

Archive/Imo/Imo1962Q1.lean

@@ -43,7 +43,7 @@ abbrev ProblemPredicate' (c n : ℕ) : Prop :=
 theorem without_digits {n : ℕ} (h1 : ProblemPredicate n) : ∃ c : ℕ, ProblemPredicate' c n := by
   use n / 10
   cases' n with n
-  · have h2 : ¬ProblemPredicate 0 := by rw [ProblemPredicate]; norm_num
+  · have h2 : ¬ProblemPredicate 0 := by norm_num [ProblemPredicate]
     contradiction
   · rw [ProblemPredicate, digits_def' (by decide : 2 ≤ 10) n.succ_pos, List.headI, List.tail_cons,
       List.concat_eq_append] at h1
@@ -131,7 +131,7 @@ Now we combine these cases to show that 153846 is the smallest solution.
 
 
 theorem satisfied_by_153846 : ProblemPredicate 153846 := by
-  dsimp [ProblemPredicate]; norm_num
+  norm_num [ProblemPredicate]
 #align imo1962_q1.satisfied_by_153846 Imo1962Q1.satisfied_by_153846
 
 theorem no_smaller_solutions (n : ℕ) (h1 : ProblemPredicate n) : n ≥ 153846 := by

Archive/Imo/Imo1975Q1.lean

@@ -42,8 +42,8 @@ theorem imo1975_q1 :
   have hσy : ∑ i : ℕ in Finset.Icc 1 n, y i ^ 2 = ∑ i : ℕ in Finset.Icc 1 n, y (σ i) ^ 2 := by
     rw [← Equiv.Perm.sum_comp σ (Finset.Icc 1 n) _ hσ]
   -- let's cancel terms appearing on both sides
-  rw [hσy, add_le_add_iff_right, ← neg_le_neg_iff, neg_sub, neg_sub, sub_le_sub_iff_right]
-  simp_rw [mul_assoc, ← Finset.mul_sum]; norm_num
+  rw [hσy, add_le_add_iff_right, sub_le_sub_iff_left]
+  simp only [gt_iff_lt, Nat.lt_one_iff, mul_assoc, ← Finset.mul_sum, zero_lt_two, mul_le_mul_left]
   -- what's left to prove is a version of the rearrangement inequality
   apply MonovaryOn.sum_mul_comp_perm_le_sum_mul _ hσ
   -- finally we need to show that `x` and `y` 'vary' together on `[1, n]` and this is due to both of

Archive/Imo/Imo1981Q3.lean

@@ -203,8 +203,7 @@ numbers in this range, and thus provide the maximum of `specifiedSet`.
 -/
 theorem imo1981_q3 : IsGreatest (specifiedSet 1981) 3524578 := by
   have := fun h => @solution_greatest 1981 16 h 3524578
-  simp only [show fib (16 : ℕ) = 987 ∧ fib (16 + 1 : ℕ) = 1597 by norm_num [fib_add_two]] at this
-  apply_mod_cast this trivial trivial
-  rw [ProblemPredicate_iff]
-  norm_num
+  norm_num at this
+  apply this
+  norm_num [ProblemPredicate_iff]
 #align imo1981_q3 imo1981_q3

Archive/Imo/Imo2008Q4.lean

@@ -56,8 +56,8 @@ theorem imo2008_q4 (f : ℝ → ℝ) (H₁ : ∀ x > 0, f x > 0) :
   have h₀ : f 1 ≠ 0 := by specialize H₁ 1 zero_lt_one; exact ne_of_gt H₁
   have h₁ : f 1 = 1 := by
     specialize H₂ 1 1 1 1 zero_lt_one zero_lt_one zero_lt_one zero_lt_one rfl
-    norm_num at H₂
-    rw [← two_mul, ← two_mul, mul_div_mul_left (f 1 ^ 2) (f 1) two_ne_zero] at H₂
+    norm_num [← two_mul] at H₂
+    rw [mul_div_mul_left (f 1 ^ 2) (f 1) two_ne_zero] at H₂
     rwa [← (div_eq_iff h₀).mpr (sq (f 1))]
   have h₂ : ∀ x > 0, (f x - x) * (f x - 1 / x) = 0 := by
     intro x hx

Archive/Imo/Imo2019Q4.lean

@@ -97,9 +97,9 @@ theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
   · left; congr; norm_num at h; rw [factorial_eq_one] at h; apply antisymm h
     apply succ_le_of_lt hk
   -- n = 2
-  · right; congr; rw [prod_range_succ] at h; norm_num at h; norm_cast at h; rw [← factorial_inj]
+  · right; congr; norm_num [prod_range_succ] at h; norm_cast at h; rw [← factorial_inj]
     exact h; rw [h]; norm_num
-  all_goals exfalso; (repeat rw [prod_range_succ] at h); norm_num at h; norm_cast at h
+  all_goals exfalso; norm_num [prod_range_succ] at h; norm_cast at h
   -- n = 3
   · refine' monotone_factorial.ne_of_lt_of_lt_nat 5 _ _ _ h <;> norm_num
   -- n = 4

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -107,19 +107,16 @@ theorem real_roots_Phi_le : Fintype.card ((Φ ℚ a b).rootSet ℝ) ≤ 3 := by
   rw [← map_Phi a b (algebraMap ℤ ℚ), Φ, ← one_mul (X ^ 5), ← C_1]
   refine' (card_rootSet_le_derivative _).trans
     (Nat.succ_le_succ ((card_rootSet_le_derivative _).trans (Nat.succ_le_succ _)))
-  simp only [algebraMap_int_eq, map_one, one_mul, map_natCast, Polynomial.map_add,
-    Polynomial.map_sub, Polynomial.map_pow, map_X, Polynomial.map_mul, Polynomial.map_nat_cast,
-    map_add, map_sub, derivative_X_pow, Nat.cast_ofNat, ge_iff_le, Nat.succ_sub_succ_eq_sub,
-    tsub_zero, derivative_mul, derivative_nat_cast, zero_mul, derivative_X, mul_one, zero_add,
-    add_zero, derivative_C, sub_zero, map_C, eq_ratCast, ne_eq, Rat.cast_eq_zero, not_false_eq_true,
-    roots_C_mul, roots_pow, roots_X, Fintype.card_le_one_iff_subsingleton]
-  rw [← mul_assoc, ← _root_.map_mul, rootSet_C_mul_X_pow] <;>
+  suffices : (Polynomial.rootSet (C (20 : ℚ) * X ^ 3) ℝ).Subsingleton
+  · norm_num [Fintype.card_le_one_iff_subsingleton, ← mul_assoc] at *
+    exact this
+  rw [rootSet_C_mul_X_pow] <;>
   norm_num
 #align abel_ruffini.real_roots_Phi_le AbelRuffini.real_roots_Phi_le
 
 theorem real_roots_Phi_ge_aux (hab : b < a) :
     ∃ x y : ℝ, x ≠ y ∧ aeval x (Φ ℚ a b) = 0 ∧ aeval y (Φ ℚ a b) = 0 := by
-  let f := fun x : ℝ => aeval x (Φ ℚ a b)
+  let f : ℝ → ℝ := fun x : ℝ => aeval x (Φ ℚ a b)
   have hf : f = fun x : ℝ => x ^ 5 - a * x + b := by simp [Φ]
   have hc : ∀ s : Set ℝ, ContinuousOn f s := fun s => (Φ ℚ a b).continuousOn_aeval
   have ha : (1 : ℝ) ≤ a := Nat.one_le_cast.mpr (Nat.one_le_of_lt hab)
@@ -139,9 +136,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
     have hfa :=
       calc
         f (-a) = (a : ℝ) ^ 2 - (a : ℝ) ^ 5 + b := by
-            -- Porting note: was `norm_num [hf, ← sq]`
-            simp only [hf, mul_neg, ← sq, sub_neg_eq_add, Nat.cast_pow, add_left_inj]
-            rw [Odd.neg_pow (by norm_num), neg_add_eq_sub]
+          norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow]
         _ ≤ (a : ℝ) ^ 2 - (a : ℝ) ^ 3 + (a - 1) := by
           refine' add_le_add (sub_le_sub_left (pow_le_pow ha _) _) _ <;> linarith
         _ = -((a : ℝ) - 1) ^ 2 * (a + 1) := by ring
@@ -168,7 +163,7 @@ theorem complex_roots_Phi (h : (Φ ℚ a b).Separable) : Fintype.card ((Φ ℚ a
 theorem gal_Phi (hab : b < a) (h_irred : Irreducible (Φ ℚ a b)) :
     Bijective (galActionHom (Φ ℚ a b) ℂ) := by
   apply galActionHom_bijective_of_prime_degree' h_irred
-  · rw [natDegree_Phi]; norm_num
+  · norm_num [natDegree_Phi]
   · rw [complex_roots_Phi a b h_irred.separable, Nat.succ_le_succ_iff]
     exact (real_roots_Phi_le a b).trans (Nat.le_succ 3)
   · simp_rw [complex_roots_Phi a b h_irred.separable, Nat.succ_le_succ_iff]

Archive/Wiedijk100Theorems/AreaOfACircle.lean

@@ -133,8 +133,7 @@ theorem area_disc : volume (disc r) = NNReal.pi * r ^ 2 := by
       integral_eq_sub_of_hasDerivAt_of_le (neg_le_self r.2) hcont hderiv
         (continuous_const.mul hf).continuousOn.intervalIntegrable
     _ = NNReal.pi * (r : ℝ) ^ 2 := by
-      norm_num
-      simp [inv_mul_cancel hlt.ne', ← mul_div_assoc, mul_comm π]
+      norm_num [inv_mul_cancel hlt.ne', ← mul_div_assoc, mul_comm π]
 #align theorems_100.area_disc Theorems100.area_disc
 
 end Theorems100

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -137,7 +137,7 @@ def unitCube : Cube n :=
 
 @[simp]
 theorem side_unitCube {j : Fin n} : unitCube.side j = Ico 0 1 := by
-  rw [unitCube, side]; norm_num
+  norm_num [unitCube, side]
 #align theorems_100.«82».cube.side_unit_cube Theorems100.«82».Cube.side_unitCube
 
 end Cube
@@ -254,7 +254,7 @@ theorem valley_unitCube [Nontrivial ι] (h : Correct cs) : Valley cs unitCube :=
     intro h0 hv
     have : v ∈ (unitCube : Cube (n + 1)).toSet := by
       dsimp only [toSet, unitCube, mem_setOf_eq]
-      rw [forall_fin_succ, h0]; constructor; rw [side, unitCube]; norm_num; exact hv
+      rw [forall_fin_succ, h0]; constructor; norm_num [side, unitCube]; exact hv
     rw [← h.2, mem_iUnion] at this; rcases this with ⟨i, hi⟩
     use i
     constructor

Mathlib/Algebra/PUnitInstances.lean

@@ -48,7 +48,8 @@ theorem one_eq : (1 : PUnit) = unit :=
 #align punit.one_eq PUnit.one_eq
 #align punit.zero_eq PUnit.zero_eq
 
-@[to_additive (attr := simp)]
+-- note simp can prove this when the Boolean ring structure is introduced
+@[to_additive]
 theorem mul_eq : x * y = unit :=
   rfl
 #align punit.mul_eq PUnit.mul_eq

Mathlib/Algebra/Ring/BooleanRing.lean

@@ -56,14 +56,12 @@ variable [BooleanRing α] (a b : α)
 instance : IsIdempotent α (· * ·) :=
   ⟨BooleanRing.mul_self⟩
 
--- Porting note: simpNF linter complains. This causes lemmas in other files not to be in simpNF
--- @[simp]
+@[simp]
 theorem mul_self : a * a = a :=
   BooleanRing.mul_self _
 #align mul_self mul_self
 
--- Porting note: simpNF linter complains. This causes lemmas in other files not to be in simpNF
--- @[simp]
+@[simp]
 theorem add_self : a + a = 0 := by
   have : a + a = a + a + (a + a) :=
     calc
@@ -73,8 +71,7 @@ theorem add_self : a + a = 0 := by
   rwa [self_eq_add_left] at this
 #align add_self add_self
 
--- Porting note: simpNF linter complains. This causes lemmas in other files not to be in simpNF
--- @[simp]
+@[simp]
 theorem neg_eq : -a = a :=
   calc
     -a = -a + 0 := by rw [add_zero]
@@ -88,8 +85,7 @@ theorem add_eq_zero' : a + b = 0 ↔ a = b :=
     _ ↔ a = b := by rw [neg_eq]
 #align add_eq_zero' add_eq_zero'
 
--- Porting note: simpNF linter complains. This causes lemmas in other files not to be in simpNF
--- @[simp]
+@[simp]
 theorem mul_add_mul : a * b + b * a = 0 := by
   have : a + b = a + b + (a * b + b * a) :=
     calc
@@ -100,8 +96,7 @@ theorem mul_add_mul : a * b + b * a = 0 := by
   rwa [self_eq_add_right] at this
 #align mul_add_mul mul_add_mul
 
--- Porting note: simpNF linter complains. This causes lemmas in other files not to be in simpNF
--- @[simp]
+@[simp]
 theorem sub_eq_add : a - b = a + b := by rw [sub_eq_add_neg, add_right_inj, neg_eq]
 #align sub_eq_add sub_eq_add
 
@@ -263,7 +258,7 @@ def toBooleanAlgebra : BooleanAlgebra α :=
       change
         1 + (a + (1 + a) + a * (1 + a)) + 1 * (a + (1 + a) + a * (1 + a)) =
           a + (1 + a) + a * (1 + a)
-      norm_num [mul_add, mul_self]
+      norm_num [mul_add, mul_self, add_self]
       rw [← add_assoc, add_self] }
 #align boolean_ring.to_boolean_algebra BooleanRing.toBooleanAlgebra
 

Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

@@ -50,9 +50,7 @@ theorem continuous_reflTransSymmAux : Continuous reflTransSymmAux := by
   · continuity
   · continuity
   intro x hx
-  -- Porting note: norm_num ignores arguments.
-  rw [hx, mul_assoc]
-  norm_num
+  norm_num [hx, mul_assoc]
 #align path.homotopy.continuous_refl_trans_symm_aux Path.Homotopy.continuous_reflTransSymmAux
 
 theorem reflTransSymmAux_mem_I (x : I × I) : reflTransSymmAux x ∈ I := by
@@ -100,9 +98,7 @@ def reflTransSymm (p : Path x₀ x₁) : Homotopy (Path.refl x₀) (p.trans p.sy
       · simp only [Set.Icc.coe_one, one_mul, coe_mk_mk, Function.comp_apply]
         congr 1
         ext
-        -- Porting note: norm_num ignores arguments.
-        simp [sub_sub_eq_add_sub]
-        norm_num
+        norm_num [sub_sub_eq_add_sub]
       · rw [unitInterval.two_mul_sub_one_mem_iff]
         exact ⟨(not_le.1 h).le, unitInterval.le_one x⟩
   prop' t x hx := by
@@ -112,9 +108,7 @@ def reflTransSymm (p : Path x₀ x₁) : Homotopy (Path.refl x₀) (p.trans p.sy
     | inl hx
     | inr hx =>
       rw [hx]
-      simp only [reflTransSymmAux, Set.Icc.coe_zero, Set.Icc.coe_one, one_div, mul_one,
-        inv_nonneg, mul_zero, sub_zero, sub_self, Path.source, Path.target, and_self]
-      norm_num
+      norm_num [reflTransSymmAux]
 #align path.homotopy.refl_trans_symm Path.Homotopy.reflTransSymm
 
 /-- For any path `p` from `x₀` to `x₁`, we have a homotopy from the constant path based at `x₁` to
@@ -137,7 +131,6 @@ theorem continuous_transReflReparamAux : Continuous transReflReparamAux := by
   refine' continuous_if_le _ _ (Continuous.continuousOn _) (Continuous.continuousOn _) _ <;>
     [continuity; continuity; continuity; continuity; skip]
   intro x hx
-  -- Porting note: norm_num ignores arguments.
   simp [hx]
 #align path.homotopy.continuous_trans_refl_reparam_aux Path.Homotopy.continuous_transReflReparamAux
 
@@ -148,15 +141,11 @@ set_option linter.uppercaseLean3 false in
 #align path.homotopy.trans_refl_reparam_aux_mem_I Path.Homotopy.transReflReparamAux_mem_I
 
 theorem transReflReparamAux_zero : transReflReparamAux 0 = 0 := by
-  -- Porting note: norm_num ignores arguments.
-  simp [transReflReparamAux]
-  norm_num
+  norm_num [transReflReparamAux]
 #align path.homotopy.trans_refl_reparam_aux_zero Path.Homotopy.transReflReparamAux_zero
 
 theorem transReflReparamAux_one : transReflReparamAux 1 = 1 := by
-  -- Porting note: norm_num ignores arguments.
-  simp [transReflReparamAux]
-  norm_num
+  norm_num [transReflReparamAux]
 #align path.homotopy.trans_refl_reparam_aux_one Path.Homotopy.transReflReparamAux_one
 
 theorem trans_refl_reparam (p : Path x₀ x₁) :
@@ -203,9 +192,7 @@ theorem continuous_transAssocReparamAux : Continuous transAssocReparamAux := by
     [continuity; continuity; continuity; continuity; continuity; continuity; continuity; skip;
       skip] <;>
     · intro x hx
-      -- Porting note: norm_num ignores arguments.
-      simp [hx]
-      norm_num
+      norm_num [hx]
 #align path.homotopy.continuous_trans_assoc_reparam_aux Path.Homotopy.continuous_transAssocReparamAux
 
 theorem transAssocReparamAux_mem_I (t : I) : transAssocReparamAux t ∈ I := by
@@ -215,15 +202,11 @@ set_option linter.uppercaseLean3 false in
 #align path.homotopy.trans_assoc_reparam_aux_mem_I Path.Homotopy.transAssocReparamAux_mem_I
 
 theorem transAssocReparamAux_zero : transAssocReparamAux 0 = 0 := by
-  -- Porting note: norm_num ignores arguments.
-  simp [transAssocReparamAux]
-  norm_num
+  norm_num [transAssocReparamAux]
 #align path.homotopy.trans_assoc_reparam_aux_zero Path.Homotopy.transAssocReparamAux_zero
 
 theorem transAssocReparamAux_one : transAssocReparamAux 1 = 1 := by
-  -- Porting note: norm_num ignores arguments.
-  simp [transAssocReparamAux]
-  norm_num
+  norm_num [transAssocReparamAux]
 #align path.homotopy.trans_assoc_reparam_aux_one Path.Homotopy.transAssocReparamAux_one
 
 theorem trans_assoc_reparam {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) :

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -269,8 +269,7 @@ theorem inner_self_ne_zero {x : F} : ⟪x, x⟫ ≠ 0 ↔ x ≠ 0 :=
 #align inner_product_space.core.inner_self_ne_zero InnerProductSpace.Core.inner_self_ne_zero
 
 theorem inner_self_ofReal_re (x : F) : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ := by
-  rw [ext_iff, inner_self_im]
-  norm_num
+  norm_num [ext_iff, inner_self_im]
 set_option linter.uppercaseLean3 false in
 #align inner_product_space.core.inner_self_re_to_K InnerProductSpace.Core.inner_self_ofReal_re
 

Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

@@ -133,7 +133,7 @@ theorem log_inv_eq_ite (x : ℂ) : log x⁻¹ = if x.arg = π then -conj (log x)
 theorem log_inv (x : ℂ) (hx : x.arg ≠ π) : log x⁻¹ = -log x := by rw [log_inv_eq_ite, if_neg hx]
 #align complex.log_inv Complex.log_inv
 
-theorem two_pi_I_ne_zero : (2 * π * I : ℂ) ≠ 0 := by norm_num; simp [Real.pi_ne_zero, I_ne_zero]
+theorem two_pi_I_ne_zero : (2 * π * I : ℂ) ≠ 0 := by norm_num [Real.pi_ne_zero, I_ne_zero]
 set_option linter.uppercaseLean3 false in
 #align complex.two_pi_I_ne_zero Complex.two_pi_I_ne_zero
 

Mathlib/Analysis/SpecialFunctions/Integrals.lean

@@ -452,7 +452,7 @@ theorem integral_one_div_of_neg (ha : a < 0) (hb : b < 0) :
 @[simp]
 theorem integral_exp : ∫ x in a..b, exp x = exp b - exp a := by
   rw [integral_deriv_eq_sub']
-  · norm_num
+  · simp
   · exact fun _ _ => differentiableAt_exp
   · exact continuousOn_exp
 #align integral_exp integral_exp
@@ -679,7 +679,7 @@ theorem integral_sin_pow_even :
 theorem integral_sin_pow_pos : 0 < ∫ x in (0)..π, sin x ^ n := by
   rcases even_or_odd' n with ⟨k, rfl | rfl⟩ <;>
   simp only [integral_sin_pow_even, integral_sin_pow_odd] <;>
-  refine' mul_pos (by norm_num <;> exact pi_pos) (prod_pos fun n _ => div_pos _ _) <;>
+  refine' mul_pos (by norm_num [pi_pos]) (prod_pos fun n _ => div_pos _ _) <;>
   norm_cast <;>
   linarith
 #align integral_sin_pow_pos integral_sin_pow_pos

Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean

@@ -50,8 +50,7 @@ protected def coe (r : ℝ) : Angle := QuotientAddGroup.mk r
 instance : Coe ℝ Angle := ⟨Angle.coe⟩
 
 instance : CircularOrder Real.Angle :=
-  -- Porting note: `norm_num` didn't use `pi_pos` when supplied
-  @AddCircle.instCircularOrderAddCircle _ _ _ _ _ ⟨by norm_num; exact pi_pos⟩ _
+  @AddCircle.instCircularOrderAddCircle _ _ _ _ _ ⟨by norm_num [pi_pos]⟩ _
 
 @[continuity]
 theorem continuous_coe : Continuous ((↑) : ℝ → Angle) :=

Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

@@ -65,7 +65,7 @@ theorem sin_gt_sub_cube {x : ℝ} (h : 0 < x) (h' : x ≤ 1) : x - x ^ 3 / 4 < s
   have := neg_le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])
   rw [le_sub_iff_add_le, hx] at this
   refine' lt_of_lt_of_le _ this
-  have : x ^ 3 / ↑4 - x ^ 3 / ↑6 = x ^ 3 * 12⁻¹ := by ring
+  have : x ^ 3 / ↑4 - x ^ 3 / ↑6 = x ^ 3 * 12⁻¹ := by norm_num [div_eq_mul_inv, ← mul_sub]
   rw [add_comm, sub_add, sub_neg_eq_add, sub_lt_sub_iff_left, ← lt_sub_iff_add_lt', this]
   refine' mul_lt_mul' _ (by norm_num) (by norm_num) (pow_pos h 3)
   apply pow_le_pow_of_le_one h.le h'

Mathlib/Combinatorics/Catalan.lean

@@ -140,10 +140,12 @@ theorem succ_mul_catalan_eq_centralBinom (n : ℕ) : (n + 1) * catalan n = n.cen
   (Nat.eq_mul_of_div_eq_right n.succ_dvd_centralBinom (catalan_eq_centralBinom_div n).symm).symm
 #align succ_mul_catalan_eq_central_binom succ_mul_catalan_eq_centralBinom
 
-theorem catalan_two : catalan 2 = 2 := by unfold catalan; rfl
+theorem catalan_two : catalan 2 = 2 := by
+  norm_num [catalan_eq_centralBinom_div, Nat.centralBinom, Nat.choose]
 #align catalan_two catalan_two
 
-theorem catalan_three : catalan 3 = 5 := by unfold catalan; rfl
+theorem catalan_three : catalan 3 = 5 := by
+  norm_num [catalan_eq_centralBinom_div, Nat.centralBinom, Nat.choose]
 #align catalan_three catalan_three
 
 namespace Tree

Mathlib/Data/Complex/Exponential.lean

@@ -1940,14 +1940,7 @@ theorem exp_bound_div_one_sub_of_interval' {x : ℝ} (h1 : 0 < x) (h2 : x < 1) :
       -- Porting note: was `norm_num [Finset.sum] <;> nlinarith`
       -- This proof should be restored after the norm_num plugin for big operators is ported.
       -- (It may also need the positivity extensions in #3907.)
-      rw [Finset.sum, range_val]
-      nth_rw 1 [← two_add_one_eq_three]
-      rw [← Nat.succ_eq_add_one, Multiset.range_succ, Multiset.map_cons, Multiset.sum_cons]
-      nth_rw 3 [← one_add_one_eq_two]
-      rw [← Nat.succ_eq_add_one, Multiset.range_succ, Multiset.map_cons, Multiset.sum_cons]
-      nth_rw 3 [← zero_add 1]
-      rw [← Nat.succ_eq_add_one, Multiset.range_succ, Multiset.map_cons, Multiset.sum_cons]
-      rw [Multiset.range_zero, Multiset.map_zero, Multiset.sum_zero]
+      repeat erw [Finset.sum_range_succ]
       norm_num
       nlinarith
     _ < 1 / (1 - x) := by rw [lt_div_iff] <;> nlinarith

Mathlib/Data/Nat/Choose/Sum.lean

@@ -125,7 +125,7 @@ theorem choose_middle_le_pow (n : ℕ) : choose (2 * n + 1) n ≤ 4 ^ n := by
 theorem four_pow_le_two_mul_add_one_mul_central_binom (n : ℕ) :
     4 ^ n ≤ (2 * n + 1) * choose (2 * n) n :=
   calc
-    4 ^ n = (1 + 1) ^ (2 * n) := by simp only [pow_mul, one_add_one_eq_two]; rfl
+    4 ^ n = (1 + 1) ^ (2 * n) := by norm_num [pow_mul]
     _ = ∑ m in range (2 * n + 1), choose (2 * n) m := by simp [add_pow]
     _ ≤ ∑ m in range (2 * n + 1), choose (2 * n) (2 * n / 2) := by gcongr; apply choose_le_middle
     _ = (2 * n + 1) * choose (2 * n) n := by simp

Mathlib/Data/Nat/Parity.lean

@@ -42,7 +42,7 @@ theorem even_iff : Even n ↔ n % 2 = 0 :=
 instance : DecidablePred (Even : ℕ → Prop) := fun _ => decidable_of_iff _ even_iff.symm
 
 theorem odd_iff : Odd n ↔ n % 2 = 1 :=
-  ⟨fun ⟨m, hm⟩ => by rw [hm, add_mod, mul_mod_right]; rfl,
+  ⟨fun ⟨m, hm⟩ => by norm_num [hm, add_mod],
     fun h => ⟨n / 2, (mod_add_div n 2).symm.trans (by rw [h, add_comm])⟩⟩
 #align nat.odd_iff Nat.odd_iff