awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
r : R
m : M
⊢ Eq (α := R ⊗[R] M)
    (((mk R R M : (a : R) → M →ₗ[R] R ⊗[R] M) 1 ∘ₗ lift (LinearMap.lsmul R M) : (a : R ⊗[R] M) → R ⊗[R] M) (r ⊗ₜ[R] m) :
      R ⊗[R] M)
    ((LinearMap.id : (a : R ⊗[R] M) → R ⊗[R] M) (r ⊗ₜ[R] m) : R ⊗[R] M)

Tactic:
simp [← tmul_smul, ← smul_tmul, smul_eq_mul, mul_one]

Premises used: TensorProduct.smul_tmul, TensorProduct.tmul_smul, smul_eq_mul, mul_one
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
r : R
⊢ (TensorProduct.lid R M : (a : R ⊗[R] M) → M) (r ⊗ₜ[R] m) = r • m

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ Eq (α := R ⊗[R] M) ((LinearEquiv.symm (TensorProduct.lid R M) : (a : M) → R ⊗[R] M) m : R ⊗[R] M)
    (1 ⊗ₜ[R] m : R ⊗[R] M)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := M →ₗ[R] R ⊗[R] M) (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M)
    ((mk R R M : (a : R) → M →ₗ[R] R ⊗[R] M) 1)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_11
inst_3 : Semiring S
inst_4 : Algebra R S
m : R ⊗[R] M
this :
  ∀ (m : M),
    Eq (α := S ⊗[R] M)
      ((LinearMap.rTensor M (AlgHom.toLinearMap (Algebra.algHom R R S)) ∘ₗ
              (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M) :
            (a : M) → S ⊗[R] M)
          m :
        S ⊗[R] M)
      (1 ⊗ₜ[R] m : S ⊗[R] M)
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] (TensorProduct.lid R M : (a : R ⊗[R] M) → M) m : S ⊗[R] M)
    ((LinearMap.rTensor M (AlgHom.toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] M) → S ⊗[R] M) m : S ⊗[R] M)

Tactic:
simp [← this]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_11
inst_3 : Semiring S
inst_4 : Algebra R S
m : R ⊗[R] M
suffices :
  ∀ (m : M),
    Eq (α := S ⊗[R] M)
      ((LinearMap.rTensor M (AlgHom.toLinearMap (Algebra.algHom R R S)) ∘ₗ
              (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M) :
            (a : M) → S ⊗[R] M)
          m :
        S ⊗[R] M)
      (1 ⊗ₜ[R] m : S ⊗[R] M)
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] (TensorProduct.lid R M : (a : R ⊗[R] M) → M) m : S ⊗[R] M)
    ((LinearMap.rTensor M (AlgHom.toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] M) → S ⊗[R] M) m : S ⊗[R] M)

Tactic:
suffices ∀ m, (LinearMap.rTensor M (Algebra.algHom R R S).toLinearMap).comp
    (TensorProduct.lid R M).symm.toLinearMap m = 1 ⊗ₜ[R] m by
    simp [← this]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_11
