-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Prod (goal)
Goal:
R : Type u_1
S : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : Algebra R S
inst_6 : Module R M₁
inst_7 : Module S M₁
inst_8 : IsScalarTower R S M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
a :
  ∀ (x : M₁) (x_1 : M₂),
    Eq (α := M₁ ⊗[R] (M₂ × M₃))
      ((((AlgebraTensorModule.curry
                      (LinearMap.coprod
                          (((AlgebraTensorModule.lTensor S M₁ :
                                (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                              (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                            (LinearMap.inl R M₂ M₃))
                          (((AlgebraTensorModule.lTensor S M₁ :
                                (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                              (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                            (LinearMap.inr R M₂ M₃)) ∘ₗ
                        AlgebraTensorModule.lift
                          (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                            LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃))) :
                    M₁ →ₗ[S] M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃)) :
                  (a : M₁) → M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃))
                x ∘ₗ
              LinearMap.inl R M₂ M₃ :
            (a : M₂) → M₁ ⊗[R] (M₂ × M₃))
          x_1 :
        M₁ ⊗[R] (M₂ × M₃))
      ((((AlgebraTensorModule.curry LinearMap.id : M₁ →ₗ[S] M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃)) :
                  (a : M₁) → M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃))
                x ∘ₗ
              LinearMap.inl R M₂ M₃ :
            (a : M₂) → M₁ ⊗[R] (M₂ × M₃))
          x_1 :
        M₁ ⊗[R] (M₂ × M₃))
⊢ Eq (α := M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
    (LinearMap.coprod
          (((AlgebraTensorModule.lTensor S M₁ : (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
              (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
            (LinearMap.inl R M₂ M₃))
          (((AlgebraTensorModule.lTensor S M₁ : (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
              (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
            (LinearMap.inr R M₂ M₃)) ∘ₗ
        AlgebraTensorModule.lift
          (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
            LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃)) :
      M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
    (LinearMap.id : M₁ ⊗[R] (M₂ × M₃) →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
have a₁ : ∀ (x : M₁) (x_1 : M₃),
  Eq (α := M₁ ⊗[R] (M₂ × M₃))
    ((((AlgebraTensorModule.curry
                    (LinearMap.coprod
                        (((AlgebraTensorModule.lTensor S M₁ :
                              (M₂ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                            (a : M₂ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₂ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                          (LinearMap.inl R M₂ M₃))
                        (((AlgebraTensorModule.lTensor S M₁ :
                              (M₃ →ₗ[R] M₂ × M₃) →ₗ[R] M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃)) :
                            (a : M₃ →ₗ[R] M₂ × M₃) → M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))
                          (LinearMap.inr R M₂ M₃)) ∘ₗ
                      AlgebraTensorModule.lift
                        (LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
                          LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃))) :
                  M₁ →ₗ[S] M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃)) :
                (a : M₁) → M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃))
              x ∘ₗ
            LinearMap.inr R M₂ M₃ :
          (a : M₃) → M₁ ⊗[R] (M₂ × M₃))
        x_1 :
      M₁ ⊗[R] (M₂ × M₃))
    ((((AlgebraTensorModule.curry LinearMap.id : M₁ →ₗ[S] M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃)) :
                (a : M₁) → M₂ × M₃ →ₗ[R] M₁ ⊗[R] (M₂ × M₃))
              x ∘ₗ
            LinearMap.inr R M₂ M₃ :
          (a : M₃) → M₁ ⊗[R] (M₂ × M₃))
        x_1 :
      M₁ ⊗[R] (M₂ × M₃))
Tactic: ext