awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (map f g) h : (a : M ⊗[R] N ⊗[R] P) → Q ⊗[R] S ⊗[R] T)
        ((LinearEquiv.symm (TensorProduct.assoc R M N P) : (a : M ⊗[R] (N ⊗[R] P)) → M ⊗[R] N ⊗[R] P) x) :
      Q ⊗[R] S ⊗[R] T)
    ((LinearEquiv.symm (TensorProduct.assoc R Q S T) : (a : Q ⊗[R] (S ⊗[R] T)) → Q ⊗[R] S ⊗[R] T)
        ((map f (map 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_symm_eq _ _ _) _

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, TensorProduct.map_map_comp_assoc_symm_eq
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
Q : Type u_8
S : Type u_9
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid Q
inst_4 : AddCommMonoid S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R S
⊢ Eq (α := M ⊗[R] N ⊗[R] Q ⊗[R] S ≃ₗ[R] M ⊗[R] N ⊗[R] (Q ⊗[R] S)) (TensorProduct.assoc R (M ⊗[R] N) Q S)
    (LinearEquiv.rTensor S (TensorProduct.assoc R M N Q) ≪≫ₗ TensorProduct.assoc R M (N ⊗[R] Q) S ≪≫ₗ
        LinearEquiv.lTensor M (TensorProduct.assoc R N Q S) ≪≫ₗ
      LinearEquiv.symm (TensorProduct.assoc R M N (Q ⊗[R] S)))

Tactic:
LinearEquiv.toLinearMap_inj.mp <| ext_fourfold fun _ _ _ => congrFun rfl

Premises used: LinearEquiv.toLinearMap_inj, congrFun, Iff.mp, rfl, TensorProduct.ext_fourfold
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
Q : Type u_8
S : Type u_9
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid Q
inst_4 : AddCommMonoid S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R S
⊢ Eq (α := M ⊗[R] (N ⊗[R] Q) ⊗[R] S ≃ₗ[R] M ⊗[R] (N ⊗[R] Q ⊗[R] S)) (TensorProduct.assoc R M (N ⊗[R] Q) S)
    (LinearEquiv.rTensor S (LinearEquiv.symm (TensorProduct.assoc R M N Q)) ≪≫ₗ TensorProduct.assoc R (M ⊗[R] N) Q S ≪≫ₗ
        TensorProduct.assoc R M N (Q ⊗[R] S) ≪≫ₗ
      LinearEquiv.lTensor M (LinearEquiv.symm (TensorProduct.assoc R N Q S)))

Tactic:
LinearEquiv.toLinearMap_inj.mp <| ext_fourfold'' fun _ _ _ => congrFun rfl

Premises used: LinearEquiv.toLinearMap_inj, TensorProduct.ext_fourfold'', congrFun, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_5
N : Type u_6
Q : Type u_8
S : Type u_9
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid Q
inst_4 : AddCommMonoid S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R S
⊢ Eq (α := M ⊗[R] N ⊗[R] (Q ⊗[R] S) ≃ₗ[R] M ⊗[R] (N ⊗[R] (Q ⊗[R] S))) (TensorProduct.assoc R M N (Q ⊗[R] S))
    (LinearEquiv.symm (TensorProduct.assoc R (M ⊗[R] N) Q S) ≪≫ₗ LinearEquiv.rTensor S (TensorProduct.assoc R M N Q) ≪≫ₗ
        TensorProduct.assoc R M (N ⊗[R] Q) S ≪≫ₗ
      LinearEquiv.lTensor M (TensorProduct.assoc R N Q S))

Tactic:
LinearEquiv.toLinearMap_inj.mp <| ext_fourfold' fun _ _ _ => congrFun rfl

Premises used: LinearEquiv.toLinearMap_inj, congrFun, Iff.mp, rfl, TensorProduct.ext_fourfold'
-- 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
⊢ Eq (α := R ⊗[R] (M ⊗[R] N) ≃ₗ[R] M ⊗[R] N) (TensorProduct.lid R (M ⊗[R] N))
    (LinearEquiv.symm (TensorProduct.assoc R R M N) ≪≫ₗ LinearEquiv.rTensor N (TensorProduct.lid R M))

Tactic:
LinearEquiv.toLinearMap_inj.mp <| ext_threefold' fun _ _ => congrFun rfl

Premises used: LinearEquiv.toLinearMap_inj, congrFun, Iff.mp, TensorProduct.ext_threefold', 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 (α := N ⊗[R] (M ⊗[R] P))
    ((leftComm R M N P : (a : M ⊗[R] (N ⊗[R] P)) → N ⊗[R] (M ⊗[R] P)) (m ⊗ₜ[R] (n ⊗ₜ[R] p)) : N ⊗[R] (M ⊗[R] P))
    (n ⊗ₜ[R] (m ⊗ₜ[R] p) : N ⊗[R] (M ⊗[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 (leftComm R M N P) : (a : N ⊗[R] (M ⊗[R] P)) → M ⊗[R] (N ⊗[R] P)) (n ⊗ₜ[R] (m ⊗ₜ[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
a :
  Eq (α := M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P)) (↑(leftComm R M N P) : M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P))
    (↑(LinearEquiv.symm (TensorProduct.assoc R M N P) ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
          TensorProduct.assoc R N M P) :
      M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P))
⊢ Eq (α := M ⊗[R] (N ⊗[R] P) ≃ₗ[R] N ⊗[R] (M ⊗[R] P)) (leftComm R M N P)
    (LinearEquiv.symm (TensorProduct.assoc R M N P) ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
      TensorProduct.assoc R N M P)

Tactic:
apply LinearEquiv.toLinearMap_injective

Premises used: LinearEquiv.toLinearMap_injective
-- 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
a :
  ∀ (x : M) (x_1 : N) (x_2 : P),
    Eq (α := N ⊗[R] (M ⊗[R] P))
      ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                    ((compr₂ₛₗ (mk R M (N ⊗[R] P)) (↑(leftComm R M N P) : M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
                        (a : M) → N ⊗[R] P →ₗ[R] N ⊗[R] (M ⊗[R] P))
                      x) :
                  (a : N) → P →ₗ[R] N ⊗[R] (M ⊗[R] P))
                x_1 :
              P →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
            (a : P) → N ⊗[R] (M ⊗[R] P))
          x_2 :
        N ⊗[R] (M ⊗[R] P))
      ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                    ((compr₂ₛₗ (mk R M (N ⊗[R] P))
                          (↑(LinearEquiv.symm (TensorProduct.assoc R M N P) ≪≫ₗ
                                  congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
                                TensorProduct.assoc R N M P) :
                            M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
                        (a : M) → N ⊗[R] P →ₗ[R] N ⊗[R] (M ⊗[R] P))
                      x) :
                  (a : N) → P →ₗ[R] N ⊗[R] (M ⊗[R] P))
                x_1 :
              P →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
            (a : P) → N ⊗[R] (M ⊗[R] P))
          x_2 :
        N ⊗[R] (M ⊗[R] P))
⊢ Eq (α := M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P)) (↑(leftComm R M N P) : M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P))
    (↑(LinearEquiv.symm (TensorProduct.assoc R M N P) ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
          TensorProduct.assoc R N M P) :
      M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P))

