feat(*): add simp/gcongr attrs and use them (#27718)

Also weaken assumptions of `Polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd`.



Co-authored-by: Yury Kudryashov <162619279+yury-harmonic@users.noreply.github.com>

Author: yury-harmonic

Mathlib/Algebra/Divisibility/Basic.lean

@@ -96,6 +96,12 @@ Schreier domain if it is moreover integrally closed. -/
 theorem exists_dvd_and_dvd_of_dvd_mul [DecompositionMonoid α] {b c a : α} (H : a ∣ b * c) :
     ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂ := DecompositionMonoid.primal a H
 
+@[gcongr]
+theorem mul_dvd_mul_left (a : α) (h : b ∣ c) : a * b ∣ a * c := by
+  obtain ⟨d, rfl⟩ := h
+  use d
+  rw [mul_assoc]
+
 end Semigroup
 
 section Monoid
@@ -117,6 +123,7 @@ theorem dvd_of_eq (h : a = b) : a ∣ b := by rw [h]
 
 alias Eq.dvd := dvd_of_eq
 
+@[gcongr]
 lemma pow_dvd_pow (a : α) (h : m ≤ n) : a ^ m ∣ a ^ n :=
   ⟨a ^ (n - m), by rw [← pow_add, Nat.add_comm, Nat.sub_add_cancel h]⟩
 
@@ -128,11 +135,6 @@ alias Dvd.dvd.pow := dvd_pow
 
 lemma dvd_pow_self (a : α) {n : ℕ} (hn : n ≠ 0) : a ∣ a ^ n := dvd_rfl.pow hn
 
-theorem mul_dvd_mul_left (a : α) (h : b ∣ c) : a * b ∣ a * c := by
-  obtain ⟨d, rfl⟩ := h
-  use d
-  rw [mul_assoc]
-
 end Monoid
 
 section CommSemigroup
@@ -166,6 +168,7 @@ alias Dvd.dvd.mul_left := dvd_mul_of_dvd_right
 
 attribute [local simp] mul_assoc mul_comm mul_left_comm
 
+@[gcongr]
 theorem mul_dvd_mul : ∀ {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
   | a, _, c, _, ⟨e, rfl⟩, ⟨f, rfl⟩ => ⟨e * f, by simp⟩
 
@@ -176,21 +179,28 @@ theorem dvd_mul [DecompositionMonoid α] {k m n : α} :
     k ∣ m * n ↔ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂ := by
   refine ⟨exists_dvd_and_dvd_of_dvd_mul, ?_⟩
   rintro ⟨d₁, d₂, hy, hz, rfl⟩
-  exact mul_dvd_mul hy hz
+  gcongr
 
 end CommSemigroup
 
 section CommMonoid
 
 variable [CommMonoid α] {a b : α}
 
+@[gcongr]
 theorem mul_dvd_mul_right (h : a ∣ b) (c : α) : a * c ∣ b * c :=
   mul_dvd_mul h (dvd_refl c)
 
-theorem pow_dvd_pow_of_dvd (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n
-  | 0 => by rw [pow_zero, pow_zero]
-  | n + 1 => by
+@[gcongr]
+theorem pow_dvd_pow_of_dvd (h : a ∣ b) (n : ℕ) : a ^ n ∣ b ^ n := by
+  induction n with
+  | zero => simp
+  | succ =>
     rw [pow_succ, pow_succ]
-    exact mul_dvd_mul (pow_dvd_pow_of_dvd h n) h
+    gcongr
+
+@[gcongr]
+lemma pow_dvd_pow_of_dvd_of_le {m n : ℕ} (hab : a ∣ b) (hmn : m ≤ n) : a ^ m ∣ b ^ n := by
+  trans (a ^ n) <;> gcongr
 
 end CommMonoid

Mathlib/Algebra/GCDMonoid/Nat.lean

@@ -146,7 +146,7 @@ def associatesIntEquivNat : Associates ℤ ≃ ℕ := by
   refine ⟨(·.out.natAbs), (Associates.mk ·), ?_, fun n ↦ ?_⟩
   · refine Associates.forall_associated.2 fun a ↦ ?_
     refine Associates.mk_eq_mk_iff_associated.2 <| Associated.symm <| ⟨normUnit a, ?_⟩
-    simp [Int.abs_eq_normalize, normalize_apply]
+    simp [Int.natCast_natAbs, Int.abs_eq_normalize, normalize_apply]
   · dsimp only [Associates.out_mk]
     rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_natCast]
 

Mathlib/Algebra/Order/Group/Unbundled/Int.lean

@@ -37,7 +37,7 @@ theorem abs_eq_natAbs : ∀ a : ℤ, |a| = natAbs a
   | (n : ℕ) => abs_of_nonneg <| ofNat_zero_le _
   | -[_+1] => abs_of_nonpos <| le_of_lt <| negSucc_lt_zero _
 
-@[simp, norm_cast] lemma natCast_natAbs (n : ℤ) : (n.natAbs : ℤ) = |n| := n.abs_eq_natAbs.symm
+@[norm_cast] lemma natCast_natAbs (n : ℤ) : (n.natAbs : ℤ) = |n| := n.abs_eq_natAbs.symm
 
 theorem natAbs_abs (a : ℤ) : natAbs |a| = natAbs a := by rw [abs_eq_natAbs]; rfl
 

Mathlib/Algebra/Order/Ring/Int.lean

@@ -43,6 +43,7 @@ instance instIsStrictOrderedRing : IsStrictOrderedRing ℤ := .of_mul_pos @Int.m
 lemma isCompl_even_odd : IsCompl { n : ℤ | Even n } { n | Odd n } := by
   simp [← not_even_iff_odd, ← Set.compl_setOf, isCompl_compl]
 
+@[simp]
 lemma _root_.Nat.cast_natAbs {α : Type*} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = |n| := by
   rw [← natCast_natAbs, Int.cast_natCast]
 

Mathlib/Combinatorics/SimpleGraph/Finite.lean

@@ -71,12 +71,11 @@ theorem edgeFinset_subset_edgeFinset : G₁.edgeFinset ⊆ G₂.edgeFinset ↔ G
 
 theorem edgeFinset_ssubset_edgeFinset : G₁.edgeFinset ⊂ G₂.edgeFinset ↔ G₁ < G₂ := by simp
 
-@[gcongr] alias ⟨_, edgeFinset_mono⟩ := edgeFinset_subset_edgeFinset
+@[mono, gcongr] alias ⟨_, edgeFinset_mono⟩ := edgeFinset_subset_edgeFinset
 
+@[mono, gcongr]
 alias ⟨_, edgeFinset_strict_mono⟩ := edgeFinset_ssubset_edgeFinset
 
-attribute [mono] edgeFinset_mono edgeFinset_strict_mono
-
 @[simp]
 theorem edgeFinset_bot : (⊥ : SimpleGraph V).edgeFinset = ∅ := by simp [edgeFinset]
 

Mathlib/Data/Finset/Card.lean

@@ -292,6 +292,7 @@ theorem card_filter_eq_zero_iff {p : α → Prop} [DecidablePred p] :
     #(s.filter p) = 0 ↔ ∀ x ∈ s, ¬ p x := by
   rw [card_eq_zero, filter_eq_empty_iff]
 
+@[gcongr]
 nonrec lemma card_lt_card (h : s ⊂ t) : #s < #t := card_lt_card <| val_lt_iff.2 h
 
 lemma card_strictMono : StrictMono (card : Finset α → ℕ) := fun _ _ ↦ card_lt_card

Mathlib/Data/Int/Log.lean

@@ -142,17 +142,17 @@ theorem log_zpow {b : ℕ} (hb : 1 < b) (z : ℤ) : log b (b ^ z : R) = z := by
       neg_nonpos.2 (Int.natCast_nonneg _)),
       zpow_neg, inv_inv, zpow_natCast, ← Nat.cast_pow, Nat.ceil_natCast, Nat.clog_pow _ _ hb]
 
