merge master

Author: kim-em

Mathlib.lean

@@ -5439,6 +5439,7 @@ import Mathlib.RingTheory.LocalRing.RingHom.Basic
 import Mathlib.RingTheory.LocalRing.Subring
 import Mathlib.RingTheory.Localization.Algebra
 import Mathlib.RingTheory.Localization.AsSubring
+import Mathlib.RingTheory.Localization.AtPrime
 import Mathlib.RingTheory.Localization.AtPrime.Basic
 import Mathlib.RingTheory.Localization.Away.AdjoinRoot
 import Mathlib.RingTheory.Localization.Away.Basic
@@ -6561,6 +6562,7 @@ import Mathlib.Topology.PreorderRestrict
 import Mathlib.Topology.QuasiSeparated
 import Mathlib.Topology.Semicontinuous
 import Mathlib.Topology.SeparatedMap
+import Mathlib.Topology.Separation.AlexandrovDiscrete
 import Mathlib.Topology.Separation.Basic
 import Mathlib.Topology.Separation.CompletelyRegular
 import Mathlib.Topology.Separation.Connected

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -265,8 +265,7 @@ protected theorem rel_map_of_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddM
       -- If `R = (· < ·)`, then the proof looks like
       -- `f x < f (l + a) ≤ f (l + n • a) < f y`
       trans f (l + (1 : ℤ) • a)
-      · rw [one_zsmul]
-        exact hf x (Ico_subset_Icc_self hx) (l + a) (by simpa) hx.2
+      · grind
       have hy : R (f (l + n • a)) (f y) := by
         rw [← sub_add_cancel y (n • a), map_add_zsmul, map_add_zsmul]
         refine hR _ <| hf _ ?_ _ (Ioc_subset_Icc_self hny) hny.1; simpa

Mathlib/Algebra/Algebra/Operations.lean

@@ -362,6 +362,9 @@ theorem algebraMap_mem (r : R) : algebraMap R A r ∈ (1 : Submodule R A) := by
 theorem mem_one {x : A} : x ∈ (1 : Submodule R A) ↔ ∃ y, algebraMap R A y = x := by
   simp [one_eq_range]
 
+theorem smul_one_eq_span (x : A) : x • (1 : Submodule R A) = span R {x} := by
+  rw [one_eq_span, smul_span, smul_set_singleton, smul_eq_mul, mul_one]
+
 protected theorem map_one {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') :
     map f.toLinearMap (1 : Submodule R A) = 1 := by
   ext

Mathlib/Algebra/BigOperators/Associated.lean

@@ -122,7 +122,7 @@ theorem Multiset.prod_primes_dvd [CancelCommMonoidWithZero M₀]
   | cons a s induct =>
     rw [Multiset.prod_cons]
     obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)
-    apply mul_dvd_mul_left a
+    gcongr
     refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
       fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
     have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)

Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

@@ -112,9 +112,7 @@ theorem prod_ite_eq' [DecidableEq α] (f : α →₀ M) (a : α) (b : α → M 
 /-- A restatement of `sum_ite_self_eq` with the equality test reversed. -/
 theorem sum_ite_self_eq' [DecidableEq α] {N : Type*} [AddCommMonoid N] (f : α →₀ N) (a : α) :
     (f.sum fun x v => ite (x = a) v 0) = f a := by
