-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Subalgebra (goal)
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
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R ↥⊥ : (a : R) → ↥⊥) x' = x
y' : R
hy : (algebraMap R ↥⊥ : (a : R) → ↥⊥) y' = y
refine_1 :
  ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      (HMul.hMul (α := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x' : ↥⊥) y ⊗ₜ[R] (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x' ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (y ⊗ₜ[R] b) :
        ↥A)
refine_1₁ :
  ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      (HMul.hMul (α := ↥⊥) (β := ↥⊥) ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x' : ↥⊥)
          ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y' : ↥⊥) ⊗ₜ[R]
        (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x' ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y' ⊗ₜ[R] b) :
        ↥A)
refine_1₂ :
  ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((algebraMap R ↥⊥ : (a : R) → ↥⊥) (x' * y') ⊗ₜ[R] (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          ((algebraMap R ↥⊥ : (a : R) → ↥⊥) x' ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y' ⊗ₜ[R] b) :
        ↥A)
refine_1₃ :
  ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((algebraMap R ↥⊥ : (a : R) → ↥⊥) (x' * y') ⊗ₜ[R] (a * b)) =
    HMul.hMul (β := ↥A) (x' • a)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          ((algebraMap R ↥⊥ : (a : R) → ↥⊥) y' ⊗ₜ[R] b) :
        ↥A)
refine_1₄ :
  ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((algebraMap R ↥⊥ : (a : R) → ↥⊥) (x' * y') ⊗ₜ[R] (a * b)) =
    x' • a * y' • b
⊢ ((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
          ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
            ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
        (a : ↥⊥ ⊗[R] ↥A) → ↥A)
      ((x * y) ⊗ₜ[R] (a * b)) =
    HMul.hMul (α := ↥A) (β := ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (x ⊗ₜ[R] a) :
        ↥A)
      (((Submodule.lTensorOne ((toSubmodule : (a : Subalgebra R S) → Submodule R S) A) :
              ↥⊥ ⊗[R] ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S) ≃ₗ[R]
                ↥((toSubmodule : (a : Subalgebra R S) → Submodule R S) A : Submodule R S)) :
            (a : ↥⊥ ⊗[R] ↥A) → ↥A)
          (y ⊗ₜ[R] b) :
        ↥A)
have refine_1₅ : (x' * y') • (a * b) = x' • a * y' • b
Tactic: rw [← hx, ← hy, ← map_mul, (toSubmodule A).lTensorOne_tmul x' a,
      (toSubmodule A).lTensorOne_tmul y' b, (toSubmodule A).lTensorOne_tmul (x' * y') (a * b),
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul, mul_comm x' y']