awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ Eq (α := N ⊗[R] ((i : ι) → M i))
    (((LinearEquiv.symm (piRight R S N M) :
          ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) ≃ₗ[S] N ⊗[R] ((i : ι) → M i)) :
        (a : (i : ι) → N ⊗[R] M i) → N ⊗[R] ((i : ι) → M i))
      fun (i : ι) ↦ x ⊗ₜ[R] m i)
    (x ⊗ₜ[R] m)

Tactic:
simp [piRight]

Premises used: TensorProduct.piRight
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x : N
i : ι
m : M i
⊢ Eq (α := N ⊗[R] ((i : ι) → M i))
    (((LinearEquiv.symm (piRight R S N M) :
            ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) ≃ₗ[S] N ⊗[R] ((i : ι) → M i)) :
          (a : (i : ι) → N ⊗[R] M i) → N ⊗[R] ((i : ι) → M i))
        (Pi.single (M := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) i (x ⊗ₜ[R] m)) :
      N ⊗[R] ((i : ι) → M i))
    (x ⊗ₜ[R] Pi.single (M := M) i m : N ⊗[R] ((j : ι) → M j))

Tactic:
simp [piRight]

Premises used: TensorProduct.piRight
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
x y : N
h :
  ∀ (i : ι → R) (j : ι),
    Eq.{u_3 + 1} (α := N) ((LinearMap.compLeft (toSpanSingleton R N (x + y)) ι : (a : ι → R) → ι → N) i j : N)
      ((HAdd.hAdd (α := (ι → R) →ₗ[R] ι → N) (LinearMap.compLeft (toSpanSingleton R N x) ι)
              (LinearMap.compLeft (toSpanSingleton R N y) ι) :
            (a : ι → R) → ι → N)
          i j :
        N)
⊢ LinearMap.compLeft (toSpanSingleton R N (x + y)) ι =
    HAdd.hAdd (α := (ι → R) →ₗ[R] ι → N) (LinearMap.compLeft (toSpanSingleton R N x) ι)
      (LinearMap.compLeft (toSpanSingleton R N y) ι)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
x y : N
i : ι → R
j : ι
⊢ Eq.{u_3 + 1} (α := N) ((LinearMap.compLeft (toSpanSingleton R N (x + y)) ι : (a : ι → R) → ι → N) i j : N)
    ((HAdd.hAdd (α := (ι → R) →ₗ[R] ι → N) (LinearMap.compLeft (toSpanSingleton R N x) ι)
            (LinearMap.compLeft (toSpanSingleton R N y) ι) :
          (a : ι → R) → ι → N)
        i j :
      N)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
s : S
x : N
h :
  ∀ (i : ι → R) (j : ι),
    Eq.{u_3 + 1} (α := N) ((LinearMap.compLeft (toSpanSingleton R N (s • x)) ι : (a : ι → R) → ι → N) i j : N)
      ((HSMul.hSMul (α := S) (β := (ι → R) →ₗ[R] ι → N) ((RingHom.id S : (a : S) → S) s : S)
              (LinearMap.compLeft (toSpanSingleton R N x) ι) :
            (a : ι → R) → ι → N)
          i j :
        N)
⊢ LinearMap.compLeft (toSpanSingleton R N (s • x)) ι =
    HSMul.hSMul (α := S) (β := (ι → R) →ₗ[R] ι → N) ((RingHom.id S : (a : S) → S) s : S)
      (LinearMap.compLeft (toSpanSingleton R N x) ι)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
h : i j • s • x = s • i j • x
⊢ Eq.{u_3 + 1} (α := N) ((LinearMap.compLeft (toSpanSingleton R N (s • x)) ι : (a : ι → R) → ι → N) i j : N)
    ((HSMul.hSMul (α := S) (β := (ι → R) →ₗ[R] ι → N) ((RingHom.id S : (a : S) → S) s : S)
            (LinearMap.compLeft (toSpanSingleton R N x) ι) :
          (a : ι → R) → ι → N)
        i j :
      N)

Tactic:
dsimp only [coe_comp, coe_single, Function.comp_apply, compLeft_apply, toSpanSingleton_apply,
      RingHom.id_apply, smul_apply, Pi.smul_apply]

Premises used: RingHom.id_apply, LinearMap.smul_apply, LinearMap.toSpanSingleton_apply, LinearMap.compLeft_apply, LinearMap.coe_comp, LinearMap.coe_single, Function.comp_apply, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
h : s • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) (i j) : S) x = s • i j • x
⊢ i j • s • x = s • i j • x

Tactic:
rw [← IsScalarTower.smul_assoc, _root_.Algebra.smul_def, mul_comm, mul_smul]

