-- 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
x : A
hx : x ∈ S
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)
h :
  HMul.hMul (α := A ⊗[R] B) ((includeLeft : (a : A) → A ⊗[R] B) x : A ⊗[R] B)
      (HAdd.hAdd (α := 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)
        ((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)
      (HAdd.hAdd (α := 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)
        ((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)
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)
            y :
          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)
            z :
          A ⊗[R] B) =
    HMul.hMul (β := A ⊗[R] B)
      (HAdd.hAdd (α := 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)
        ((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)
h₂ :
  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) +
      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)
      (HAdd.hAdd (α := 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)
        ((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)
h₃ :
  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) +
      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)
      (HAdd.hAdd (α := 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)
        ((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)
h₄ h₅ :
  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) +
      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)
        ((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) +
      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)

Tactic:
rw [map_add, mul_add, hy, hz, add_mul]

Premises used: add_mul, map_add, mul_add