chore: ext lemma for DirectSum (#20600)

kim-em · kim-em · commit 66b1e307fa9d · 2025-01-10T00:02:55.000Z
diff --git a/Mathlib/Algebra/DirectSum/Basic.lean b/Mathlib/Algebra/DirectSum/Basic.lean
@@ -90,6 +90,9 @@ end AddCommGroup
 
 variable [∀ i, AddCommMonoid (β i)]
 
+@[ext] theorem ext {x y : DirectSum ι β} (w : ∀ i, x i = y i) : x = y :=
+  DFunLike.ext _ _ w
+
 @[simp]
 theorem zero_apply (i : ι) : (0 : ⨁ i, β i) i = 0 :=
   rfl
diff --git a/Mathlib/Algebra/DirectSum/Module.lean b/Mathlib/Algebra/DirectSum/Module.lean
@@ -182,12 +182,14 @@ variable {ι M}
 theorem apply_eq_component (f : ⨁ i, M i) (i : ι) : f i = component R ι M i f := rfl
 
 -- Note(kmill): `@[ext]` cannot prove `ext_iff` because `R` is not determined by `f` or `g`.
-@[ext (iff := false)]
-theorem ext {f g : ⨁ i, M i} (h : ∀ i, component R ι M i f = component R ι M i g) : f = g :=
+-- This is not useful as an `@[ext]` lemma as the `ext` tactic can not infer `R`.
+theorem ext_component {f g : ⨁ i, M i} (h : ∀ i, component R ι M i f = component R ι M i g) :
+    f = g :=
   DFinsupp.ext h
 
-theorem ext_iff {f g : ⨁ i, M i} : f = g ↔ ∀ i, component R ι M i f = component R ι M i g :=
-  ⟨fun h _ ↦ by rw [h], ext R⟩
+theorem ext_component_iff {f g : ⨁ i, M i} :
+    f = g ↔ ∀ i, component R ι M i f = component R ι M i g :=
+  ⟨fun h _ ↦ by rw [h], ext_component R⟩
 
 @[simp]
 theorem lof_apply [DecidableEq ι] (i : ι) (b : M i) : ((lof R ι M i) b) i = b :=
diff --git a/Mathlib/Algebra/DirectSum/Ring.lean b/Mathlib/Algebra/DirectSum/Ring.lean
@@ -235,7 +235,7 @@ private theorem mul_assoc (a b c : ⨁ i, A i) : a * b * c = a * (b * c) := by
       simpa only [coe_comp, Function.comp_apply, AddMonoidHom.compHom_apply_apply, flip_apply,
         AddMonoidHom.flipHom_apply]
         using DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this a) b) c
-  ext ai ax bi bx ci cx
+  ext ai ax bi bx ci cx : 6
   dsimp only [coe_comp, Function.comp_apply, AddMonoidHom.compHom_apply_apply, flip_apply,
     AddMonoidHom.flipHom_apply]
   simp_rw [mulHom_of_of]
diff --git a/Mathlib/Algebra/Lie/DirectSum.lean b/Mathlib/Algebra/Lie/DirectSum.lean
@@ -43,13 +43,13 @@ variable [∀ i, LieRingModule L (M i)] [∀ i, LieModule R L (M i)]
 instance : LieRingModule L (⨁ i, M i) where
   bracket x m := m.mapRange (fun _ m' => ⁅x, m'⁆) fun _ => lie_zero x
   add_lie x y m := by
-    refine DFinsupp.ext fun _ => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
+    ext
     simp only [mapRange_apply, add_apply, add_lie]
   lie_add x m n := by
-    refine DFinsupp.ext fun _ => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
+    ext
     simp only [mapRange_apply, add_apply, lie_add]
   leibniz_lie x y m := by
-    refine DFinsupp.ext fun _ => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
+    ext
     simp only [mapRange_apply, lie_lie, add_apply, sub_add_cancel]
 
 @[simp]
@@ -58,10 +58,10 @@ theorem lie_module_bracket_apply (x : L) (m : ⨁ i, M i) (i : ι) : ⁅x, m⁆
 
 instance : LieModule R L (⨁ i, M i) where
   smul_lie t x m := by
-    refine DFinsupp.ext fun _ => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext i`
+    ext
     simp only [smul_lie, lie_module_bracket_apply, smul_apply]
   lie_smul t x m := by
-    refine DFinsupp.ext fun _ => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext i`
+    ext
     simp only [lie_smul, lie_module_bracket_apply, smul_apply]
 
 variable (R ι L M)
