feat(Tactic/GCongr): add norm_num as a side goal discharger for gcongr

Archive/Imo/Imo2019Q4.lean

@@ -52,7 +52,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0)
   · gcongr
     · intro i hi
       simp only [mem_range] at hi
-      have : (2:ℤ) ^ i ≤ (2:ℤ) ^ n := by gcongr; norm_num
+      have : (2:ℤ) ^ i ≤ (2:ℤ) ^ n := by gcongr
       linarith
     · apply sub_le_self
       positivity
@@ -68,7 +68,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0)
     apply sum_le_sum_of_subset
     simpa using hn'
   calc 2 ^ ((n' + 1) * (n' + 1))
-      ≤ 2 ^ (n' * n' + 4 * n') := by gcongr <;> linarith
+      ≤ 2 ^ (n' * n' + 4 * n') := by gcongr; linarith
     _ = 2 ^ (n' * n') * (2 ^ 4) ^ n' := by rw [← pow_mul, ← pow_add]
     _ < A ! * (2 ^ 4) ^ n' := by gcongr
     _ = A ! * (15 + 1) ^ n' := rfl

Mathlib/Analysis/Distribution/SchwartzSpace.lean

@@ -538,7 +538,6 @@ theorem _root_.Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform_aux {f
     right
     exact ⟨N, hN, rfl.le⟩
   gcongr
-  · simp
   exact Finset.le_sup hN
 
 lemma _root_.Function.HasTemperateGrowth.of_fderiv {f : E → F}

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -415,7 +415,7 @@ lemma norm_iteratedFDeriv_fourierPowSMulRight
     · rw [← Nat.cast_pow, Nat.cast_le]
       calc n.descFactorial i ≤ n ^ i := Nat.descFactorial_le_pow _ _
       _ ≤ (n + 1) ^ i := by gcongr; omega
-      _ ≤ (n + 1) ^ k := by gcongr; exacts [le_add_self, Finset.mem_range_succ_iff.mp hi]
+      _ ≤ (n + 1) ^ k := by gcongr; exact Finset.mem_range_succ_iff.mp hi
     · exact hv _ (by omega) _ (by omega)
   _ = (2 * n + 2) ^ k * (‖L‖^n * C) := by
     simp only [← Finset.sum_mul, ← Nat.cast_sum, Nat.sum_range_choose, mul_one, ← mul_assoc,

Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

@@ -113,8 +113,7 @@ lemma eventually_zero_of_frequently_zero (hf : GrowsPolynomially f) (hf' : ∃
       case ineq =>
         rw [Set.left_mem_Icc]
         gcongr
-        · norm_num
-        · omega
+        omega
       simp only [ih, mul_zero, Set.Icc_self, Set.mem_singleton_iff] at hx
       refine hx ⟨?lb₁, ?ub₁⟩
       case lb₁ =>
@@ -213,7 +212,7 @@ lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) :
           refine hyp_ind (1/2 * z) ⟨?lb, ?ub⟩
           case lb =>
             calc max n₀ 2 ≤ ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ) ^ 1 * max n₀ 2 := by simp
-                        _ ≤ ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ) ^ n * max n₀ 2 := by gcongr; norm_num
+                        _ ≤ ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ) ^ n * max n₀ 2 := by gcongr
                         _ ≤ _ := by rw [mul_assoc]; gcongr; exact_mod_cast hz.1
           case ub =>
             have h₁ : (2 : ℝ)^n = ((1 : ℝ)/(2 : ℝ)) * (2 : ℝ)^(n+1) := by

Mathlib/Data/Real/Basic.lean

@@ -589,8 +589,7 @@ lemma mul_add_one_le_add_one_pow {a : ℝ} (ha : 0 ≤ a) (b : ℕ) : a * b + 1
         simp [mul_add, add_assoc, add_left_comm]
       _ ≤ (a + 1) ^ b * a + (a + 1) ^ b := by
         gcongr
-        · norm_num
-        · exact hb ha'
+        exact hb ha'
       _ = (a + 1) ^ (b + 1) := by simp [pow_succ, mul_add]
 
 end Real

Mathlib/Data/Real/Pi/Bounds.lean

@@ -43,7 +43,7 @@ theorem pi_lt_sqrtTwoAddSeries (n : ℕ) :
     calc
       π ≤ 4 := pi_le_four
       _ = 2 ^ (0 + 2) := by norm_num
-      _ ≤ 2 ^ (n + 2) := by gcongr <;> norm_num
+      _ ≤ 2 ^ (n + 2) := by gcongr; norm_num
   refine lt_of_lt_of_le this (le_of_eq ?_); rw [add_mul]; congr 1
   · ring
   simp only [show (4 : ℝ) = 2 ^ 2 by norm_num, ← pow_mul, div_div, ← pow_add]

Mathlib/NumberTheory/Bertrand.lean

@@ -118,7 +118,6 @@ theorem bertrand_main_inequality {n : ℕ} (n_large : 512 ≤ n) :
   · have n2_pos : 0 < 2 * n := by positivity
     exact mod_cast n2_pos
   · exact_mod_cast Real.nat_sqrt_le_real_sqrt
-  · norm_num1
   · exact cast_div_le.trans (by norm_cast)
 
 /-- A lemma that tells us that, in the case where Bertrand's postulate does not hold, the prime

Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean

@@ -298,7 +298,6 @@ theorem minkowskiBound_lt_boundOfDiscBdd : minkowskiBound K ↑1 < boundOfDiscBd
   · exact pow_le_one₀ (by positivity) (by norm_num)
   · rwa [← NNReal.coe_le_coe, coe_nnnorm, Int.norm_eq_abs, ← Int.cast_abs,
       NNReal.coe_natCast, ← Int.cast_natCast, Int.cast_le]
-  · exact one_le_two
   · exact rank_le_rankOfDiscrBdd hK
 
 include hK in
@@ -343,7 +342,6 @@ theorem finite_of_discr_bdd_of_isReal :
         rw [show max ↑(max (B : ℝ≥0) 1) (1 : ℝ) = max (B : ℝ) 1 by simp, val_eq_coe, NNReal.coe_mul,
           NNReal.coe_pow, NNReal.coe_max, NNReal.coe_one, NNReal.coe_natCast]
         gcongr
-        · exact le_max_right _ 1
         · exact rank_le_rankOfDiscrBdd hK₂
         · exact (Nat.choose_le_choose _ (rank_le_rankOfDiscrBdd hK₂)).trans
             (Nat.choose_le_middle _ _)
@@ -390,7 +388,6 @@ theorem finite_of_discr_bdd_of_isComplex :
         rw [val_eq_coe, NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_max, NNReal.coe_one,
           Real.coe_sqrt, NNReal.coe_add 1, NNReal.coe_one, NNReal.coe_pow]
         gcongr
-        · exact le_max_right _ 1
         · exact rank_le_rankOfDiscrBdd hK₂
         · rw [NNReal.coe_natCast, Nat.cast_le]
           exact (Nat.choose_le_choose _ (rank_le_rankOfDiscrBdd hK₂)).trans

Mathlib/Probability/Kernel/Disintegration/Density.lean

@@ -584,7 +584,7 @@ lemma setIntegral_density (hκν : fst κ ≤ ν) [IsFiniteKernel ν]
       ENNReal.toReal_sub_of_le (measure_mono (by intro x; simp)) (measure_ne_top _ _)]
     rw [eq_tsub_iff_add_eq_of_le, add_comm]
     · exact h
