feat(linear_algebra/prod): add an ext lemma that recurses into produc…

…ts (#6124)

Combined with #6105, this means that applying `ext` when faced with an equality between `A × (B ⊗[R] C) →ₗ[R] D`s now expands to two goals, the first taking `a : A` and the second taking `b : B` and `c : C`.

Again, this comes at the expense of sometimes needing to `simp [prod.mk_fst, linear_map.inr_apply]` after using `ext`, but those are all covered by `dsimp` anyway.

src/linear_algebra/prod.lean

@@ -18,6 +18,7 @@ It contains theorems relating these to each other, as well as to `submodule.prod
   - `linear_map.fst`
   - `linear_map.snd`
   - `linear_map.coprod`
+  - `linear_map.prod_ext`
 - products in the codomain:
   - `linear_map.inl`
   - `linear_map.inr`
@@ -154,6 +155,20 @@ their domains. -/
   map_smul' := λ r a,
     by { ext, simp only [smul_add, smul_apply, prod.smul_snd, prod.smul_fst, coprod_apply] } }
 
+/--
+Split equality of linear maps from a product into linear maps over each component, to allow `ext`
+to apply lemmas specific to `M →ₗ M₃` and `M₂ →ₗ M₃`.
+
+See note [partially-applied ext lemmas]. -/
+@[ext] theorem prod_ext {f g : M × M₂ →ₗ[R] M₃}
+  (hl : f.comp (inl _ _ _) = g.comp (inl _ _ _))
+  (hr : f.comp (inr _ _ _) = g.comp (inr _ _ _)) :
+  f = g :=
+begin
+  refine (coprod_equiv ℕ).symm.injective _,
+  simp only [coprod_equiv_symm_apply, hl, hr],
+end
+
 /-- `prod.map` of two linear maps. -/
 def prod_map (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₄) : (M × M₂) →ₗ[R] (M₃ × M₄) :=
 (f.comp (fst R M M₂)).prod (g.comp (snd R M M₂))