@@ -70,7 +70,7 @@ variable (R ι L M)
 def lieModuleOf [DecidableEq ι] (j : ι) : M j →ₗ⁅R,L⁆ ⨁ i, M i :=
   { lof R ι M j with
     map_lie' := fun {x m} => by
-      refine DFinsupp.ext fun i => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext i`
+      ext i
       by_cases h : j = i
       · rw [← h]; simp
       · -- This used to be the end of the proof before https://github.com/leanprover/lean4/pull/2644
@@ -98,16 +98,16 @@ instance lieRing : LieRing (⨁ i, L i) :=
   { (inferInstance : AddCommGroup _) with
     bracket := zipWith (fun _ => fun x y => ⁅x, y⁆) fun _ => lie_zero 0
     add_lie := fun x y z => by
-      refine DFinsupp.ext fun _ => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
+      ext
       simp only [zipWith_apply, add_apply, add_lie]
     lie_add := fun x y z => by
-      refine DFinsupp.ext fun _ => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
+      ext
       simp only [zipWith_apply, add_apply, lie_add]
     lie_self := fun x => by
-      refine DFinsupp.ext fun _ => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
+      ext
       simp only [zipWith_apply, add_apply, lie_self, zero_apply]
     leibniz_lie := fun x y z => by
-      refine DFinsupp.ext fun _ => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
+      ext
       simp only [sub_apply, zipWith_apply, add_apply, zero_apply]
       apply leibniz_lie }
 
@@ -121,7 +121,7 @@ theorem lie_of_same [DecidableEq ι] {i : ι} (x y : L i) :
 
 theorem lie_of_of_ne [DecidableEq ι] {i j : ι} (hij : i ≠ j) (x : L i) (y : L j) :
     ⁅of L i x, of L j y⁆ = 0 := by
-  refine DFinsupp.ext fun k => ?_
+  ext k
   rw [bracket_apply]
   obtain rfl | hik := Decidable.eq_or_ne i k
   · rw [of_eq_of_ne _ _ _ hij.symm, lie_zero, zero_apply]
@@ -137,7 +137,7 @@ theorem lie_of [DecidableEq ι] {i j : ι} (x : L i) (y : L j) :
 instance lieAlgebra : LieAlgebra R (⨁ i, L i) :=
   { (inferInstance : Module R _) with
     lie_smul := fun c x y => by
-      refine DFinsupp.ext fun _ => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
+      ext
       simp only [zipWith_apply, smul_apply, bracket_apply, lie_smul] }
 
 variable (R ι)
@@ -148,7 +148,7 @@ def lieAlgebraOf [DecidableEq ι] (j : ι) : L j →ₗ⁅R⁆ ⨁ i, L i :=
   { lof R ι L j with
     toFun := of L j
     map_lie' := fun {x y} => by
-      refine DFinsupp.ext fun i => ?_ -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext i`
+      ext i
       by_cases h : j = i
       · rw [← h]
         -- This used to be the end of the proof before https://github.com/leanprover/lean4/pull/2644
diff --git a/Mathlib/RingTheory/AdicCompletion/Functoriality.lean b/Mathlib/RingTheory/AdicCompletion/Functoriality.lean
@@ -287,8 +287,8 @@ theorem sumInv_apply (x : AdicCompletion I (⨁ j, M j)) (j : ι) :
 variable [DecidableEq ι]
 
 theorem sumInv_comp_sum : sumInv I M ∘ₗ sum I M = LinearMap.id := by
-  ext j x
-  apply DirectSum.ext (AdicCompletion I R) (fun i ↦ ?_)
+  ext j x : 2
+  apply DirectSum.ext_component (AdicCompletion I R) (fun i ↦ ?_)
   ext n
   simp only [LinearMap.coe_comp, Function.comp_apply, sum_lof, map_mk, component_sumInv,
     mk_apply_coe, AdicCauchySequence.map_apply_coe, Submodule.mkQ_apply, LinearMap.id_comp]
diff --git a/Mathlib/RingTheory/Flat/Basic.lean b/Mathlib/RingTheory/Flat/Basic.lean
@@ -195,7 +195,7 @@ instance directSum (ι : Type v) (M : ι → Type w) [(i : ι) → AddCommGroup
     by_cases h₂ : j = i
     · subst j; simp
     · simp [h₂]
-  intro a ha; rw [DirectSum.ext_iff R]; intro i
+  intro a ha; rw [DirectSum.ext_component_iff R]; intro i
   have f := LinearMap.congr_arg (f := (π i)) ha
   erw [LinearMap.congr_fun (h₁ i) a] at f
   rw [(map_zero (π i) : (π i) 0 = (0 : M i))] at f
