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
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 (α := 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)

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
Q : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
m : M
n : N
p : P
q : Q
⊢ Eq (α := M ⊗[R] P ⊗[R] (N ⊗[R] Q))
    ((tensorTensorTensorComm R M N P Q : (a : M ⊗[R] N ⊗[R] (P ⊗[R] Q)) → M ⊗[R] P ⊗[R] (N ⊗[R] Q))
        (m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)) :
      M ⊗[R] P ⊗[R] (N ⊗[R] Q))
    (m ⊗ₜ[R] p ⊗ₜ[R] (n ⊗ₜ[R] q) : M ⊗[R] P ⊗[R] (N ⊗[R] Q))

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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
⊢ Eq (α := M ⊗[R] P ⊗[R] (N ⊗[R] Q) ≃ₗ[R] M ⊗[R] N ⊗[R] (P ⊗[R] Q))
    (LinearEquiv.symm (tensorTensorTensorComm R M N P Q)) (tensorTensorTensorComm R M P N Q)

Tactic:
rfl

Premises used: LinearEquiv.symm, Quotient.liftOn', AddCon.liftOn, TensorProduct.tensorTensorTensorComm, LinearEquiv.trans, 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
rw :
  Eq (α := M ⊗[R] N ⊗[R] (P ⊗[R] Q) ≃ₗ[R] M ⊗[R] N ⊗[R] (P ⊗[R] Q))
    (LinearEquiv.symm (tensorTensorTensorComm R M P N Q) ≪≫ₗ tensorTensorTensorComm R M P N Q)
    (LinearEquiv.refl R (M ⊗[R] N ⊗[R] (P ⊗[R] Q)))
⊢ Eq (α := M ⊗[R] N ⊗[R] (P ⊗[R] Q) ≃ₗ[R] M ⊗[R] N ⊗[R] (P ⊗[R] Q))
    (tensorTensorTensorComm R M N P Q ≪≫ₗ tensorTensorTensorComm R M P N Q)
    (LinearEquiv.refl R (M ⊗[R] N ⊗[R] (P ⊗[R] Q)))

Tactic:
rw [← tensorTensorTensorComm_symm]

Premises used: TensorProduct.tensorTensorTensorComm_symm
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
⊢ Eq (α := M ⊗[R] N ⊗[R] (P ⊗[R] Q) ≃ₗ[R] M ⊗[R] N ⊗[R] (P ⊗[R] Q))
    (LinearEquiv.symm (tensorTensorTensorComm R M P N Q) ≪≫ₗ tensorTensorTensorComm R M P N Q)
    (LinearEquiv.refl R (M ⊗[R] N ⊗[R] (P ⊗[R] Q)))

Tactic:
LinearEquiv.symm_trans_self _

Premises used: LinearEquiv.symm_trans_self
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
⊢ Eq (α := M ⊗[R] N ⊗[R] (P ⊗[R] Q) ≃ₗ[R] M ⊗[R] N ⊗[R] (P ⊗[R] Q))
    (LinearEquiv.symm (tensorTensorTensorComm R M P N Q) ≪≫ₗ tensorTensorTensorComm R M P N Q)
    (LinearEquiv.refl R (M ⊗[R] N ⊗[R] (P ⊗[R] Q)))

Tactic:
exact LinearEquiv.symm_trans_self _

Premises used: LinearEquiv.symm_trans_self
-- 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
V : Type u_13
W : Type u_14
inst_13 : AddCommMonoid V
inst_14 : AddCommMonoid W
inst_15 : Module R V
inst_16 : Module R W
f : M →ₗ[R] S
g : N →ₗ[R] T
h : P →ₗ[R] V
j : Q →ₗ[R] W
⊢ (↑(tensorTensorTensorComm R S T V W) : S ⊗[R] T ⊗[R] (V ⊗[R] W) →ₗ[R] S ⊗[R] V ⊗[R] (T ⊗[R] W)) ∘ₗ
      map (map f g) (map h j) =
    map (map f h) (map g j) ∘ₗ
      (↑(tensorTensorTensorComm R M N P Q) : M ⊗[R] N ⊗[R] (P ⊗[R] Q) →ₗ[R] M ⊗[R] P ⊗[R] (N ⊗[R] Q))