Tactic:
ext
-- 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
x : M
x_1 : N
x_2 : P
⊢ Eq (α := N ⊗[R] (M ⊗[R] P))
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                  ((compr₂ₛₗ (mk R M (N ⊗[R] P)) (↑(leftComm R M N P) : M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
                      (a : M) → N ⊗[R] P →ₗ[R] N ⊗[R] (M ⊗[R] P))
                    x) :
                (a : N) → P →ₗ[R] N ⊗[R] (M ⊗[R] P))
              x_1 :
            P →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
          (a : P) → N ⊗[R] (M ⊗[R] P))
        x_2 :
      N ⊗[R] (M ⊗[R] P))
    ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (mk R N P)
                  ((compr₂ₛₗ (mk R M (N ⊗[R] P))
                        (↑(LinearEquiv.symm (TensorProduct.assoc R M N P) ≪≫ₗ
                                congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
                              TensorProduct.assoc R N M P) :
                          M ⊗[R] (N ⊗[R] P) →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
                      (a : M) → N ⊗[R] P →ₗ[R] N ⊗[R] (M ⊗[R] P))
                    x) :
                (a : N) → P →ₗ[R] N ⊗[R] (M ⊗[R] P))
              x_1 :
            P →ₗ[R] N ⊗[R] (M ⊗[R] P)) :
          (a : P) → N ⊗[R] (M ⊗[R] P))
        x_2 :
      N ⊗[R] (M ⊗[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
P' : Type u_11
Q' : Type u_12
inst_17 : AddCommMonoid P'
inst_18 : Module R P'
inst_19 : AddCommMonoid Q'
inst_20 : Module R Q'
H :
  ∀ (x : M) (x_1 : P) (x_2 : N),
    Eq (α := M ⊗[R] P ⊗[R] N)
      ((((((compr₂ₛₗ (mk R M P)
                          (compr₂ₛₗ (mk R (M ⊗[R] P) N)
                            (lift
                                (lift
                                  ((↑lflip : (P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N) →ₗ[R] N →ₗ[R] P →ₗ[R] M ⊗[R] P ⊗[R] N) ∘ₗ
                                    compr₂ (mk R M P) (mk R (M ⊗[R] P) N))) ∘ₗ
                              lift
                                (lift
                                  ((↑lflip : (N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) →ₗ[R] P →ₗ[R] N →ₗ[R] M ⊗[R] N ⊗[R] P) ∘ₗ
                                    compr₂ (mk R M N) (mk R (M ⊗[R] N) P))))) :
                        (a : M) → P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N)
                      x :
                    P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N) :
                  (a : P) → N →ₗ[R] M ⊗[R] P ⊗[R] N)
                x_1 :
              N →ₗ[R] M ⊗[R] P ⊗[R] N) :
            (a : N) → M ⊗[R] P ⊗[R] N)
          x_2 :
        M ⊗[R] P ⊗[R] N)
      ((((((compr₂ₛₗ (mk R M P) (compr₂ₛₗ (mk R (M ⊗[R] P) N) LinearMap.id) : (a : M) → P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N)
                      x :
                    P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N) :
                  (a : P) → N →ₗ[R] M ⊗[R] P ⊗[R] N)
                x_1 :
              N →ₗ[R] M ⊗[R] P ⊗[R] N) :
            (a : N) → M ⊗[R] P ⊗[R] N)
          x_2 :
        M ⊗[R] P ⊗[R] N)
⊢ Eq (α := M ⊗[R] P ⊗[R] N →ₗ[R] M ⊗[R] P ⊗[R] N)
    (lift
        (lift
          ((↑lflip : (P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N) →ₗ[R] N →ₗ[R] P →ₗ[R] M ⊗[R] P ⊗[R] N) ∘ₗ
            compr₂ (mk R M P) (mk R (M ⊗[R] P) N))) ∘ₗ
      lift
        (lift
          ((↑lflip : (N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) →ₗ[R] P →ₗ[R] N →ₗ[R] M ⊗[R] N ⊗[R] P) ∘ₗ
            compr₂ (mk R M N) (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
P' : Type u_11
Q' : Type u_12
inst_17 : AddCommMonoid P'
inst_18 : Module R P'
inst_19 : AddCommMonoid Q'
inst_20 : Module R Q'
x : M
x_1 : P
x_2 : N
⊢ Eq (α := M ⊗[R] P ⊗[R] N)
    ((((((compr₂ₛₗ (mk R M P)
                        (compr₂ₛₗ (mk R (M ⊗[R] P) N)
                          (lift
                              (lift
                                ((↑lflip : (P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N) →ₗ[R] N →ₗ[R] P →ₗ[R] M ⊗[R] P ⊗[R] N) ∘ₗ
                                  compr₂ (mk R M P) (mk R (M ⊗[R] P) N))) ∘ₗ
                            lift
                              (lift
                                ((↑lflip : (N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) →ₗ[R] P →ₗ[R] N →ₗ[R] M ⊗[R] N ⊗[R] P) ∘ₗ
                                  compr₂ (mk R M N) (mk R (M ⊗[R] N) P))))) :
                      (a : M) → P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N)
                    x :
                  P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N) :
                (a : P) → N →ₗ[R] M ⊗[R] P ⊗[R] N)
              x_1 :
            N →ₗ[R] M ⊗[R] P ⊗[R] N) :
          (a : N) → M ⊗[R] P ⊗[R] N)
        x_2 :
      M ⊗[R] P ⊗[R] N)
    ((((((compr₂ₛₗ (mk R M P) (compr₂ₛₗ (mk R (M ⊗[R] P) N) LinearMap.id) : (a : M) → P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N)
                    x :
                  P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N) :
                (a : P) → N →ₗ[R] M ⊗[R] P ⊗[R] N)
              x_1 :
            N →ₗ[R] M ⊗[R] P ⊗[R] N) :
          (a : N) → M ⊗[R] P ⊗[R] N)
        x_2 :
      M ⊗[R] P ⊗[R] N)

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
P' : Type u_11
Q' : Type u_12
inst_17 : AddCommMonoid P'
inst_18 : Module R P'
inst_19 : AddCommMonoid Q'
inst_20 : Module R Q'
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
                                (lift
                                  ((↑lflip : (N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) →ₗ[R] P →ₗ[R] N →ₗ[R] M ⊗[R] N ⊗[R] P) ∘ₗ
                                    compr₂ (mk R M N) (mk R (M ⊗[R] N) P))) ∘ₗ
                              lift
                                (lift
                                  ((↑lflip : (P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N) →ₗ[R] N →ₗ[R] P →ₗ[R] M ⊗[R] P ⊗[R] N) ∘ₗ
                                    compr₂ (mk R M P) (mk R (M ⊗[R] P) N))))) :
                        (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
        (lift
          ((↑lflip : (N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) →ₗ[R] P →ₗ[R] N →ₗ[R] M ⊗[R] N ⊗[R] P) ∘ₗ
            compr₂ (mk R M N) (mk R (M ⊗[R] N) P))) ∘ₗ
      lift
        (lift
          ((↑lflip : (P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N) →ₗ[R] N →ₗ[R] P →ₗ[R] M ⊗[R] P ⊗[R] N) ∘ₗ
            compr₂ (mk R M P) (mk R (M ⊗[R] P) N))))
    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
P' : Type u_11
Q' : Type u_12
inst_17 : AddCommMonoid P'
inst_18 : Module R P'
inst_19 : AddCommMonoid Q'
inst_20 : Module R Q'
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
                              (lift
                                ((↑lflip : (N →ₗ[R] P →ₗ[R] M ⊗[R] N ⊗[R] P) →ₗ[R] P →ₗ[R] N →ₗ[R] M ⊗[R] N ⊗[R] P) ∘ₗ
                                  compr₂ (mk R M N) (mk R (M ⊗[R] N) P))) ∘ₗ
                            lift
                              (lift
                                ((↑lflip : (P →ₗ[R] N →ₗ[R] M ⊗[R] P ⊗[R] N) →ₗ[R] N →ₗ[R] P →ₗ[R] M ⊗[R] P ⊗[R] N) ∘ₗ
                                  compr₂ (mk R M P) (mk R (M ⊗[R] P) N))))) :
                      (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] P ⊗[R] N)
    ((rightComm R M N P : (a : M ⊗[R] N ⊗[R] P) → M ⊗[R] P ⊗[R] N) (m ⊗ₜ[R] n ⊗ₜ[R] p) : M ⊗[R] P ⊗[R] N)
    (m ⊗ₜ[R] p ⊗ₜ[R] n : M ⊗[R] P ⊗[R] N)

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
⊢ Eq (α := M ⊗[R] P ⊗[R] N ≃ₗ[R] M ⊗[R] N ⊗[R] P) (LinearEquiv.symm (rightComm R M N P)) (rightComm R M P N)

Tactic:
rfl

Premises used: LinearEquiv.symm, Quotient.liftOn', TensorProduct.rightComm, AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct, TensorProduct.lift, 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
a :
  Eq (α := M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] P ⊗[R] N) (↑(rightComm R M N P) : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] P ⊗[R] N)
    (↑(TensorProduct.assoc R M N P ≪≫ₗ congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
          LinearEquiv.symm (TensorProduct.assoc R M P N)) :
      M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] P ⊗[R] N)