inst_3 : Semiring S
inst_4 : Algebra R S
m : R ⊗[R] M
m_1 : M
⊢ Eq (α := S ⊗[R] M)
    ((LinearMap.rTensor M (AlgHom.toLinearMap (Algebra.algHom R R S)) ∘ₗ
            (↑(LinearEquiv.symm (TensorProduct.lid R M)) : M →ₗ[R] R ⊗[R] M) :
          (a : M) → S ⊗[R] M)
        m_1 :
      S ⊗[R] M)
    (1 ⊗ₜ[R] m_1 : S ⊗[R] M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
h :
  ∀ (x : M),
    Eq (α := M ⊗[R] R)
      ((((LinearMap.compr₂ₛₗ (mk R M R)
                  ((LinearMap.flip (mk R M R) : (a : R) → M →ₗ[R] M ⊗[R] R) 1 ∘ₗ
                    lift (LinearMap.flip (LinearMap.lsmul R M))) :
                (a : M) → R →ₗ[R] M ⊗[R] R)
              x :
            R →ₗ[R] M ⊗[R] R) :
          (a : R) → M ⊗[R] R)
        1)
      ((((LinearMap.compr₂ₛₗ (mk R M R) LinearMap.id : (a : M) → R →ₗ[R] M ⊗[R] R) x : R →ₗ[R] M ⊗[R] R) :
          (a : R) → M ⊗[R] R)
        1)
⊢ Eq (α := M →ₗ[R] R →ₗ[R] M ⊗[R] R)
    (LinearMap.compr₂ₛₗ (mk R M R)
      ((LinearMap.flip (mk R M R) : (a : R) → M →ₗ[R] M ⊗[R] R) 1 ∘ₗ lift (LinearMap.flip (LinearMap.lsmul R M))))
    (LinearMap.compr₂ₛₗ (mk R M R) LinearMap.id)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
x : M
⊢ Eq (α := M ⊗[R] R)
    ((((LinearMap.compr₂ₛₗ (mk R M R)
                ((LinearMap.flip (mk R M R) : (a : R) → M →ₗ[R] M ⊗[R] R) 1 ∘ₗ
                  lift (LinearMap.flip (LinearMap.lsmul R M))) :
              (a : M) → R →ₗ[R] M ⊗[R] R)
            x :
          R →ₗ[R] M ⊗[R] R) :
        (a : R) → M ⊗[R] R)
      1)
    ((((LinearMap.compr₂ₛₗ (mk R M R) LinearMap.id : (a : M) → R →ₗ[R] M ⊗[R] R) x : R →ₗ[R] M ⊗[R] R) :
        (a : R) → M ⊗[R] R)
      1)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
r : R
⊢ (TensorProduct.rid R M : (a : M ⊗[R] R) → M) (m ⊗ₜ[R] r) = r • m

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
m : M
⊢ Eq (α := M ⊗[R] R) ((LinearEquiv.symm (TensorProduct.rid R M) : (a : M) → M ⊗[R] R) m : M ⊗[R] R)
    (m ⊗ₜ[R] 1 : M ⊗[R] R)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := M →ₗ[R] M ⊗[R] R) (↑(LinearEquiv.symm (TensorProduct.rid R M)) : M →ₗ[R] M ⊗[R] R)
    ((LinearMap.flip (mk R M R) : (a : R) → M →ₗ[R] M ⊗[R] R) 1)

Tactic:
rfl

Premises used: TensorProduct.tmul, AddCon.toQuotient, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (x : M),
    Eq.{u_5 + 1} (α := M)
      ((((LinearMap.compr₂ₛₗ (mk R M R) (↑(TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M) : M ⊗[R] R →ₗ[R] M) :
                  (a : M) → R →ₗ[R] M)
                x :
              R →ₗ[R] M) :
            (a : R) → M)
          1 :
        M)
      ((((LinearMap.compr₂ₛₗ (mk R M R) (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M) : (a : M) → R →ₗ[R] M) x :
              R →ₗ[R] M) :
            (a : R) → M)
          1 :
        M)