Premises used: mul_comm, Algebra.smul_def, SemigroupAction.mul_smul, IsScalarTower.smul_assoc
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
s : S
x : N
i : ι → R
j : ι
⊢ s • HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) (i j) : S) x = s • i j • x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
x : N
f : ι → R
h :
  ∀ (j : ι),
    ((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) : (a : N ⊗[R] (ι → R)) → ι → N) (x ⊗ₜ[R] f) j = f j • x
⊢ Eq (α := ι → N)
    (((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) : (a : N ⊗[R] (ι → R)) → ι → N) (x ⊗ₜ[R] f) : ι → N)
    fun (j : ι) ↦ f j • x

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
x : N
f : ι → R
j : ι
⊢ ((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) : (a : N ⊗[R] (ι → R)) → ι → N) (x ⊗ₜ[R] f) j = f j • x

Tactic:
simp [piScalarRightHom, piScalarRightHomBil]

Premises used: TensorProduct.piScalarRightHom, TensorProduct.piScalarRightHomBil
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
i : ι
x y : N
⊢ (x + y) ⊗ₜ[R] Pi.single (M := fun (a : ι) ↦ R) i 1 =
    HAdd.hAdd (α := N ⊗[R] (ι → R)) (x ⊗ₜ[R] Pi.single (M := fun (a : ι) ↦ R) i 1)
      (y ⊗ₜ[R] Pi.single (M := fun (a : ι) ↦ R) i 1)

Tactic:
simp [add_tmul]

Premises used: TensorProduct.add_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
x : N
i : ι
⊢ Eq (α := N ⊗[R] (ι → R))
    (((piScalarRightInv R S N ι : (ι → N) →ₗ[S] N ⊗[R] (ι → R)) : (a : ι → N) → N ⊗[R] (ι → R))
        (Pi.single (M := fun (a : ι) ↦ N) i x) :
      N ⊗[R] (ι → R))
    (x ⊗ₜ[R] Pi.single (M := fun (j : ι) ↦ R) i 1 : N ⊗[R] ((j : ι) → R))

Tactic:
simp [piScalarRightInv, Pi.single_apply, TensorProduct.ite_tmul]

Premises used: Pi.single_apply, TensorProduct.piScalarRightInv, TensorProduct.ite_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
h :
  ∀ (i : ι) (x : N) (j : ι),
    Eq.{u_3 + 1} (α := N)
      ((((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) ∘ₗ
                (piScalarRightInv R S N ι : (ι → N) →ₗ[S] N ⊗[R] (ι → R))) ∘ₗ
              single.{u_2, u_4, u_3} S (fun (i : ι) ↦ N) i :
            (a : N) → ι → N)
          x j :
        N)
      (((LinearMap.id ∘ₗ single.{u_2, u_4, u_3} S (fun (i : ι) ↦ N) i : N →ₗ[S] ι → N) : (a : N) → ι → N) x j : N)
⊢ Eq (α := (ι → N) →ₗ[S] ι → N)
    ((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) ∘ₗ
      (piScalarRightInv R S N ι : (ι → N) →ₗ[S] N ⊗[R] (ι → R)))
    LinearMap.id

Tactic:
ext i x j
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
i : ι
x : N
j : ι
⊢ Eq.{u_3 + 1} (α := N)
    ((((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) ∘ₗ
              (piScalarRightInv R S N ι : (ι → N) →ₗ[S] N ⊗[R] (ι → R))) ∘ₗ
            single.{u_2, u_4, u_3} S (fun (i : ι) ↦ N) i :
          (a : N) → ι → N)
        x j :
      N)
    (((LinearMap.id ∘ₗ single.{u_2, u_4, u_3} S (fun (i : ι) ↦ N) i : N →ₗ[S] ι → N) : (a : N) → ι → N) x j : N)

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
a :
  ∀ (x : N) (i : ι),
    Eq (α := N ⊗[R] (ι → R))
      (((((AlgebraTensorModule.curry (piScalarRightInv R S N ι ∘ₗ piScalarRightHom R S N ι) :
                    N →ₗ[S] (ι → R) →ₗ[R] N ⊗[R] (ι → R)) :
                  (a : N) → (ι → R) →ₗ[R] N ⊗[R] (ι → R))
                x ∘ₗ
              single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] N ⊗[R] (ι → R)) :
          (a : R) → N ⊗[R] (ι → R))
        1)
      (((((AlgebraTensorModule.curry LinearMap.id : N →ₗ[S] (ι → R) →ₗ[R] N ⊗[R] (ι → R)) :
                  (a : N) → (ι → R) →ₗ[R] N ⊗[R] (ι → R))
                x ∘ₗ
              single R (fun (i : ι) ↦ R) i :
            R →ₗ[R] N ⊗[R] (ι → R)) :
          (a : R) → N ⊗[R] (ι → R))
        1)
