feat(LinearAlgebra/SModEq): add gcongr lemmas (#28008)

Author: astrainfinita

Mathlib/LinearAlgebra/SModEq.lean

@@ -64,42 +64,72 @@ instance : IsRefl _ (SModEq U) :=
 nonrec theorem symm (hxy : x ≡ y [SMOD U]) : y ≡ x [SMOD U] :=
   hxy.symm
 
+theorem comm : x ≡ y [SMOD U] ↔ y ≡ x [SMOD U] := ⟨symm, symm⟩
+
 @[trans]
 nonrec theorem trans (hxy : x ≡ y [SMOD U]) (hyz : y ≡ z [SMOD U]) : x ≡ z [SMOD U] :=
   hxy.trans hyz
 
 instance instTrans : Trans (SModEq U) (SModEq U) (SModEq U) where
   trans := trans
 
+@[gcongr]
 theorem add (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ + x₂ ≡ y₁ + y₂ [SMOD U] := by
   rw [SModEq.def] at hxy₁ hxy₂ ⊢
   simp_rw [Quotient.mk_add, hxy₁, hxy₂]
 
+@[gcongr]
+theorem sum {ι} {s : Finset ι} {x y : ι → M}
+    (hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]) : ∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U] := by
+  classical
+  induction s using Finset.cons_induction with
+  | empty => simp [SModEq.rfl]
+  | cons i s _ ih =>
+    grw [Finset.sum_cons, Finset.sum_cons, hxy i (Finset.mem_cons_self i s),
+      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]
+
+@[gcongr]
 theorem smul (hxy : x ≡ y [SMOD U]) (c : R) : c • x ≡ c • y [SMOD U] := by
   rw [SModEq.def] at hxy ⊢
   simp_rw [Quotient.mk_smul, hxy]
 
+@[gcongr]
 lemma nsmul (hxy : x ≡ y [SMOD U]) (n : ℕ) : n • x ≡ n • y [SMOD U] := by
   rw [SModEq.def] at hxy ⊢
   simp_rw [Quotient.mk_smul, hxy]
 
+@[gcongr]
 lemma zsmul (hxy : x ≡ y [SMOD U]) (n : ℤ) : n • x ≡ n • y [SMOD U] := by
   rw [SModEq.def] at hxy ⊢
   simp_rw [Quotient.mk_smul, hxy]
 
+@[gcongr]
 theorem mul {I : Ideal A} {x₁ x₂ y₁ y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I])
     (hxy₂ : x₂ ≡ y₂ [SMOD I]) : x₁ * x₂ ≡ y₁ * y₂ [SMOD I] := by
   simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_mul] at hxy₁ hxy₂ ⊢
   rw [hxy₁, hxy₂]
 
+@[gcongr]
+theorem prod {I : Ideal A} {ι} {s : Finset ι} {x y : ι → A}
+    (hxy : ∀ i ∈ s, x i ≡ y i [SMOD I]) : ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I] := by
+  classical
+  induction s using Finset.cons_induction with
+  | empty => simp [SModEq.rfl]
+  | cons i s _ ih =>
+    grw [Finset.prod_cons, Finset.prod_cons, hxy i (Finset.mem_cons_self i s),
+      ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]
+
+@[gcongr]
 lemma pow {I : Ideal A} {x y : A} (n : ℕ) (hxy : x ≡ y [SMOD I]) :
     x ^ n ≡ y ^ n [SMOD I] := by
   simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_pow] at hxy ⊢
   rw [hxy]
 
+@[gcongr]
 lemma neg (hxy : x ≡ y [SMOD U]) : - x ≡ - y [SMOD U] := by
   simpa only [SModEq.def, Quotient.mk_neg, neg_inj]
 
+@[gcongr]
 lemma sub (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ - x₂ ≡ y₁ - y₂ [SMOD U] := by
   rw [SModEq.def] at hxy₁ hxy₂ ⊢
   simp_rw [Quotient.mk_sub, hxy₁, hxy₂]
@@ -116,11 +146,10 @@ theorem comap {f : M →ₗ[R] N} (hxy : f x ≡ f y [SMOD V]) : x ≡ y [SMOD V
   (Submodule.Quotient.eq _).2 <|
     show f (x - y) ∈ V from (f.map_sub x y).symm ▸ (Submodule.Quotient.eq _).1 hxy
 
+@[gcongr]
 theorem eval {R : Type*} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD I]) (f : R[X]) :
     f.eval x ≡ f.eval y [SMOD I] := by
-  rw [SModEq.def] at h ⊢
-  change Ideal.Quotient.mk I (f.eval x) = Ideal.Quotient.mk I (f.eval y)
-  replace h : Ideal.Quotient.mk I x = Ideal.Quotient.mk I y := h
-  rw [← Polynomial.eval₂_at_apply, ← Polynomial.eval₂_at_apply, h]
+  simp_rw [Polynomial.eval_eq_sum, Polynomial.sum]
+  gcongr
 
 end SModEq