-@[mono]
+@[mono, gcongr]
 theorem log_mono_right {b : ℕ} {r₁ r₂ : R} (h₀ : 0 < r₁) (h : r₁ ≤ r₂) : log b r₁ ≤ log b r₂ := by
   rcases le_total r₁ 1 with h₁ | h₁ <;> rcases le_total r₂ 1 with h₂ | h₂
-  · rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂, neg_le_neg_iff, Int.ofNat_le]
-    exact Nat.clog_mono_right _ (Nat.ceil_mono <| inv_anti₀ h₀ h)
+  · rw [log_of_right_le_one _ h₁, log_of_right_le_one _ h₂]
+    gcongr
   · rw [log_of_right_le_one _ h₁, log_of_one_le_right _ h₂]
     exact (neg_nonpos.mpr (Int.natCast_nonneg _)).trans (Int.natCast_nonneg _)
   · obtain rfl := le_antisymm h (h₂.trans h₁)
     rfl
-  · rw [log_of_one_le_right _ h₁, log_of_one_le_right _ h₂, Int.ofNat_le]
-    exact Nat.log_mono_right (Nat.floor_mono h)
+  · rw [log_of_one_le_right _ h₁, log_of_one_le_right _ h₂]
+    gcongr
 
 variable (R) in
 /-- Over suitable subtypes, `zpow` and `Int.log` form a galois coinsertion -/