⊢ Eq (α := M →ₗ[R] R →ₗ[R] M)
    (LinearMap.compr₂ₛₗ (mk R M R) (↑(TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M) : M ⊗[R] R →ₗ[R] M))
    (LinearMap.compr₂ₛₗ (mk R M R) (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq.{u_5 + 1} (α := M)
    ((((LinearMap.compr₂ₛₗ (mk R M R) (↑(TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M) : M ⊗[R] R →ₗ[R] M) :
                (a : M) → R →ₗ[R] M)
              x :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)
    ((((LinearMap.compr₂ₛₗ (mk R M R) (↑(TensorProduct.rid R M) : M ⊗[R] R →ₗ[R] M) : (a : M) → R →ₗ[R] M) x :
            R →ₗ[R] M) :
          (a : R) → M)
        1 :
      M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
h :
  ∀ (x : M),
    Eq (α := M)
      (((LinearMap.compr₂ₛₗ (mk R R M) (↑(TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M) : R ⊗[R] M →ₗ[R] M) :
                (a : R) → M →ₗ[R] M)
              1 :
            (a : M) → M)
          x :
        M)
      (((LinearMap.compr₂ₛₗ (mk R R M) (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) : (a : R) → M →ₗ[R] M) 1 :
            (a : M) → M)
          x :
        M)
⊢ Eq (α := LinearMap.{u_1, u_1, u_1, u_5} (RingHom.id R) R (M →ₗ[R] M))
    (LinearMap.compr₂ₛₗ (mk R R M) (↑(TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M) : R ⊗[R] M →ₗ[R] M))
    (LinearMap.compr₂ₛₗ (mk R R M) (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
⊢ Eq (α := M)
    (((LinearMap.compr₂ₛₗ (mk R R M) (↑(TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M) : R ⊗[R] M →ₗ[R] M) :
              (a : R) → M →ₗ[R] M)
            1 :
          (a : M) → M)
        x :
      M)
    (((LinearMap.compr₂ₛₗ (mk R R M) (↑(TensorProduct.lid R M) : R ⊗[R] M →ₗ[R] M) : (a : R) → M →ₗ[R] M) 1 :
          (a : M) → M)
        x :
      M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := R ⊗[R] R ≃ₗ[R] R) (TensorProduct.lid R R) (TensorProduct.rid R R)

Tactic:
LinearEquiv.toLinearMap_injective <| ext' mul_comm

Premises used: LinearEquiv.toLinearMap_injective, mul_comm, TensorProduct.ext'
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_4
M : Type u_5
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring A
inst_4 : Module A M
inst_5 : Module R A
inst_6 : SMulCommClass R A A
inst_7 : CompatibleSMul R A A M
inst_8 : CompatibleSMul A R A M
a : A
m : M
⊢ (lidOfCompatibleSMul R A M : (a : A ⊗[R] M) → M) (a ⊗ₜ[R] m) = a • m

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
A : Type u_11
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A M
inst_8 : IsScalarTower R A M
inst_9 : Module A N
inst_10 : IsScalarTower R A N
h : Function.Surjective.{u_1 + 1, u_11 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
a : A
m : M
n : N
obtain :
  ∀ (r : R),
    Eq (α := M ⊗[R] N) (HSMul.hSMul.{u_11, u_5, u_5} (α := A) ((algebraMap R A : (a : R) → A) r : A) m ⊗ₜ[R] n)
      (m ⊗ₜ[R] HSMul.hSMul.{u_11, u_6, u_6} (α := A) ((algebraMap R A : (a : R) → A) r : A) n)
⊢ Eq (α := M ⊗[R] N) ((a • m) ⊗ₜ[R] n) (m ⊗ₜ[R] (a • n))

Tactic:
obtain ⟨r, rfl⟩ := h a

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
A : Type u_11
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A M
inst_8 : IsScalarTower R A M
inst_9 : Module A N
inst_10 : IsScalarTower R A N
h : Function.Surjective.{u_1 + 1, u_11 + 1} (α := R) (β := A) (⇑(algebraMap R A) : (a : R) → A)
m : M
n : N
r : R
⊢ Eq (α := M ⊗[R] N) (HSMul.hSMul.{u_11, u_5, u_5} (α := A) ((algebraMap R A : (a : R) → A) r : A) m ⊗ₜ[R] n)
    (m ⊗ₜ[R] HSMul.hSMul.{u_11, u_6, u_6} (α := A) ((algebraMap R A : (a : R) → A) r : A) n)

Tactic:
simp [smul_tmul]

Premises used: TensorProduct.CompatibleSMul.smul_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
H :
  ∀ (x : M) (x_1 : N) (x_2 : P),
    Eq (α := M ⊗[R] (N ⊗[R] P))
      ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                    ((compr₂ₛₗ (mk R M (N ⊗[R] P))
                          (lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) ∘ₗ
                            lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P))) :
                        (a : M) → N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P))
                      x) :
                  (a : N) → P →ₗ[R] M ⊗[R] (N ⊗[R] P))
                x_1 :
              P →ₗ[R] M ⊗[R] (N ⊗[R] P)) :
            (a : P) → M ⊗[R] (N ⊗[R] P))
          x_2 :
        M ⊗[R] (N ⊗[R] P))
      ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                    ((compr₂ₛₗ (mk R M (N ⊗[R] P)) LinearMap.id : (a : M) → N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) x) :
                  (a : N) → P →ₗ[R] M ⊗[R] (N ⊗[R] P))
                x_1 :
              P →ₗ[R] M ⊗[R] (N ⊗[R] P)) :
            (a : P) → M ⊗[R] (N ⊗[R] P))
          x_2 :
        M ⊗[R] (N ⊗[R] P))