-  classical
-    convert f.sum_ite_eq' a fun _ => id
-    simp [ite_eq_right_iff.2 Eq.symm]
+  simp
 
 @[to_additive (attr := simp)]
 theorem prod_pow [Fintype α] (f : α →₀ ℕ) (g : α → N) :

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -830,10 +830,8 @@ theorem prod_unique_nonempty [Unique ι] (s : Finset ι) (f : ι → M) (h : s.N
   rw [h.eq_singleton_default, Finset.prod_singleton]
 
 lemma prod_dvd_prod_of_dvd (f g : ι → M) (h : ∀ i ∈ s, f i ∣ g i) :
-    ∏ i ∈ s, f i ∣ ∏ i ∈ s, g i := by
-  induction s using Finset.cons_induction with
-  | empty => simp
-  | cons a T haT IH => grind [mul_dvd_mul]
+    ∏ i ∈ s, f i ∣ ∏ i ∈ s, g i :=
+  Multiset.prod_dvd_prod_of_dvd _ _ h
 
 end CommMonoid
 

Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean

@@ -304,8 +304,7 @@ theorem succ_nth_conv_eq_squashGCF_nth_conv [Field K]
             (contsAux_eq_contsAux_squashGCF_of_le n'.le_succ).symm]
         symm
         simpa only [eq1, eq2, eq3, eq4, mul_div_cancel_right₀ _ b_ne_zero]
-      field_simp
-      congr 1 <;> ring
+      grind
 
 end Squash
 
@@ -350,9 +349,7 @@ theorem convs_eq_convs' [Field K] [LinearOrder K] [IsStrictOrderedRing K]
           suffices 0 < gp_m.a ∧ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b by
             have ot : g'.s.get? m = some ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ :=
               squashSeq_nth_of_not_terminated mth_s_eq s_succ_mth_eq
-            have : gp' = ⟨gp_m.a, gp_m.b + gp_succ_m.a / gp_succ_m.b⟩ := by
-              simp_all only [Option.some.injEq]
-            rwa [this]
+            grind
           have m_lt_n : m < m.succ := Nat.lt_succ_self m
           refine ⟨(s_pos (Nat.lt.step m_lt_n) mth_s_eq).left, ?_⟩
           refine add_pos (s_pos (Nat.lt.step m_lt_n) mth_s_eq).right ?_

Mathlib/Algebra/ContinuedFractions/Determinant.lean

@@ -60,10 +60,7 @@ theorem determinant_aux (hyp : n = 0 ∨ ¬(↑s : GenContFract K).TerminatedAt
       rw [gp_a_eq_one, this.symm]
       ring
     suffices pA * ppB - pB * ppA = (-1) ^ (n + 1) by grind
-    suffices ppA * pB - ppB * pA = (-1) ^ n by
-      have pow_succ_n : (-1 : K) ^ (n + 1) = -1 * (-1) ^ n := pow_succ' (-1) n
-      rw [pow_succ_n, ← this]
-      ring
+    suffices ppA * pB - ppB * pA = (-1) ^ n by grind
     exact IH <| Or.inr <| mt (terminated_stable <| n.sub_le 1) not_terminated_at_n
 
 /-- The determinant formula `Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-1)^(n + 1)`. -/

Mathlib/Algebra/Divisibility/Basic.lean

@@ -187,11 +187,9 @@ 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 mul_dvd_mul_right (h : a ∣ b) (c : α) : a * c ∣ b * c := by
+  gcongr
 
-@[gcongr]
 theorem pow_dvd_pow_of_dvd (h : a ∣ b) (n : ℕ) : a ^ n ∣ b ^ n := by
   induction n with
   | zero => simp
@@ -201,6 +199,6 @@ theorem pow_dvd_pow_of_dvd (h : a ∣ b) (n : ℕ) : a ^ n ∣ b ^ n := by
 
 @[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
+  trans (a ^ n) <;> [gcongr; apply_rules [pow_dvd_pow_of_dvd]]
 
 end CommMonoid

Mathlib/Algebra/Divisibility/Hom.lean

@@ -23,6 +23,7 @@ attribute [local simp] mul_assoc mul_comm mul_left_comm
 
 variable {M N : Type*}
 
+@[gcongr]
 theorem map_dvd [Semigroup M] [Semigroup N] {F : Type*} [FunLike F M N] [MulHomClass F M N]
     (f : F) {a b} : a ∣ b → f a ∣ f b
   | ⟨c, h⟩ => ⟨f c, h.symm ▸ map_mul f a c⟩