awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
a : Aᵐᵒᵖ
b : Bᵐᵒᵖ
⊢ Eq (α := (A ⊗[R] B)ᵐᵒᵖ)
    (((opAlgEquiv R S A B : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ) :
          (a : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ) → (A ⊗[R] B)ᵐᵒᵖ)
        (a ⊗ₜ[R] b) :
      (A ⊗[R] B)ᵐᵒᵖ)
    (op (unop a ⊗ₜ[R] unop b) : (A ⊗[R] B)ᵐᵒᵖ)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, MulOpposite.unop, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl, MulOpposite.op
-- Module: Mathlib.LinearAlgebra.TensorProduct.Opposite
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra S A
inst_8 : IsScalarTower R S A
a : A
b : B
⊢ Eq (α := TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    (((AlgEquiv.symm (opAlgEquiv R S A B) : (A ⊗[R] B)ᵐᵒᵖ ≃ₐ[S] TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ) :
          (a : (A ⊗[R] B)ᵐᵒᵖ) → Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
        (op (a ⊗ₜ[R] b)) :
      TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)
    (op a ⊗ₜ[R] op b : TensorProduct.{u_1, u_3, u_4} R Aᵐᵒᵖ Bᵐᵒᵖ)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, MulOpposite.unop, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl, MulOpposite.op
-- 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)
x x_1 : N
h :
  ∀ (x_2 : (i : ι) → M i) (x_3 : ι),
    Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M x_3))
      ((pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
              (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) (x + x_1) ∘ₗ proj (φ := M) i :
            (a : (i : ι) → M i) → (i : ι) → N ⊗[R] M i)
          x_2 x_3 :
        TensorProduct.{u_1, u_3, u_5} R N (M x_3))
      ((HAdd.hAdd (α := ((i : ι) → M i) →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
              (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
                (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) x ∘ₗ proj (φ := M) i)
              (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
                (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) x_1 ∘ₗ proj (φ := M) i) :
            (a : (i : ι) → M i) → (i : ι) → N ⊗[R] M i)
          x_2 x_3 :
        TensorProduct.{u_1, u_3, u_5} R N (M x_3))
⊢ (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
      (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) (x + x_1) ∘ₗ proj (φ := M) i) =
    HAdd.hAdd (α := ((i : ι) → M i) →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
      (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
        (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) x ∘ₗ proj (φ := M) i)
      (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
        (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) x_1 ∘ₗ proj (φ := M) i)

Tactic:
ext
-- 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)
x x_1 : N
x_2 : (i : ι) → M i
x_3 : ι
⊢ Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M x_3))
    ((pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
            (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) (x + x_1) ∘ₗ proj (φ := M) i :
          (a : (i : ι) → M i) → (i : ι) → N ⊗[R] M i)
        x_2 x_3 :
      TensorProduct.{u_1, u_3, u_5} R N (M x_3))
    ((HAdd.hAdd (α := ((i : ι) → M i) →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
            (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
              (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) x ∘ₗ proj (φ := M) i)
            (pi (φ := fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) fun (i : ι) ↦
              (mk R N (M i) : (a : N) → M i →ₗ[R] N ⊗[R] M i) x_1 ∘ₗ proj (φ := M) i) :
          (a : (i : ι) → M i) → (i : ι) → N ⊗[R] M i)
        x_2 x_3 :
      TensorProduct.{u_1, u_3, u_5} R N (M x_3))

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
M : ι → Type u_5
inst_7 : (i : ι) → AddCommMonoid (M i)
inst_8 : (i : ι) → Module.{u_1, u_5} R (M i)
x : N
f : (i : ι) → M i
⊢ Eq (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
    (((piRightHom R S N M : N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
          (a : N ⊗[R] ((i : ι) → M i)) → (i : ι) → N ⊗[R] M i)
        (x ⊗ₜ[R] f) :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
    fun (j : ι) ↦ (x ⊗ₜ[R] f j : TensorProduct.{u_1, u_3, u_5} R N (M j))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, 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
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
simp : Eq (α := N ⊗[R] ((i : ι) → M i)) (∑ x_1 : ι, x ⊗ₜ[R] Pi.single (M := M) x_1 (m x_1)) (x ⊗ₜ[R] m)
⊢ Eq (α := N ⊗[R] ((i : ι) → M i))
    (((piRightInv 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 only [piRightInv, lsum_apply, coe_sum, coe_comp, coe_proj, Finset.sum_apply,
    Function.comp_apply, Function.eval, AlgebraTensorModule.map_tmul, id_coe, id_eq, coe_single]

Premises used: TensorProduct.piRightInv, LinearMap.id_coe, Finset.sum_apply, LinearMap.lsum_apply, LinearMap.coe_proj, LinearMap.coe_sum, Function.eval, LinearMap.coe_comp, LinearMap.coe_single, TensorProduct.AlgebraTensorModule.map_tmul, Function.comp_apply, id_eq
-- 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
rw : Eq (α := N ⊗[R] ((i : ι) → M i)) (x ⊗ₜ[R] ∑ a : ι, Pi.single (M := M) a (m a)) (x ⊗ₜ[R] m)
⊢ Eq (α := N ⊗[R] ((i : ι) → M i)) (∑ x_1 : ι, x ⊗ₜ[R] Pi.single (M := M) x_1 (m x_1)) (x ⊗ₜ[R] m)

Tactic:
rw [← tmul_sum]

Premises used: TensorProduct.tmul_sum
-- 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
e_n : ∑ a : ι, Pi.single (M := M) a (m a) = m
⊢ Eq (α := N ⊗[R] ((i : ι) → M i)) (x ⊗ₜ[R] ∑ a : ι, Pi.single (M := M) a (m a)) (x ⊗ₜ[R] m)

Tactic:
congr
-- 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
e_n : ∀ (j : ι), (∑ a : ι, Pi.single (M := M) a (m a)) j = m j
⊢ ∑ a : ι, Pi.single (M := M) a (m a) = m

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
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
j : ι
⊢ (∑ a : ι, Pi.single (M := M) a (m a)) j = m j

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
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
h :
  ∀ (j : ι),
    Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M j))
      (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i
          (x ⊗ₜ[R] m : TensorProduct.{u_1, u_3, u_5} R N (M i)) j :
        TensorProduct.{u_1, u_3, u_5} R N (M j))
      (x ⊗ₜ[R] Pi.single (M := M) i m j : TensorProduct.{u_1, u_3, u_5} R N (M j))
⊢ Eq (α := (j : ι) → TensorProduct.{u_1, u_3, u_5} R N (M j))
    (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i (x ⊗ₜ[R] m)) fun (j : ι) ↦
    x ⊗ₜ[R] Pi.single (M := M) i m j

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
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
j : ι
h h₁ :
  Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M j)) (x ⊗ₜ[R] Pi.single (M := M) i m j)
    (x ⊗ₜ[R] Pi.single (M := M) i m j)
⊢ Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M j))
    (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i
        (x ⊗ₜ[R] m : TensorProduct.{u_1, u_3, u_5} R N (M i)) j :
      TensorProduct.{u_1, u_3, u_5} R N (M j))
    (x ⊗ₜ[R] Pi.single (M := M) i m j : TensorProduct.{u_1, u_3, u_5} R N (M j))

Tactic:
rw [← tmul_single]

Premises used: TensorProduct.tmul_single
-- 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 (α := (j : ι) → TensorProduct.{u_1, u_3, u_5} R N (M j))
    (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i (x ⊗ₜ[R] m)) fun (j : ι) ↦
    x ⊗ₜ[R] Pi.single (M := M) i m j

Tactic:
have : Pi.single i (x ⊗ₜ m) = fun j ↦ x ⊗ₜ[R] (Pi.single i m j) := by
    ext j
    rw [← tmul_single]
-- 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
this :
  Eq (α := (j : ι) → TensorProduct.{u_1, u_3, u_5} R N (M j))
    (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i (x ⊗ₜ[R] m)) fun (j : ι) ↦
    x ⊗ₜ[R] Pi.single (M := M) i m j
rw :
  Eq (α := N ⊗[R] ((i : ι) → M i))
    (((piRightInv 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 (j : ι) ↦ x ⊗ₜ[R] Pi.single (M := M) i m j)
    (x ⊗ₜ[R] Pi.single (M := M) i m)
⊢ Eq (α := N ⊗[R] ((i : ι) → M i))
    (((piRightInv 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:
rw [this]
-- 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
this :
  Eq (α := (j : ι) → TensorProduct.{u_1, u_3, u_5} R N (M j))
    (Pi.single (M := fun (j : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M j)) i (x ⊗ₜ[R] m)) fun (j : ι) ↦
    x ⊗ₜ[R] Pi.single (M := M) i m j
⊢ Eq (α := N ⊗[R] ((i : ι) → M i))
    (((piRightInv 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 (j : ι) ↦ x ⊗ₜ[R] Pi.single (M := M) i m j)
    (x ⊗ₜ[R] Pi.single (M := M) i m)

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
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 ι
h :
  ∀ (i : ι) (x : N) (m : M i) (j : ι),
    Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M j))
      (((((AlgebraTensorModule.curry
                      (((piRightHom R S N M :
                              N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) ∘ₗ
                            (piRightInv R S N M :
                              ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) :
                          ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S]
                            (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) ∘ₗ
                        (single S (fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) i :
                          TensorProduct.{u_1, u_3, u_5} R N (M i) →ₗ[S]
                            (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))) :
                    N →ₗ[S] M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
                  (a : N) → M i →ₗ[R] (i : ι) → N ⊗[R] M i)
                x :
              M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
            (a : M i) → (i : ι) → N ⊗[R] M i)
          m j :
        TensorProduct.{u_1, u_3, u_5} R N (M j))
      (((((AlgebraTensorModule.curry
                      (LinearMap.id ∘ₗ single S (fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) i) :
                    N →ₗ[S] M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
                  (a : N) → M i →ₗ[R] (i : ι) → N ⊗[R] M i)
                x :
              M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
            (a : M i) → (i : ι) → N ⊗[R] M i)
          m j :
        TensorProduct.{u_1, u_3, u_5} R N (M j))
⊢ Eq (α := ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
    ((piRightHom R S N M : N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) ∘ₗ
        (piRightInv R S N M : ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) :
      ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
    (LinearMap.id :
      ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))

Tactic:
ext i x m 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
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 ι
i : ι
x : N
m : M i
j : ι
⊢ Eq (α := TensorProduct.{u_1, u_3, u_5} R N (M j))
    (((((AlgebraTensorModule.curry
                    (((piRightHom R S N M :
                            N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) ∘ₗ
                          (piRightInv R S N M :
                            ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) :
                        ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S]
                          (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) ∘ₗ
                      (single S (fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) i :
                        TensorProduct.{u_1, u_3, u_5} R N (M i) →ₗ[S]
                          (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))) :
                  N →ₗ[S] M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
                (a : N) → M i →ₗ[R] (i : ι) → N ⊗[R] M i)
              x :
            M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
          (a : M i) → (i : ι) → N ⊗[R] M i)
        m j :
      TensorProduct.{u_1, u_3, u_5} R N (M j))
    (((((AlgebraTensorModule.curry
                    (LinearMap.id ∘ₗ single S (fun (i : ι) ↦ TensorProduct.{u_1, u_3, u_5} R N (M i)) i) :
                  N →ₗ[S] M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
                (a : N) → M i →ₗ[R] (i : ι) → N ⊗[R] M i)
              x :
            M i →ₗ[R] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
          (a : M i) → (i : ι) → N ⊗[R] M i)
        m j :
      TensorProduct.{u_1, u_3, u_5} R N (M j))

Tactic:
simp [tmul_single]

Premises used: TensorProduct.tmul_single
-- 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 ι
a :
  ∀ (x : N) (j : ι) (m : M j),
    Eq (α := N ⊗[R] ((i : ι) → M i))
      ((((AlgebraTensorModule.curry
                      ((piRightInv R S N M :
                          ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) ∘ₗ
                        (piRightHom R S N M :
                          N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))) :
                    N →ₗ[S] ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i)) :
                  (a : N) → ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i))
                x ∘ₗ
              single R M j :
            (a : M j) → N ⊗[R] ((i : ι) → M i))
          m :
        N ⊗[R] ((i : ι) → M i))
      ((((AlgebraTensorModule.curry LinearMap.id : N →ₗ[S] ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i)) :
                  (a : N) → ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i))
                x ∘ₗ
              single R M j :
            (a : M j) → N ⊗[R] ((i : ι) → M i))
          m :
        N ⊗[R] ((i : ι) → M i))
⊢ Eq (α := N ⊗[R] ((i : ι) → M i) →ₗ[S] N ⊗[R] ((i : ι) → M i))
    ((piRightInv R S N M : ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) ∘ₗ
        (piRightHom R S N M : N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
      N ⊗[R] ((i : ι) → M i) →ₗ[S] N ⊗[R] ((i : ι) → M i))
    (LinearMap.id : N ⊗[R] ((i : ι) → M i) →ₗ[S] N ⊗[R] ((i : ι) → M i))

Tactic:
ext x j m
-- 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
j : ι
m : M j
⊢ Eq (α := N ⊗[R] ((i : ι) → M i))
    ((((AlgebraTensorModule.curry
                    ((piRightInv R S N M :
                        ((i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) →ₗ[S] N ⊗[R] ((i : ι) → M i)) ∘ₗ
                      (piRightHom R S N M :
                        N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))) :
                  N →ₗ[S] ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i)) :
                (a : N) → ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i))
              x ∘ₗ
            single R M j :
          (a : M j) → N ⊗[R] ((i : ι) → M i))
        m :
      N ⊗[R] ((i : ι) → M i))
    ((((AlgebraTensorModule.curry LinearMap.id : N →ₗ[S] ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i)) :
                (a : N) → ((i : ι) → M i) →ₗ[R] N ⊗[R] ((i : ι) → M i))
              x ∘ₗ
            single R M j :
          (a : M j) → N ⊗[R] ((i : ι) → M i))
        m :
      N ⊗[R] ((i : ι) → M i))

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
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 ⊗[R] ((i : ι) → M i)
⊢ Eq (α := (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
    (((piRight R S N M : N ⊗[R] ((i : ι) → M i) ≃ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
          (a : N ⊗[R] ((i : ι) → M i)) → (i : ι) → N ⊗[R] M i)
        x :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))
    (((piRightHom R S N M : N ⊗[R] ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i)) :
          (a : N ⊗[R] ((i : ι) → M i)) → (i : ι) → N ⊗[R] M i)
        x :
      (i : ι) → TensorProduct.{u_1, u_3, u_5} R N (M i))

Tactic:
rfl