feat(linear_algebra/pi): ext lemma for f : (Π i, M i) →ₗ[R] N (#6233)

src/algebra/big_operators/pi.lean

@@ -61,7 +61,6 @@ begin
   { intro h, exfalso, simpa using h, },
 end
 
-@[ext]
 lemma add_monoid_hom.functions_ext [fintype I] (G : Type*)
   [add_comm_monoid G] (g h : (Π i, Z i) →+ G)
   (w : ∀ (i : I) (x : Z i), g (pi.single i x) = h (pi.single i x)) : g = h :=
@@ -73,22 +72,28 @@ begin
   apply w,
 end
 
+/-- This is used as the ext lemma instead of `add_monoid_hom.functions_ext` for reasons explained in
+note [partially-applied ext lemmas]. -/
+@[ext]
+lemma add_monoid_hom.functions_ext' [fintype I] (M : Type*) [add_comm_monoid M]
+  (g h : (Π i, Z i) →+ M)
+  (H : ∀ i, g.comp (add_monoid_hom.single Z i) = h.comp (add_monoid_hom.single Z i)) :
+  g = h :=
+have _ := λ i, add_monoid_hom.congr_fun (H i), -- elab without an expected type
+g.functions_ext M h this
+
 end single
 
 section ring_hom
 open pi
 variables {I : Type*} [decidable_eq I] {f : I → Type*}
 variables [Π i, semiring (f i)]
 
--- we need `apply`+`convert` because Lean fails to unify different `add_monoid` instances
--- on `Π i, f i`
 @[ext]
 lemma ring_hom.functions_ext [fintype I] (G : Type*) [semiring G] (g h : (Π i, f i) →+* G)
   (w : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h :=
-begin
-  apply ring_hom.coe_add_monoid_hom_injective,
-  convert add_monoid_hom.functions_ext _ _ _ _; assumption
-end
+ring_hom.coe_add_monoid_hom_injective $
+ add_monoid_hom.functions_ext G (g : (Π i, f i) →+ G) h w
 
 end ring_hom
 

src/linear_algebra/matrix.lean

@@ -140,7 +140,7 @@ end
 
 @[simp] lemma matrix.to_lin'_one :
   matrix.to_lin' (1 : matrix n n R) = id :=
-by { ext, simp }
+by { ext, simp [one_apply, std_basis_apply] }
 
 @[simp] lemma linear_map.to_matrix'_id :
   (linear_map.to_matrix' (linear_map.id : (n → R) →ₗ[R] (n → R))) = 1 :=

src/linear_algebra/std_basis.lean

@@ -44,12 +44,40 @@ def std_basis (i : ι) : φ i →ₗ[R] (Πi, φ i) := pi (diag i)
 lemma std_basis_apply (i : ι) (b : φ i) : std_basis R φ i b = update 0 i b :=
 by ext j; rw [std_basis, pi_apply, diag, update_apply]; refl
 
+lemma coe_std_basis (i : ι) : ⇑(std_basis R φ i) = pi.single i :=
+funext $ std_basis_apply R φ i
+
 @[simp] lemma std_basis_same (i : ι) (b : φ i) : std_basis R φ i b i = b :=
 by rw [std_basis_apply, update_same]
 
 lemma std_basis_ne (i j : ι) (h : j ≠ i) (b : φ i) : std_basis R φ i b j = 0 :=
 by rw [std_basis_apply, update_noteq h]; refl
 
+section ext
+
+variables {R φ} {M : Type*} [fintype ι] [add_comm_monoid M] [semimodule R M]
+  {f g : (Π i, φ i) →ₗ[R] M}
+
+lemma pi_ext (h : ∀ i x, f (pi.single i x) = g (pi.single i x)) :
+  f = g :=
+to_add_monoid_hom_injective $ add_monoid_hom.functions_ext _ _ _ h
+
+lemma pi_ext_iff : f = g ↔ ∀ i x, f (pi.single i x) = g (pi.single i x) :=
+⟨λ h i x, h ▸ rfl, pi_ext⟩
+
+/-- This is used as the ext lemma instead of `linear_map.pi_ext` for reasons explained in
+note [partially-applied ext lemmas]. -/
+@[ext] lemma pi_ext' (h : ∀ i, f.comp (std_basis R φ i) = g.comp (std_basis R φ i)) : f = g :=
+begin
+  refine pi_ext (λ i x, _),
+  simpa only [comp_apply, coe_std_basis] using linear_map.congr_fun (h i) x
+end
+
+lemma pi_ext'_iff : f = g ↔ ∀ i, f.comp (std_basis R φ i) = g.comp (std_basis R φ i) :=
+⟨λ h i, h ▸ rfl, pi_ext'⟩
+
+end ext
+
 lemma ker_std_basis (i : ι) : ker (std_basis R φ i) = ⊥ :=
 ker_eq_bot_of_injective $ assume f g hfg,
   have std_basis R φ i f i = std_basis R φ i g i := hfg ▸ rfl,