-- Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Semiring T
inst_4 : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x
y' : R
hy : (algebraMap R ↥⊥ : (a : R) → ↥⊥) y' = y
refine_1 :
  ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] HMul.hMul (α := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x' : ↥⊥) y) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x') :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] y) :
        ↥A)
refine_1₁ :
  ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R]
        HMul.hMul (α := ↥⊥) (β := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x' : ↥⊥)
          ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y' : ↥⊥)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x') :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) y') :
        ↥A)
refine_1₂ :
  ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) (x' * y')) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) x') :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) y') :
        ↥A)
refine_1₃ :
  ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) (x' * y')) =
    HMul.hMul (β := ↥A) (x' • a)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) y') :
        ↥A)
refine_1₄ :
  ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (algebraMap R ↥⊥ : (a : R) → ↥⊥) (x' * y')) =
    x' • a * y' • b
refine_1₅ : (x' * y') • (a * b) = x' • a * y' • b
refine_1₆ : (x' * y') • (a * b) = y' • (x' • a * b)
refine_1₇ : (x' * y') • (a * b) = y' • x' • (a * b)
refine_1₈ : (x' * y') • (a * b) = (y' * x') • (a * b)
refine_1₉ refine_1₁₀ : (y' * x') • (a * b) = (y' * x') • (a * b)
⊢ ((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥A ⊗[R] ↥⊥) → ↥A)
      ((a * b) ⊗ₜ[R] (x * y)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (a ⊗ₜ[R] x) :
        ↥A)
      (((Submodule.rTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ⊗[R] ↥⊥ ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥A ⊗[R] ↥⊥) → ↥A)
          (b ⊗ₜ[R] y) :
        ↥A)

Tactic:
rw [← hx, ← hy, ← map_mul, (toSubmodule A).rTensorOne_tmul x' a,
      (toSubmodule A).rTensorOne_tmul y' b, (toSubmodule A).rTensorOne_tmul (x' * y') (a * b),
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul, mul_comm x' y']

Premises used: Algebra.mul_smul_comm, HMul.hMul, smul_smul, Submodule.rTensorOne_tmul, map_mul, Algebra.smul_mul_assoc, mul_comm