chore(RingTheory/TensorProduct): golf (#7539)

This adds `LinearMap.map_mul_iff` to match `AddMonoidHom.map_mul_iff` and uses it (along with `AlgHom.ofLinearMap`) to golf away some induction proof in favor of `ext`.
The main motivation is the `map_mul_iff` lemma itself, not the golfing.

Also fixes some incorrect docstrings that were mangled during porting, and adds an explicit name to an instance.

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import Mathlib.Algebra.Algebra.Basic
+import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Hom.Iterate
 import Mathlib.Algebra.Hom.NonUnitalAlg
 import Mathlib.LinearAlgebra.TensorProduct
@@ -152,7 +153,18 @@ end NonUnital
 
 section Semiring
 
-variable (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
+variable (R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B]
+
+variable {R A B} in
+/-- A `LinearMap` preserves multiplication if pre- and post- composition with `LinearMap.mul` are
+equivalent. By converting the statement into an equality of `LinearMap`s, this lemma allows various
+specialized `ext` lemmas about `→ₗ[R]` to then be applied.
+
+This is the `LinearMap` version of `AddMonoidHom.map_mul_iff`. -/
+theorem map_mul_iff (f : A →ₗ[R] B) :
+    (∀ x y, f (x * y) = f x * f y) ↔
+      (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f :=
+  Iff.symm LinearMap.ext_iff₂
 
 /-- The multiplication in an algebra is an algebra homomorphism into the endomorphisms on
 the algebra.

Mathlib/Algebra/Algebra/RestrictScalars.lean

@@ -32,12 +32,12 @@ typeclass instead.
 There are many similarly-named definitions elsewhere which do not refer to this type alias. These
 refer to restricting the scalar type in a bundled type, such as from `A →ₗ[R] B` to `A →ₗ[S] B`:
 
-* `LinearMap.RestrictScalars`
-* `LinearEquiv.RestrictScalars`
-* `AlgHom.RestrictScalars`
-* `AlgEquiv.RestrictScalars`
-* `Submodule.RestrictScalars`
-* `Subalgebra.RestrictScalars`
+* `LinearMap.restrictScalars`
+* `LinearEquiv.restrictScalars`
+* `AlgHom.restrictScalars`
+* `AlgEquiv.restrictScalars`
+* `Submodule.restrictScalars`
+* `Subalgebra.restrictScalars`
 -/
 
 
@@ -214,7 +214,7 @@ theorem RestrictScalars.ringEquiv_map_smul (r : R) (x : RestrictScalars R S A) :
 #align restrict_scalars.ring_equiv_map_smul RestrictScalars.ringEquiv_map_smul
 
 /-- `R ⟶ S` induces `S-Alg ⥤ R-Alg` -/
-instance : Algebra R (RestrictScalars R S A) :=
+instance RestrictScalars.algebra : Algebra R (RestrictScalars R S A) :=
   { (algebraMap S A).comp (algebraMap R S) with
     smul := (· • ·)
     commutes' := fun _ _ ↦ Algebra.commutes' _ _

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -119,6 +119,9 @@ theorem congr_fun₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h :
   LinearMap.congr_fun (LinearMap.congr_fun h x) y
 #align linear_map.congr_fun₂ LinearMap.congr_fun₂
 
+theorem ext_iff₂ {f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} : f = g ↔ ∀ m n, f m n = g m n :=
+  ⟨congr_fun₂, ext₂⟩
+
 section
 
 attribute [local instance] SMulCommClass.symm

Mathlib/RingTheory/TensorProduct.lean

@@ -596,19 +596,12 @@ tensors can be directly applied by the caller (without needing `TensorProduct.on
 def algHomOfLinearMapTensorProduct (f : A ⊗[R] B →ₗ[S] C)
     (h_mul : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂))
     (h_one : f (1 ⊗ₜ[R] 1) = 1) : A ⊗[R] B →ₐ[S] C :=
-  AlgHom.ofLinearMap f h_one fun x y => by
-      simp only
-      refine TensorProduct.induction_on x ?_ ?_ ?_
-      · rw [zero_mul, map_zero, zero_mul]
-      · intro a₁ b₁
-        refine TensorProduct.induction_on y ?_ ?_ ?_
-        · rw [mul_zero, map_zero, mul_zero]
-        · intro a₂ b₂
-          rw [tmul_mul_tmul, h_mul]
-        · intro x₁ x₂ h₁ h₂
-          rw [mul_add, map_add, map_add, mul_add, h₁, h₂]
-      · intro x₁ x₂ h₁ h₂
-        rw [add_mul, map_add, map_add, add_mul, h₁, h₂]
+  AlgHom.ofLinearMap f h_one <| f.map_mul_iff.2 <| by
+    -- these instances are needed by the statement of `ext`, but not by the current definition.
+    letI : Algebra R C := RestrictScalars.algebra R S C
+    letI : IsScalarTower R S C := RestrictScalars.isScalarTower R S C
+    ext
+    exact h_mul _ _ _ _
 #align algebra.tensor_product.alg_hom_of_linear_map_tensor_product Algebra.TensorProduct.algHomOfLinearMapTensorProduct
 
 @[simp]
@@ -644,23 +637,9 @@ def algEquivOfLinearEquivTripleTensorProduct (f : (A ⊗[R] B) ⊗[R] C ≃ₗ[R
         f ((a₁ * a₂) ⊗ₜ (b₁ * b₂) ⊗ₜ (c₁ * c₂)) = f (a₁ ⊗ₜ b₁ ⊗ₜ c₁) * f (a₂ ⊗ₜ b₂ ⊗ₜ c₂))
     (h_one : f (((1 : A) ⊗ₜ[R] (1 : B)) ⊗ₜ[R] (1 : C)) = 1) :
     (A ⊗[R] B) ⊗[R] C ≃ₐ[R] D :=
--- porting note : build the whole algebra isomorphism times out, so I propose to define the version
--- of tensoring three rings in terms of the version tensoring with two rings
-algEquivOfLinearEquivTensorProduct f (fun x₁ x₂ c₁ c₂ => by
-  refine TensorProduct.induction_on x₁ ?_ ?_ ?_ <;>
-  refine TensorProduct.induction_on x₂ ?_ ?_ ?_ <;>
-  simp only [zero_tmul, tmul_zero, tmul_mul_tmul, map_zero, zero_mul, mul_zero, mul_add, add_mul,
-    map_add, add_tmul, tmul_add, h_mul] <;>
-  try
-    intros
-    trivial
-  · intros ab₁ ab₂ h₁ h₂ a b
-    rw [h₁, h₂]
-  · intros a b ab₁ ab₂ h₁ h₂
-    rw [h₁, h₂]
-  · intros ab₁ ab₂ _ _ x y hx hy
-    rw [add_add_add_comm, hx, hy, add_add_add_comm])
-  h_one
+  AlgEquiv.ofLinearEquiv f h_one <| f.map_mul_iff.2 <| by
+    ext
+    exact h_mul _ _ _ _ _ _
 #align algebra.tensor_product.alg_equiv_of_linear_equiv_triple_tensor_product Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct
 
 @[simp]