-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
f : A ⊗[R] B ⊗[R] C ≃ₗ[R] D
h_mul :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
    (f : (a : A ⊗[R] B ⊗[R] C) → D) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) =
      HMul.hMul (α := D) (β := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) : D)
        ((f : (a : A ⊗[R] B ⊗[R] C) → D) (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂) : D)
h_one : Eq.{uD + 1} (α := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) : D) (1 : D)
x : A
x_1 : B
x_2 : C
x_3 : A
x_4 : B
x_5 : C
⊢ Eq.{uD + 1} (α := D)
    (((((((AlgebraTensorModule.curry
                          (AlgebraTensorModule.curry
                            (((((((AlgebraTensorModule.curry
                                                (AlgebraTensorModule.curry
                                                  (LinearMap.compr₂ (LinearMap.mul R (A ⊗[R] B ⊗[R] C))
                                                    (↑f : A ⊗[R] B ⊗[R] C →ₗ[R] D))) :
                                              A →ₗ[R] B →ₗ[R] C →ₗ[R] A ⊗[R] B ⊗[R] C →ₗ[R] D) :
                                            (a : A) → B →ₗ[R] C →ₗ[R] A ⊗[R] B ⊗[R] C →ₗ[R] D)
                                          x :
                                        B →ₗ[R] C →ₗ[R] A ⊗[R] B ⊗[R] C →ₗ[R] D) :
                                      (a : B) → C →ₗ[R] A ⊗[R] B ⊗[R] C →ₗ[R] D)
                                    x_1 :
                                  C →ₗ[R] A ⊗[R] B ⊗[R] C →ₗ[R] D) :
                                (a : C) → A ⊗[R] B ⊗[R] C →ₗ[R] D)
                              x_2)) :
                        A →ₗ[R] B →ₗ[R] C →ₗ[R] D) :
                      (a : A) → B →ₗ[R] C →ₗ[R] D)
                    x_3 :
                  B →ₗ[R] C →ₗ[R] D) :
                (a : B) → C →ₗ[R] D)
              x_4 :
            C →ₗ[R] D) :
          (a : C) → D)
        x_5 :
      D)
    (((((((AlgebraTensorModule.curry
                          (AlgebraTensorModule.curry
                            (((((((AlgebraTensorModule.curry
                                                (AlgebraTensorModule.curry
                                                  ((LinearMap.mul R D ∘ₗ (↑f : A ⊗[R] B ⊗[R] C →ₗ[R] D)).compl₂
                                                    (↑f : A ⊗[R] B ⊗[R] C →ₗ[R] D))) :
                                              A →ₗ[R] B →ₗ[R] C →ₗ[R] A ⊗[R] B ⊗[R] C →ₗ[R] D) :
                                            (a : A) → B →ₗ[R] C →ₗ[R] A ⊗[R] B ⊗[R] C →ₗ[R] D)
                                          x :
                                        B →ₗ[R] C →ₗ[R] A ⊗[R] B ⊗[R] C →ₗ[R] D) :
                                      (a : B) → C →ₗ[R] A ⊗[R] B ⊗[R] C →ₗ[R] D)
                                    x_1 :
                                  C →ₗ[R] A ⊗[R] B ⊗[R] C →ₗ[R] D) :
                                (a : C) → A ⊗[R] B ⊗[R] C →ₗ[R] D)
                              x_2)) :
                        A →ₗ[R] B →ₗ[R] C →ₗ[R] D) :
                      (a : A) → B →ₗ[R] C →ₗ[R] D)
                    x_3 :
                  B →ₗ[R] C →ₗ[R] D) :
                (a : B) → C →ₗ[R] D)
              x_4 :
            C →ₗ[R] D) :
          (a : C) → D)
        x_5 :
      D)
have a : (f : (a : A ⊗[R] B ⊗[R] C) → D) ((x * x_3) ⊗ₜ[R] (x_1 * x_4) ⊗ₜ[R] (x_2 * x_5)) =
  HMul.hMul (α := D) (β := D) ((f : (a : A ⊗[R] B ⊗[R] C) → D) (x ⊗ₜ[R] x_1 ⊗ₜ[R] x_2) : D)
    ((f : (a : A ⊗[R] B ⊗[R] C) → D) (x_3 ⊗ₜ[R] x_4 ⊗ₜ[R] x_5) : D)
Tactic: dsimp