⊢ Eq (α := M ⊗[R] (N ⊗[R] P) →ₗ[R] M ⊗[R] (N ⊗[R] P))
    (lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) ∘ₗ
      lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)))
    LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
x : M
x_1 : N
x_2 : P
⊢ Eq (α := M ⊗[R] (N ⊗[R] P))
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                  ((compr₂ₛₗ (mk R M (N ⊗[R] P))
                        (lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) ∘ₗ
                          lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P))) :
                      (a : M) → N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P))
                    x) :
                (a : N) → P →ₗ[R] M ⊗[R] (N ⊗[R] P))
              x_1 :
            P →ₗ[R] M ⊗[R] (N ⊗[R] P)) :
          (a : P) → M ⊗[R] (N ⊗[R] P))
        x_2 :
      M ⊗[R] (N ⊗[R] P))
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                  ((compr₂ₛₗ (mk R M (N ⊗[R] P)) LinearMap.id : (a : M) → N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) x) :
                (a : N) → P →ₗ[R] M ⊗[R] (N ⊗[R] P))
              x_1 :
            P →ₗ[R] M ⊗[R] (N ⊗[R] P)) :
          (a : P) → M ⊗[R] (N ⊗[R] P))
        x_2 :
      M ⊗[R] (N ⊗[R] P))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
H :
  ∀ (x : M) (x_1 : N) (x_2 : P),
    Eq (α := M ⊗[R] N ⊗[R] P)
      ((((((compr₂ₛₗ (mk R M N)
                          (compr₂ₛₗ (mk R (M ⊗[R] N) P)
                            (lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) ∘ₗ
                              lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))))) :
                        (a : M) → N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P)
                      x :
                    N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) :
                  (a : N) → P →ₗ[R] M ⊗[R] N ⊗[R] P)
                x_1 :
              P →ₗ[R] M ⊗[R] N ⊗[R] P) :
            (a : P) → M ⊗[R] N ⊗[R] P)
          x_2 :
        M ⊗[R] N ⊗[R] P)
      ((((((compr₂ₛₗ (mk R M N) (compr₂ₛₗ (mk R (M ⊗[R] N) P) LinearMap.id) : (a : M) → N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P)
                      x :
                    N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) :
                  (a : N) → P →ₗ[R] M ⊗[R] N ⊗[R] P)
                x_1 :
              P →ₗ[R] M ⊗[R] N ⊗[R] P) :
            (a : P) → M ⊗[R] N ⊗[R] P)
          x_2 :
        M ⊗[R] N ⊗[R] P)
⊢ Eq (α := M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] N ⊗[R] P)
    (lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) ∘ₗ
      lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))))
    LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
R' : Type u_2
inst_1 : Monoid R'
R'' : Type u_3
inst_2 : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid Q
inst_7 : AddCommMonoid S
inst_8 : AddCommMonoid T
inst_9 : Module R M
inst_10 : Module R N
inst_11 : Module R Q
inst_12 : Module R S
inst_13 : Module R T
inst_14 : DistribMulAction R' M
inst_15 : Module R'' M
inst_16 : Module R P
x : M
x_1 : N
x_2 : P
⊢ Eq (α := M ⊗[R] N ⊗[R] P)
    ((((((compr₂ₛₗ (mk R M N)
                        (compr₂ₛₗ (mk R (M ⊗[R] N) P)
                          (lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) ∘ₗ
                            lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))))) :
                      (a : M) → N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P)
                    x :
                  N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) :
                (a : N) → P →ₗ[R] M ⊗[R] N ⊗[R] P)
              x_1 :
            P →ₗ[R] M ⊗[R] N ⊗[R] P) :
          (a : P) → M ⊗[R] N ⊗[R] P)
        x_2 :
      M ⊗[R] N ⊗[R] P)
    ((((((compr₂ₛₗ (mk R M N) (compr₂ₛₗ (mk R (M ⊗[R] N) P) LinearMap.id) : (a : M) → N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P)
                    x :
                  N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) :
                (a : N) → P →ₗ[R] M ⊗[R] N ⊗[R] P)
              x_1 :
            P →ₗ[R] M ⊗[R] N ⊗[R] P) :
          (a : P) → M ⊗[R] N ⊗[R] P)
        x_2 :
      M ⊗[R] N ⊗[R] P)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