@@ -269,7 +269,8 @@ theorem clog_zpow {b : ℕ} (hb : 1 < b) (z : ℤ) : clog b (b ^ z : R) = z := b
 theorem clog_mono_right {b : ℕ} {r₁ r₂ : R} (h₀ : 0 < r₁) (h : r₁ ≤ r₂) :
     clog b r₁ ≤ clog b r₂ := by
   rw [← neg_log_inv_eq_clog, ← neg_log_inv_eq_clog, neg_le_neg_iff]
-  exact log_mono_right (inv_pos.mpr <| h₀.trans_le h) (inv_anti₀ h₀ h)
+  gcongr
+  exact inv_pos.2 (h₀.trans_le h)
 
 variable (R) in
 /-- Over suitable subtypes, `Int.clog` and `zpow` form a galois insertion -/

Mathlib/Data/Int/ModEq.lean

@@ -62,6 +62,7 @@ end ModEq
 
 theorem modEq_comm : a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n] := ⟨ModEq.symm, ModEq.symm⟩
 
+@[simp]
 theorem natCast_modEq_iff {a b n : ℕ} : a ≡ b [ZMOD n] ↔ a ≡ b [MOD n] := by
   unfold ModEq Nat.ModEq; rw [← Int.ofNat_inj]; simp
 

Mathlib/Data/Multiset/Defs.lean

@@ -222,12 +222,14 @@ def card : Multiset α → ℕ := Quot.lift length fun _l₁ _l₂ => Perm.lengt
 theorem coe_card (l : List α) : card (l : Multiset α) = length l :=
   rfl
 
+@[gcongr]
 theorem card_le_card {s t : Multiset α} (h : s ≤ t) : card s ≤ card t :=
   leInductionOn h Sublist.length_le
 
 theorem eq_of_le_of_card_le {s t : Multiset α} (h : s ≤ t) : card t ≤ card s → s = t :=
   leInductionOn h fun s h₂ => congr_arg _ <| s.eq_of_length_le h₂
 
+@[gcongr]
 theorem card_lt_card {s t : Multiset α} (h : s < t) : card s < card t :=
   lt_of_not_ge fun h₂ => _root_.ne_of_lt h <| eq_of_le_of_card_le (le_of_lt h) h₂
 

Mathlib/Data/Nat/Log.lean