Tactic:
ext_fourfold' fun _ _ _ _ => rfl

Premises used: 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
P : Type u_7
Q : Type u_8
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
m : M
n : N
p : P
q : Q
⊢ Eq (α := M ⊗[R] (N ⊗[R] P) ⊗[R] Q)
    ((tensorTensorTensorAssoc R M N P Q : (a : M ⊗[R] N ⊗[R] (P ⊗[R] Q)) → M ⊗[R] (N ⊗[R] P) ⊗[R] Q)
        (m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q)) :
      M ⊗[R] (N ⊗[R] P) ⊗[R] Q)
    (m ⊗ₜ[R] (n ⊗ₜ[R] p) ⊗ₜ[R] q : M ⊗[R] (N ⊗[R] P) ⊗[R] Q)

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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
m : M
n : N
p : P
q : Q
⊢ Eq (α := M ⊗[R] N ⊗[R] (P ⊗[R] Q))
    ((LinearEquiv.symm (tensorTensorTensorAssoc R M N P Q) : (a : M ⊗[R] (N ⊗[R] P) ⊗[R] Q) → M ⊗[R] N ⊗[R] (P ⊗[R] Q))
        (m ⊗ₜ[R] (n ⊗ₜ[R] p) ⊗ₜ[R] q) :
      M ⊗[R] N ⊗[R] (P ⊗[R] Q))
    (m ⊗ₜ[R] n ⊗ₜ[R] (p ⊗ₜ[R] q) : M ⊗[R] N ⊗[R] (P ⊗[R] Q))

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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
f : P →ₗ[R] Q
⊢ Eq (α := M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] N ⊗[R] Q) (lTensor (M ⊗[R] N) f)
    ((↑(LinearEquiv.symm (assoc R M N Q)) : M ⊗[R] (N ⊗[R] Q) →ₗ[R] M ⊗[R] N ⊗[R] Q) ∘ₗ
      lTensor M (lTensor N f) ∘ₗ (↑(assoc R M N P) : M ⊗[R] N ⊗[R] P →ₗ[R] M ⊗[R] (N ⊗[R] P)))

Tactic:
TensorProduct.ext <| TensorProduct.ext rfl

Premises used: 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
g : P →ₗ[R] Q
⊢ Eq (α := P ⊗[R] (M ⊗[R] N) →ₗ[R] Q ⊗[R] (M ⊗[R] N)) (rTensor (M ⊗[R] N) g)
    ((↑(assoc R Q M N) : Q ⊗[R] M ⊗[R] N →ₗ[R] Q ⊗[R] (M ⊗[R] N)) ∘ₗ
      rTensor N (rTensor M g) ∘ₗ (↑(LinearEquiv.symm (assoc R P M N)) : P ⊗[R] (M ⊗[R] N) →ₗ[R] P ⊗[R] M ⊗[R] N))

Tactic:
TensorProduct.ext <| LinearMap.ext fun _ ↦ TensorProduct.ext 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
f : N →ₗ[R] R
⊢ Eq (α := N ⊗[R] M →ₗ[R] M) ((↑(lid R M) : R ⊗[R] M →ₗ[R] M) ∘ₗ rTensor M f) (lift (lsmul R M ∘ₗ f))

Tactic:
ext' fun _ _ ↦ rfl

Premises used: TensorProduct.ext', 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
f : M →ₗ[R] R
⊢ Eq (α := N ⊗[R] M →ₗ[R] N) ((↑(rid R N) : N ⊗[R] R →ₗ[R] N) ∘ₗ lTensor N f) (lift (compl₂ (flip (lsmul R N)) f))

Tactic:
ext' fun _ _ ↦ rfl

Premises used: 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
x : M →ₗ[R] N
simp_rw :
  Eq (α := P ⊗[R] M ⊗[R] Q →ₗ[R] P ⊗[R] (N ⊗[R] Q))
    (lTensor P (map x id) ∘ₗ (↑(assoc R P M Q) : P ⊗[R] M ⊗[R] Q →ₗ[R] P ⊗[R] (M ⊗[R] Q)))
    ((↑(assoc R P N Q) : P ⊗[R] N ⊗[R] Q →ₗ[R] P ⊗[R] (N ⊗[R] Q)) ∘ₗ map (lTensor P x) id)