⊢ Eq (α := M ⊗[R] N ⊗[R] P ≃ₗ[R] M ⊗[R] P ⊗[R] N) (rightComm R M N P)
    (TensorProduct.assoc R M N P ≪≫ₗ congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
      LinearEquiv.symm (TensorProduct.assoc R M P N))

Tactic:
apply LinearEquiv.toLinearMap_injective

Premises used: LinearEquiv.toLinearMap_injective
-- 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
a :
  ∀ (x : M) (x_1 : N) (x_2 : P),
    Eq (α := M ⊗[R] P ⊗[R] N)
      ((((((compr₂ₛₗ (mk R M N)
                          (compr₂ₛₗ (mk R (M ⊗[R] N) P)
                            (↑(rightComm R M N P) : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] P ⊗[R] N)) :
                        (a : M) → N →ₗ[R] P →ₗ[R] M ⊗[R] P ⊗[R] N)
                      x :
                    N →ₗ[R] P →ₗ[R] M ⊗[R] P ⊗[R] N) :
                  (a : N) → P →ₗ[R] M ⊗[R] P ⊗[R] N)
                x_1 :
              P →ₗ[R] M ⊗[R] P ⊗[R] N) :
            (a : P) → M ⊗[R] P ⊗[R] N)
          x_2 :
        M ⊗[R] P ⊗[R] N)
      ((((((compr₂ₛₗ (mk R M N)
                          (compr₂ₛₗ (mk R (M ⊗[R] N) P)
                            (↑(TensorProduct.assoc R M N P ≪≫ₗ
                                    congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
                                  LinearEquiv.symm (TensorProduct.assoc R M P N)) :
                              M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] P ⊗[R] N)) :
                        (a : M) → N →ₗ[R] P →ₗ[R] M ⊗[R] P ⊗[R] N)
                      x :
                    N →ₗ[R] P →ₗ[R] M ⊗[R] P ⊗[R] N) :
                  (a : N) → P →ₗ[R] M ⊗[R] P ⊗[R] N)
                x_1 :
              P →ₗ[R] M ⊗[R] P ⊗[R] N) :
            (a : P) → M ⊗[R] P ⊗[R] N)
          x_2 :
        M ⊗[R] P ⊗[R] N)
⊢ Eq (α := M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] P ⊗[R] N) (↑(rightComm R M N P) : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] P ⊗[R] N)
    (↑(TensorProduct.assoc R M N P ≪≫ₗ congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
          LinearEquiv.symm (TensorProduct.assoc R M P N)) :
      M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] P ⊗[R] N)

Tactic:
ext