-    · gcongr <;> simp
+    · gcongr; simp
   | iUnion f hf_disj hf h_eq =>
     rw [integral_iUnion hf hf_disj (integrable_density hκν _ hs).integrableOn]
     simp_rw [h_eq]

Mathlib/Probability/Moments.lean

@@ -293,7 +293,7 @@ theorem measure_ge_le_exp_mul_mgf [IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t)
   · rw [ht_zero_eq.symm]
     simp only [neg_zero, zero_mul, exp_zero, mgf_zero', one_mul]
     gcongr
-    exacts [measure_ne_top _ _, Set.subset_univ _]
+    exact Set.subset_univ _
   calc
     (μ {ω | ε ≤ X ω}).toReal = (μ {ω | exp (t * ε) ≤ exp (t * X ω)}).toReal := by
       congr with ω

Mathlib/RingTheory/LaurentSeries.lean

@@ -912,7 +912,6 @@ theorem exists_Polynomial_intValuation_lt (F : K⟦X⟧) (η : ℤₘ₀ˣ) :
     apply lt_of_le_of_lt this
     rw [← mul_one (η : ℤₘ₀), mul_assoc, one_mul]
     gcongr
-    · exact zero_lt_iff.2 η.ne_zero
     rw [← WithZero.coe_one, coe_lt_coe, ofAdd_neg, Right.inv_lt_one_iff, ← ofAdd_zero,
       Multiplicative.ofAdd_lt]
     exact Int.zero_lt_one

Mathlib/Tactic/GCongr.lean

@@ -10,6 +10,7 @@ import Mathlib.Tactic.GCongr.CoreAttrs
 
 The core implementation of the `gcongr` ("generalized congruence") tactic is in the file
 `Tactic.GCongr.Core`. In this file we set it up for use across the library by listing
-`positivity` as a first-pass discharger for side goals (`gcongr_discharger`). -/
+`positivity` and `norm_num` as first-pass dischargers for side goals (`gcongr_discharger`). -/
 
 macro_rules | `(tactic| gcongr_discharger) => `(tactic| positivity)
+macro_rules | `(tactic| gcongr_discharger) => `(tactic| (norm_num; done))

Mathlib/Topology/Algebra/Polynomial.lean

@@ -184,8 +184,7 @@ theorem coeff_bdd_of_roots_le {B : ℝ} {d : ℕ} (f : F →+* K) {p : F[X]} (h1
       _ ≤ max B 1 ^ (p.natDegree - i) * p.natDegree.choose i := by gcongr; apply le_max_left
       _ ≤ max B 1 ^ d * p.natDegree.choose i := by
         gcongr
-        · apply le_max_right
-        · exact le_trans (Nat.sub_le _ _) h3
+        exact le_trans (Nat.sub_le _ _) h3
       _ ≤ max B 1 ^ d * d.choose (d / 2) := by
         gcongr; exact (i.choose_mono h3).trans (i.choose_le_middle d)
   · rw [eq_one_of_roots_le hB h1 h2 h4, Polynomial.map_one, coeff_one]

Mathlib/Topology/Algebra/Valued/ValuationTopology.lean

@@ -45,7 +45,7 @@ theorem subgroups_basis : RingSubgroupsBasis fun γ : Γ₀ˣ => (v.ltAddSubgrou
       simp only [ltAddSubgroup, AddSubgroup.coe_set_mk, mem_setOf_eq] at r_in s_in
       calc
         (v (r * s) : Γ₀) = v r * v s := Valuation.map_mul _ _ _
-        _ < γ₀ * γ₀ := by gcongr <;> exact zero_le'
+        _ < γ₀ * γ₀ := by gcongr
         _ ≤ γ := mod_cast h
     leftMul := by
       rintro x γ

MathlibTest/GCongr/inequalities.lean

@@ -145,14 +145,12 @@ example (A B C : ℝ) : |A + B| + C ≤ |A| + |B| + C := by gcongr ?_ + (A : ℝ
 
 example {n i : ℕ} (hi : i ∈ range n) : 2 ^ i ≤ 2 ^ n := by
   gcongr
-  · norm_num
-  · apply le_of_lt
-    simpa using hi
+  apply le_of_lt
+  simpa using hi
 
 example {n' : ℕ} (hn': 6 ≤ n') : 2 ^ ((n' + 1) * (n' + 1)) ≤ 2 ^ (n' * n' + 4 * n') := by
   gcongr
-  · norm_num
-  · linarith
+  linarith
 
 example {F : ℕ → ℕ} (le_sum: ∀ {N : ℕ}, 6 ≤ N → 15 ≤ F N) {n' : ℕ} (hn' : 6 ≤ n') :
     let A := F n';