-- Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : Semiring A
inst_2 : Algebra R A
B : Type u_3
inst_3 : Semiring B
inst_4 : Algebra R B
S : Set A
inst_5 : Module.Free R B
w : TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B
x : A
hx : x ∈ S
h :
  HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          0 :
        A ⊗[R] B) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          0 :
        A ⊗[R] B)
      ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
h₁ :
  ∀ (b : ↥(centralizer R S)) (c : B),
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
        ((AlgHom.toRingHom
                (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                  TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
              (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
            (b ⊗ₜ[R] c) :
          A ⊗[R] B) =
      HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
        ((AlgHom.toRingHom
                (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                  TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
              (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
            (b ⊗ₜ[R] c) :
          A ⊗[R] B)
        ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
h₂ :
  ∀ (y z : TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B)
    (hy :
      HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
          ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                    TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
                (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
              y :
            A ⊗[R] B) =
        HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
          ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                    TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
                (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
              y :
            A ⊗[R] B)
          ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B))
    (hz :
      HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
          ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                    TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
                (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
              z :
            A ⊗[R] B) =
        HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
          ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                    TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
                (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
              z :
            A ⊗[R] B)
          ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)),
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
        ((AlgHom.toRingHom
                (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                  TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
              (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
            (y + z) :
          A ⊗[R] B) =
      HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
        ((AlgHom.toRingHom
                (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                  TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
              (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
            (y + z) :
          A ⊗[R] B)
        ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
⊢ HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          w :
        A ⊗[R] B) =
    HMul.hMul (α := A ⊗[R] B) (β := A ⊗[R] B)
      ((AlgHom.toRingHom
              (Algebra.TensorProduct.map (val (centralizer R S)) (AlgHom.id R B) :
                TensorProduct.{u_1, u_2, u_3} R (↥(centralizer R S)) B →ₐ[R] A ⊗[R] B) :
            (a : ↥(centralizer R S) ⊗[R] B) → A ⊗[R] B)
          w :
        A ⊗[R] B)
      ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)

Tactic:
induction w using TensorProduct.induction_on with
    | zero => simp
    | tmul b c =>
      simp [Subalgebra.mem_centralizer_iff _ |>.1 b.2 x hx]
    | add y z hy hz => rw [map_add, mul_add, hy, hz, add_mul]

Premises used: add_mul, map_add, mul_add, TensorProduct.tmul