simp_rw₁ :
  Eq (α := P ⊗[R] M ⊗[R] Q →ₗ[R] P ⊗[R] (N ⊗[R] Q))
    (map id (map x id) ∘ₗ (↑(assoc R P M Q) : P ⊗[R] M ⊗[R] Q →ₗ[R] P ⊗[R] (M ⊗[R] Q)))
    ((↑(assoc R P N Q) : P ⊗[R] N ⊗[R] Q →ₗ[R] P ⊗[R] (N ⊗[R] Q)) ∘ₗ map (map id x) id)
⊢ Eq (α := P ⊗[R] M ⊗[R] Q →ₗ[R] P ⊗[R] (N ⊗[R] Q))
    (lTensor P (rTensor Q x) ∘ₗ (↑(assoc R P M Q) : P ⊗[R] M ⊗[R] Q →ₗ[R] P ⊗[R] (M ⊗[R] Q)))
    ((↑(assoc R P N Q) : P ⊗[R] N ⊗[R] Q →ₗ[R] P ⊗[R] (N ⊗[R] Q)) ∘ₗ rTensor Q (lTensor P x))

Tactic:
simp_rw [rTensor, lTensor, map_map_comp_assoc_eq]

Premises used: LinearMap.lTensor, TensorProduct.map_map_comp_assoc_eq, LinearMap.rTensor
-- 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
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R Q
inst_8 : Module R P
x : M →ₗ[R] N
simp_rw :
  Eq (α := P ⊗[R] (M ⊗[R] Q) →ₗ[R] P ⊗[R] N ⊗[R] Q)
    (map (lTensor P x) id ∘ₗ (↑(LinearEquiv.symm (assoc R P M Q)) : P ⊗[R] (M ⊗[R] Q) →ₗ[R] P ⊗[R] M ⊗[R] Q))
    ((↑(LinearEquiv.symm (assoc R P N Q)) : P ⊗[R] (N ⊗[R] Q) →ₗ[R] P ⊗[R] N ⊗[R] Q) ∘ₗ lTensor P (map x id))
simp_rw₁ :
  Eq (α := P ⊗[R] (M ⊗[R] Q) →ₗ[R] P ⊗[R] N ⊗[R] Q)
    (map (map id x) id ∘ₗ (↑(LinearEquiv.symm (assoc R P M Q)) : P ⊗[R] (M ⊗[R] Q) →ₗ[R] P ⊗[R] M ⊗[R] Q))
    ((↑(LinearEquiv.symm (assoc R P N Q)) : P ⊗[R] (N ⊗[R] Q) →ₗ[R] P ⊗[R] N ⊗[R] Q) ∘ₗ map id (map x id))
⊢ Eq (α := P ⊗[R] (M ⊗[R] Q) →ₗ[R] P ⊗[R] N ⊗[R] Q)
    (rTensor Q (lTensor P x) ∘ₗ (↑(LinearEquiv.symm (assoc R P M Q)) : P ⊗[R] (M ⊗[R] Q) →ₗ[R] P ⊗[R] M ⊗[R] Q))
    ((↑(LinearEquiv.symm (assoc R P N Q)) : P ⊗[R] (N ⊗[R] Q) →ₗ[R] P ⊗[R] N ⊗[R] Q) ∘ₗ lTensor P (rTensor Q x))

Tactic:
simp_rw [rTensor, lTensor, map_map_comp_assoc_symm_eq]

Premises used: LinearMap.lTensor, TensorProduct.map_map_comp_assoc_symm_eq, LinearMap.rTensor
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_11
A : Type u_12
A' : Type u_13
B : Type u_14
B' : Type u_15
C : Type u_16
C' : Type u_17
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : AddCommMonoid C'
inst_4 : Module R A'
inst_5 : Module R B'
inst_6 : Module R C'
eA : A ≃ A'
eB : B ≃ B'
eC : C ≃ C'
h :
  ∀ (x : A ⊗[R] B ⊗[R] C),
    Eq (α := A ⊗[R] (B ⊗[R] C))
      ((TensorProduct.assoc R A B C : (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C)) x : A ⊗[R] (B ⊗[R] C))
      ((TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
              (TensorProduct.assoc R A' B' C' ≪≫ₗ
                TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
                  (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))) :
            (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C))
          x :
        A ⊗[R] (B ⊗[R] C))