@@ -146,6 +146,7 @@ theorem log_eq_of_pow_le_of_lt_pow {b m n : ℕ} (h₁ : b ^ m ≤ n) (h₂ : n
     exact log_of_lt h₂
   · exact (log_eq_iff (Or.inl hm)).2 ⟨h₁, h₂⟩
 
+@[simp]
 theorem log_pow {b : ℕ} (hb : 1 < b) (x : ℕ) : log b (b ^ x) = x :=
   log_eq_of_pow_le_of_lt_pow le_rfl (Nat.pow_lt_pow_right hb x.lt_succ_self)
 
@@ -156,6 +157,7 @@ theorem log_eq_one_iff {b n : ℕ} : log b n = 1 ↔ n < b * b ∧ 1 < b ∧ b 
   log_eq_one_iff'.trans
     ⟨fun h => ⟨h.2, lt_mul_self_iff.1 (h.1.trans_lt h.2), h.1⟩, fun h => ⟨h.2.2, h.1⟩⟩
 
+@[simp]
 theorem log_mul_base {b n : ℕ} (hb : 1 < b) (hn : n ≠ 0) : log b (n * b) = log b n + 1 := by
   apply log_eq_of_pow_le_of_lt_pow <;> rw [pow_succ', Nat.mul_comm b]
   exacts [Nat.mul_le_mul_right _ (pow_log_le_self _ hn),
@@ -172,7 +174,7 @@ theorem log_monotone {b : ℕ} : Monotone (log b) := by
     exact zero_le _
   · exact le_log_of_pow_le hb (pow_log_le_add_one _ _)
 
-@[mono]
+@[mono, gcongr]
 theorem log_mono_right {b n m : ℕ} (h : n ≤ m) : log b n ≤ log b m :=
   log_monotone h
 
@@ -190,7 +192,7 @@ theorem log_eq_log_succ_iff {b n : ℕ} (hb : 1 < b) (hn : n ≠ 0) :
   simp only [le_antisymm_iff, and_iff_right_iff_imp]
   exact fun  _ ↦ log_monotone (le_add_right n 1)
 
-@[mono]
+@[mono, gcongr]
 theorem log_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : log b n ≤ log c n := by
   rcases eq_or_ne n 0 with (rfl | hn); · rw [log_zero_right, log_zero_right]
   apply le_log_of_pow_le hc
@@ -201,6 +203,12 @@ theorem log_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : log b n ≤ lo
 theorem log_antitone_left {n : ℕ} : AntitoneOn (fun b => log b n) (Set.Ioi 1) := fun _ hc _ _ hb =>
   log_anti_left (Set.mem_Iio.1 hc) hb
 
+@[gcongr]
+theorem log_mono {b c m n : ℕ} (hc : 1 < c) (hb : c ≤ b) (hmn : m ≤ n) :
+    log b m ≤ log c n := by
+  trans log c m <;> gcongr
+  assumption
+
 @[simp]
 theorem log_div_base (b n : ℕ) : log b (n / b) = log b n - 1 := by
   rcases le_or_gt b 1 with hb | hb
@@ -293,6 +301,7 @@ theorem le_pow_iff_clog_le {b : ℕ} (hb : 1 < b) {x y : ℕ} : x ≤ b ^ y ↔
 theorem pow_lt_iff_lt_clog {b : ℕ} (hb : 1 < b) {x y : ℕ} : b ^ y < x ↔ y < clog b x :=
   lt_iff_lt_of_le_iff_le (le_pow_iff_clog_le hb)
 
+@[simp]
 theorem clog_pow (b x : ℕ) (hb : 1 < b) : clog b (b ^ x) = x :=
   eq_of_forall_ge_iff fun z ↦ by rw [← le_pow_iff_clog_le hb, Nat.pow_le_pow_iff_right hb]
 
@@ -304,15 +313,15 @@ theorem pow_pred_clog_lt_self {b : ℕ} (hb : 1 < b) {x : ℕ} (hx : 1 < x) :
 theorem le_pow_clog {b : ℕ} (hb : 1 < b) (x : ℕ) : x ≤ b ^ clog b x :=
   (le_pow_iff_clog_le hb).2 le_rfl
 
-@[mono]
+@[mono, gcongr]
 theorem clog_mono_right (b : ℕ) {n m : ℕ} (h : n ≤ m) : clog b n ≤ clog b m := by
   rcases le_or_gt b 1 with hb | hb
   · rw [clog_of_left_le_one hb]
     exact zero_le _
   · rw [← le_pow_iff_clog_le hb]
     exact h.trans (le_pow_clog hb _)
 
-@[mono]
+@[mono, gcongr]
 theorem clog_anti_left {b c n : ℕ} (hc : 1 < c) (hb : c ≤ b) : clog b n ≤ clog c n := by
   rw [← le_pow_iff_clog_le (lt_of_lt_of_le hc hb)]
   calc
@@ -324,6 +333,12 @@ theorem clog_monotone (b : ℕ) : Monotone (clog b) := fun _ _ => clog_mono_righ
 theorem clog_antitone_left {n : ℕ} : AntitoneOn (fun b : ℕ => clog b n) (Set.Ioi 1) :=
   fun _ hc _ _ hb => clog_anti_left (Set.mem_Iio.1 hc) hb
 
+@[gcongr]
+theorem clog_mono {b c m n : ℕ} (hc : 1 < c) (hb : c ≤ b) (hmn : m ≤ n) :
+    clog b m ≤ clog c n := by
+  trans clog b n <;> gcongr; assumption
+
+@[simp]
 theorem log_le_clog (b n : ℕ) : log b n ≤ clog b n := by
   obtain hb | hb := le_or_gt b 1
   · rw [log_of_left_le_one hb]