m : M
n : N
p : P
⊢ Eq (α := M ⊗[R] (N ⊗[R] P))
    ((TensorProduct.assoc R M N P : (a : M ⊗[R] N ⊗[R] P) → M ⊗[R] (N ⊗[R] P)) (m ⊗ₜ[R] n ⊗ₜ[R] p) : M ⊗[R] (N ⊗[R] P))
    (m ⊗ₜ[R] (n ⊗ₜ[R] p) : M ⊗[R] (N ⊗[R] P))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
m : M
n : N
p : P
⊢ Eq (α := M ⊗[R] N ⊗[R] P)
    ((LinearEquiv.symm (TensorProduct.assoc R M N P) : (a : M ⊗[R] (N ⊗[R] P)) → M ⊗[R] N ⊗[R] P)
        (m ⊗ₜ[R] (n ⊗ₜ[R] p)) :
      M ⊗[R] N ⊗[R] P)
    (m ⊗ₜ[R] n ⊗ₜ[R] p : M ⊗[R] N ⊗[R] P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : AddCommMonoid T
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R Q
inst_10 : Module R S
inst_11 : Module R T
inst_12 : Module R P
f : M →ₗ[R] Q
g : N →ₗ[R] S
h : P →ₗ[R] T
⊢ map f (map g h) ∘ₗ (↑(TensorProduct.assoc R M N P) : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)) =
    (↑(TensorProduct.assoc R Q S T) : Q ⊗[R] S ⊗[R] T →ₗ[R] Q ⊗[R] (S ⊗[R] T)) ∘ₗ map (map f g) h

Tactic:
ext <| ext <| LinearMap.ext fun _ => LinearMap.ext fun _ => LinearMap.ext fun _ => rfl

Premises used: LinearMap.ext, TensorProduct.ext, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : AddCommMonoid T
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R Q
inst_10 : Module R S
inst_11 : Module R T
inst_12 : Module R P
f : M →ₗ[R] Q
g : N →ₗ[R] S
h : P →ₗ[R] T
x : M ⊗[R] N ⊗[R] P
⊢ Eq (α := Q ⊗[R] (S ⊗[R] T))
    ((map f (map g h) : (a : M ⊗[R] (N ⊗[R] P)) → Q ⊗[R] (S ⊗[R] T))
        ((TensorProduct.assoc R M N P : (a : M ⊗[R] N ⊗[R] P) → M ⊗[R] (N ⊗[R] P)) x) :
      Q ⊗[R] (S ⊗[R] T))
    ((TensorProduct.assoc R Q S T : (a : Q ⊗[R] S ⊗[R] T) → Q ⊗[R] (S ⊗[R] T))
        ((map (map f g) h : (a : M ⊗[R] N ⊗[R] P) → Q ⊗[R] S ⊗[R] T) x) :
      Q ⊗[R] (S ⊗[R] T))

Tactic:
DFunLike.congr_fun (map_map_comp_assoc_eq _ _ _) _

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, TensorProduct.map_map_comp_assoc_eq
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : AddCommMonoid S
inst_6 : AddCommMonoid T
inst_7 : Module R M
inst_8 : Module R N
inst_9 : Module R Q
inst_10 : Module R S
inst_11 : Module R T
inst_12 : Module R P
f : M →ₗ[R] Q
g : N →ₗ[R] S
h : P →ₗ[R] T
⊢ map (map f g) h ∘ₗ (↑(LinearEquiv.symm (TensorProduct.assoc R M N P)) : M ⊗[R] (N ⊗[R] P) →ₗ[R] M ⊗[R] N ⊗[R] P) =
    (↑(LinearEquiv.symm (TensorProduct.assoc R Q S T)) : Q ⊗[R] (S ⊗[R] T) →ₗ[R] Q ⊗[R] S ⊗[R] T) ∘ₗ map f (map g h)

Tactic:
ext <| LinearMap.ext fun _ => ext <| LinearMap.ext fun _ => LinearMap.ext fun _ => rfl

Premises used: LinearMap.ext, TensorProduct.ext, rfl