⊢ Eq (α := A ⊗[R] B ⊗[R] C ≃ₗ[R] A ⊗[R] (B ⊗[R] C)) (TensorProduct.assoc R A B C)
    (TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
      (TensorProduct.assoc R A' B' C' ≪≫ₗ
        TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
          (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))))

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_11
A : Type u_12
A' : Type u_13
B : Type u_14
B' : Type u_15
C : Type u_16
C' : Type u_17
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : AddCommMonoid C'
inst_4 : Module R A'
inst_5 : Module R B'
inst_6 : Module R C'
eA : A ≃ A'
eB : B ≃ B'
eC : C ≃ C'
⊢ Eq (α := A ⊗[R] (B ⊗[R] C)) ((TensorProduct.assoc R A B C : (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C)) 0)
    ((TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
          (TensorProduct.assoc R A' B' C' ≪≫ₗ
            TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
              (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))) :
        (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C))
      0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_11
A : Type u_12
A' : Type u_13
B : Type u_14
B' : Type u_15
C : Type u_16
C' : Type u_17
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : AddCommMonoid C'
inst_4 : Module R A'
inst_5 : Module R B'
inst_6 : Module R C'
eA : A ≃ A'
eB : B ≃ B'
eC : C ≃ C'
x y : A ⊗[R] B ⊗[R] C
h :
  Eq (α := A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.assoc R A B C : (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C)) x : A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
            (TensorProduct.assoc R A' B' C' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
                (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))) :
          (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C))
        x :
      A ⊗[R] (B ⊗[R] C))
h_1 :
  Eq (α := A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.assoc R A B C : (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C)) y : A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
            (TensorProduct.assoc R A' B' C' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
                (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))) :
          (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C))
        y :
      A ⊗[R] (B ⊗[R] C))
⊢ Eq (α := A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.assoc R A B C : (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C)) (x + y) : A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
            (TensorProduct.assoc R A' B' C' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
                (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))) :
          (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C))
        (x + y) :
      A ⊗[R] (B ⊗[R] C))

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_11
A : Type u_12
A' : Type u_13
B : Type u_14
B' : Type u_15
C : Type u_16
C' : Type u_17
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : AddCommMonoid C'
inst_4 : Module R A'
inst_5 : Module R B'
inst_6 : Module R C'
eA : A ≃ A'
eB : B ≃ B'
eC : C ≃ C'
a : C
⊢ Eq (α := A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.assoc R A B C : (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C)) (0 ⊗ₜ[R] a) : A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
            (TensorProduct.assoc R A' B' C' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
                (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))) :
          (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C))
        (0 ⊗ₜ[R] a) :
      A ⊗[R] (B ⊗[R] C))

Tactic:
simp [*, add_tmul]

Premises used: TensorProduct.add_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_11
A : Type u_12
A' : Type u_13
B : Type u_14
B' : Type u_15
C : Type u_16
C' : Type u_17
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : AddCommMonoid C'
inst_4 : Module R A'
inst_5 : Module R B'
inst_6 : Module R C'
eA : A ≃ A'
eB : B ≃ B'
eC : C ≃ C'
a : C
x : A
y : B
⊢ Eq (α := A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.assoc R A B C : (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C)) (x ⊗ₜ[R] y ⊗ₜ[R] a) : A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
            (TensorProduct.assoc R A' B' C' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
                (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))) :
          (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C))
        (x ⊗ₜ[R] y ⊗ₜ[R] a) :
      A ⊗[R] (B ⊗[R] C))

Tactic:
simp [*, add_tmul]

Premises used: TensorProduct.add_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Associator
Goal:
R : Type u_11
A : Type u_12
A' : Type u_13
B : Type u_14
B' : Type u_15
C : Type u_16
C' : Type u_17
inst : CommSemiring R
inst_1 : AddCommMonoid A'
inst_2 : AddCommMonoid B'
inst_3 : AddCommMonoid C'
inst_4 : Module R A'
inst_5 : Module R B'
inst_6 : Module R C'
eA : A ≃ A'
eB : B ≃ B'
eC : C ≃ C'
a : C
x y : A ⊗[R] B
h :
  Eq (α := A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.assoc R A B C : (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C)) (x ⊗ₜ[R] a) : A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
            (TensorProduct.assoc R A' B' C' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
                (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))) :
          (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C))
        (x ⊗ₜ[R] a) :
      A ⊗[R] (B ⊗[R] C))