⊢ Eq (α := N ⊗[R] (ι → R) →ₗ[S] N ⊗[R] (ι → R))
    (piScalarRightInv R S N ι ∘ₗ piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] N ⊗[R] (ι → R))
    (LinearMap.id : N ⊗[R] (ι → R) →ₗ[S] N ⊗[R] (ι → R))

Tactic:
ext x i
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
x : N
i : ι
⊢ Eq (α := N ⊗[R] (ι → R))
    (((((AlgebraTensorModule.curry (piScalarRightInv R S N ι ∘ₗ piScalarRightHom R S N ι) :
                  N →ₗ[S] (ι → R) →ₗ[R] N ⊗[R] (ι → R)) :
                (a : N) → (ι → R) →ₗ[R] N ⊗[R] (ι → R))
              x ∘ₗ
            single R (fun (i : ι) ↦ R) i :
          R →ₗ[R] N ⊗[R] (ι → R)) :
        (a : R) → N ⊗[R] (ι → R))
      1)
    (((((AlgebraTensorModule.curry LinearMap.id : N →ₗ[S] (ι → R) →ₗ[R] N ⊗[R] (ι → R)) :
                (a : N) → (ι → R) →ₗ[R] N ⊗[R] (ι → R))
              x ∘ₗ
            single R (fun (i : ι) ↦ R) i :
          R →ₗ[R] N ⊗[R] (ι → R)) :
        (a : R) → N ⊗[R] (ι → R))
      1)

Tactic:
simp [Pi.single_apply_smul]

Premises used: Pi.single_apply_smul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
x : N ⊗[R] (ι → R)
⊢ Eq (α := ι → N) (((piScalarRight R S N ι : N ⊗[R] (ι → R) ≃ₗ[S] ι → N) : (a : N ⊗[R] (ι → R)) → ι → N) x : ι → N)
    (((piScalarRightHom R S N ι : N ⊗[R] (ι → R) →ₗ[S] ι → N) : (a : N ⊗[R] (ι → R)) → ι → N) x : ι → N)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Pi
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module S N
inst_6 : IsScalarTower R S N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
x : N
i : ι
⊢ Eq (α := N ⊗[R] (ι → R))
    (((LinearEquiv.symm (piScalarRight R S N ι) : (ι → N) ≃ₗ[S] N ⊗[R] (ι → R)) : (a : ι → N) → N ⊗[R] (ι → R))
        (Pi.single (M := fun (a : ι) ↦ N) i x) :
      N ⊗[R] (ι → R))
    (x ⊗ₜ[R] Pi.single (M := fun (j : ι) ↦ R) i 1 : N ⊗[R] ((j : ι) → R))

Tactic:
simp [piScalarRight]

Premises used: TensorProduct.piScalarRight
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
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₃
x : M₁
x_1 : M₂
⊢ Eq (α := M₁ ⊗[R] M₂)
    (((((AlgebraTensorModule.curry
                    (((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₁ ⊗[R] 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₃)) :
                          M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))) ∘ₗ
                      LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                  M₁ →ₗ[S] M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
              x :
            M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₂) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        x_1).1
    (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                  M₁ →ₗ[S] M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
              x :
            M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₂) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        x_1).1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
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₃
x : M₁
x_1 : M₂
⊢ Eq (α := M₁ ⊗[R] M₃)
    (((((AlgebraTensorModule.curry
                    (((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₁ ⊗[R] 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₃)) :
                          M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))) ∘ₗ
                      LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                  M₁ →ₗ[S] M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
              x :
            M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₂) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        x_1).2
    (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inl S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                  M₁ →ₗ[S] M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                (a : M₁) → M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
              x :
            M₂ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₂) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        x_1).2

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
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₃
x : M₁
x_1 : M₃
⊢ Eq (α := M₁ ⊗[R] M₂)
    (((((AlgebraTensorModule.curry
                    (((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₁ ⊗[R] 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₃)) :
                          M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))) ∘ₗ
                      LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                  M₁ →ₗ[S] M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
              x :
            M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₃) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        x_1).1
    (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                  M₁ →ₗ[S] M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
              x :
            M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₃) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        x_1).1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Prod
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₃
x : M₁
x_1 : M₃
⊢ Eq (α := M₁ ⊗[R] M₃)
    (((((AlgebraTensorModule.curry
                    (((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₁ ⊗[R] 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₃)) :
                          M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃ →ₗ[S] M₁ ⊗[R] (M₂ × M₃))) ∘ₗ
                      LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                  M₁ →ₗ[S] M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
              x :
            M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₃) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        x_1).2
    (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ LinearMap.inr S (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃)) :
                  M₁ →ₗ[S] M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
                (a : M₁) → M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
              x :
            M₃ →ₗ[R] M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃) :
          (a : M₃) → M₁ ⊗[R] M₂ × M₁ ⊗[R] M₃)
        x_1).2

Tactic:
simp