h_1 :
  Eq (α := A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.assoc R A B C : (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C)) (y ⊗ₜ[R] a) : A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
            (TensorProduct.assoc R A' B' C' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
                (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))) :
          (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C))
        (y ⊗ₜ[R] a) :
      A ⊗[R] (B ⊗[R] C))
⊢ Eq (α := A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.assoc R A B C : (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C)) ((x + y) ⊗ₜ[R] a) : A ⊗[R] (B ⊗[R] C))
    ((TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
            (TensorProduct.assoc R A' B' C' ≪≫ₗ
              TensorProduct.congr (LinearEquiv.symm (linearEquiv R eA))
                (TensorProduct.congr (LinearEquiv.symm (linearEquiv R eB)) (LinearEquiv.symm (linearEquiv R eC)))) :
          (a : A ⊗[R] B ⊗[R] C) → A ⊗[R] (B ⊗[R] C))
        ((x + y) ⊗ₜ[R] a) :
      A ⊗[R] (B ⊗[R] C))

Tactic:
simp [*, add_tmul]

Premises used: TensorProduct.add_tmul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Basic
Goal:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring R₂
inst_2 : CommSemiring R₃
inst_3 : Monoid R'
inst_4 : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : AddCommMonoid P
inst_8 : AddCommMonoid Q
inst_9 : AddCommMonoid S
inst_10 : AddCommMonoid P'
inst_11 : AddCommMonoid Q'
inst_12 : AddCommMonoid M₂
inst_13 : AddCommMonoid N₂
inst_14 : AddCommMonoid P₂
inst_15 : AddCommMonoid Q₂
inst_16 : AddCommMonoid M₃
inst_17 : AddCommMonoid N₃
inst_18 : AddCommMonoid P₃
inst_19 : AddCommMonoid Q₃
inst_20 : DistribMulAction R' M
inst_21 : Module R'' M
inst_22 : Module R M
inst_23 : Module R N
inst_24 : Module R S
inst_25 : Module R P'
inst_26 : Module R Q'
inst_27 : Module R₂ M₂
inst_28 : Module R₂ N₂
inst_29 : Module R₂ P₂
inst_30 : Module R₂ Q₂
inst_31 : Module R₃ M₃
inst_32 : Module R₃ N₃
inst_33 : Module R₃ P₃
inst_34 : Module R₃ Q₃
f : M →+ N →+ P
hf :
  ∀ (r : R) (m : M) (n : N),
    Eq.{u_9 + 1} (α := P) ((((f : (a : M) → N →+ P) (r • m) : N →+ P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →+ P) m : N →+ P) : (a : N) → P) (r • n) : P)
x y : FreeAddMonoid (M × N)
hxy : Eqv R M N x y
n : N
simp_rw :
  Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (0, n)) :
      P)
    (0 : P)
simp_rw₁ : Eq.{u_9 + 1} (α := P) (((f : (a : M) → N →+ P) 0 : (a : N) → P) n : P) (0 : P)
simp_rw₂ : Eq.{u_9 + 1} (α := P) ((0 : (a : N) → P) n : P) (0 : P)
⊢ Eq.{u_9 + 1} (α := P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        (FreeAddMonoid.of (0, n)) :
      P)
    (((FreeAddMonoid.lift : (a : M × N → P) → FreeAddMonoid (M × N) →+ P) fun (mn : M × N) ↦
            (((f : (a : M) → N →+ P) mn.1 : N →+ P) : (a : N) → P) mn.2 :
          (a : FreeAddMonoid (M × N)) → P)
        0 :
      P)

Tactic:
simp_rw [map_zero, FreeAddMonoid.lift_eval_of, map_zero,
          AddMonoidHom.zero_apply]

Premises used: AddMonoidHom.zero_apply, map_zero, FreeAddMonoid.lift_eval_of