awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f : M →ₗ[R] M₁ ⊗[R] M₂ ⊗[R] M₃
rw : (f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α) ∘ₗ f = α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ f
rw₁ : (f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α) ∘ₗ f = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f
rw₂ rw₃ : (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f
⊢ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f = α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ f

Tactic:
rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_eq]

Premises used: LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_eq
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f : M →ₗ[R] M₁ ⊗[R] (M₂ ⊗[R] M₃)
rw : ((f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹) ∘ₗ f = α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ f
rw₁ : ((f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹) ∘ₗ f = (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ f
rw₂ rw₃ : (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ f = (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ f
⊢ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ f = α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ f

Tactic:
rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_symm_eq]

Premises used: LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_symm_eq
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
rw : α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id
⊢ α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ = f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id

Tactic:
rw [← LinearMap.comp_assoc, map_map_comp_assoc_eq]

Premises used: LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_eq
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
a :
  ∀ (x : M) (x_1 : M₃),
    Eq («α» := N₁ ⊗[R] (N₂ ⊗[R] N₃))
      (((((AlgebraTensorModule.curry (α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃) : M →ₗ[R] M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃)) :
                  (a : M) → M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃))
                x :
              M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃)) :
            (a : M₃) → N₁ ⊗[R] (N₂ ⊗[R] N₃))
          x_1 :
        N₁ ⊗[R] (N₂ ⊗[R] N₃))
      (((((AlgebraTensorModule.curry ((α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id) :
                    M →ₗ[R] M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃)) :
                  (a : M) → M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃))
                x :
              M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃)) :
            (a : M₃) → N₁ ⊗[R] (N₂ ⊗[R] N₃))
          x_1 :
        N₁ ⊗[R] (N₂ ⊗[R] N₃))
⊢ α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
x : M
x_1 : M₃
⊢ Eq («α» := N₁ ⊗[R] (N₂ ⊗[R] N₃))
    (((((AlgebraTensorModule.curry (α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃) : M →ₗ[R] M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃)) :
                (a : M) → M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃))
              x :
            M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃)) :
          (a : M₃) → N₁ ⊗[R] (N₂ ⊗[R] N₃))
        x_1 :
      N₁ ⊗[R] (N₂ ⊗[R] N₃))
    (((((AlgebraTensorModule.curry ((α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id) :
                  M →ₗ[R] M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃)) :
                (a : M) → M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃))
              x :
            M₃ →ₗ[R] N₁ ⊗[R] (N₂ ⊗[R] N₃)) :
          (a : M₃) → N₁ ⊗[R] (N₂ ⊗[R] N₃))
        x_1 :
      N₁ ⊗[R] (N₂ ⊗[R] N₃))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
f : M →ₗ[R] M ⊗[R] M₃
⊢ α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ ∘ₗ f = f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id ∘ₗ f

Tactic:
simp only [← LinearMap.comp_assoc, assoc_comp_map_map_comp]

Premises used: CoassocSimps.assoc_comp_map_map_comp, LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₃
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N₃
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
rw : α ∘ₗ f₁₂ ⊗ₘ f₃ = (α ∘ₗ (LinearMap.id ⊗ₘ LinearMap.id) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id
⊢ α ∘ₗ f₁₂ ⊗ₘ f₃ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id

Tactic:
rw [← LinearMap.comp_assoc, map_map_comp_assoc_eq]

Premises used: LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_eq
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₃
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N₃
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
⊢ α ∘ₗ f₁₂ ⊗ₘ f₃ = (α ∘ₗ (LinearMap.id ⊗ₘ LinearMap.id) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id

Tactic:
simp only [coassoc_simps]
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
P : Type u_5
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : AddCommMonoid M₃
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₃
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
f : P →ₗ[R] M ⊗[R] M₃
rw : (α ∘ₗ f₁₂ ⊗ₘ f₃) ∘ₗ f = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id ∘ₗ f
⊢ α ∘ₗ f₁₂ ⊗ₘ f₃ ∘ₗ f = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id ∘ₗ f

Tactic:
rw [← LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
P : Type u_5
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : AddCommMonoid M₃
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₃
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
f : P →ₗ[R] M ⊗[R] M₃
⊢ (α ∘ₗ f₁₂ ⊗ₘ f₃) ∘ₗ f = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id ∘ₗ f

Tactic:
simp only [coassoc_simps]
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N₁
f₁ : M₁ →ₗ[R] N₁
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
rw : α⁻¹ ∘ₗ f₁ ⊗ₘ f₂₃ = (α⁻¹ ∘ₗ f₁ ⊗ₘ (LinearMap.id ⊗ₘ LinearMap.id)) ∘ₗ LinearMap.id ⊗ₘ f₂₃
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ f₂₃ = (f₁ ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃

Tactic:
rw [← LinearMap.comp_assoc, map_map_comp_assoc_symm_eq]

Premises used: LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_symm_eq
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N₁
f₁ : M₁ →ₗ[R] N₁
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ f₂₃ = (α⁻¹ ∘ₗ f₁ ⊗ₘ (LinearMap.id ⊗ₘ LinearMap.id)) ∘ₗ LinearMap.id ⊗ₘ f₂₃

Tactic:
simp only [coassoc_simps]
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
P : Type u_5
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : AddCommMonoid M₃
inst_8 : AddCommMonoid N₁
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
f₁ : M₁ →ₗ[R] N₁
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
f : P →ₗ[R] M₁ ⊗[R] M
rw : (α⁻¹ ∘ₗ f₁ ⊗ₘ f₂₃) ∘ₗ f = (f₁ ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃ ∘ₗ f
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ f₂₃ ∘ₗ f = (f₁ ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃ ∘ₗ f

Tactic:
rw [← LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
P : Type u_5
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid P
inst_4 : Module R P
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : AddCommMonoid M₃
inst_8 : AddCommMonoid N₁
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
f₁ : M₁ →ₗ[R] N₁
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
f : P →ₗ[R] M₁ ⊗[R] M
⊢ (α⁻¹ ∘ₗ f₁ ⊗ₘ f₂₃) ∘ₗ f = (f₁ ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃ ∘ₗ f

Tactic:
simp only [coassoc_simps]
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
rw : α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) = (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ LinearMap.id ⊗ₘ f₂₃
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) = (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃

Tactic:
rw [← LinearMap.comp_assoc, map_map_comp_assoc_symm_eq]

Premises used: LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_symm_eq
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
a :
  ∀ (x : M₁) (x_1 : M),
    Eq («α» := N₁ ⊗[R] N₂ ⊗[R] N₃)
      (((((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃)) : M₁ →ₗ[R] M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃) :
                  (a : M₁) → M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃)
                x :
              M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃) :
            (a : M) → N₁ ⊗[R] N₂ ⊗[R] N₃)
          x_1 :
        N₁ ⊗[R] N₂ ⊗[R] N₃)
      (((((AlgebraTensorModule.curry ((α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ LinearMap.id ⊗ₘ f₂₃) :
                    M₁ →ₗ[R] M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃) :
                  (a : M₁) → M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃)
                x :
              M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃) :
            (a : M) → N₁ ⊗[R] N₂ ⊗[R] N₃)
          x_1 :
        N₁ ⊗[R] N₂ ⊗[R] N₃)
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) = (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ LinearMap.id ⊗ₘ f₂₃

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : AddCommMonoid N₁
inst_7 : AddCommMonoid N₂
inst_8 : AddCommMonoid N₃
inst_9 : Module R M₁
inst_10 : Module R M₂
inst_11 : Module R M₃
inst_12 : Module R N₁
inst_13 : Module R N₂
inst_14 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
x : M₁
x_1 : M
⊢ Eq («α» := N₁ ⊗[R] N₂ ⊗[R] N₃)
    (((((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃)) : M₁ →ₗ[R] M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃) :
                (a : M₁) → M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃)
              x :
            M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃) :
          (a : M) → N₁ ⊗[R] N₂ ⊗[R] N₃)
        x_1 :
      N₁ ⊗[R] N₂ ⊗[R] N₃)
    (((((AlgebraTensorModule.curry ((α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ LinearMap.id ⊗ₘ f₂₃) :
                  M₁ →ₗ[R] M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃) :
                (a : M₁) → M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃)
              x :
            M →ₗ[R] N₁ ⊗[R] N₂ ⊗[R] N₃) :
          (a : M) → N₁ ⊗[R] N₂ ⊗[R] N₃)
        x_1 :
      N₁ ⊗[R] N₂ ⊗[R] N₃)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₁ : Type u_14
N₂ : Type u_15
N₃ : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid M₁
inst_6 : AddCommMonoid M₂
inst_7 : AddCommMonoid M₃
inst_8 : AddCommMonoid N₁
inst_9 : AddCommMonoid N₂
inst_10 : AddCommMonoid N₃
inst_11 : Module R M₁
inst_12 : Module R M₂
inst_13 : Module R M₃
inst_14 : Module R N₁
inst_15 : Module R N₂
inst_16 : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
f : N →ₗ[R] M₁ ⊗[R] M
⊢ α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) ∘ₗ f = (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃ ∘ₗ f

Tactic:
simp only [← LinearMap.comp_assoc, assoc_symm_comp_map_map_comp]

Premises used: LinearMap.comp_assoc, CoassocSimps.assoc_symm_comp_map_map_comp
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
⊢ Eq («α» := M ⊗[R] N →ₗ[R] R ⊗[R] M ⊗[R] N) (α⁻¹ ∘ₗ λ⁻¹) (λ⁻¹ ⊗ₘ LinearMap.id)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.map, TensorProduct.tmul, TensorProduct.lift, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
f : P →ₗ[R] M ⊗[R] N
⊢ α⁻¹ ∘ₗ λ⁻¹ ∘ₗ f = λ⁻¹ ⊗ₘ LinearMap.id ∘ₗ f

Tactic:
rfl

Premises used: addConGen, Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.map, Quotient, TensorProduct, TensorProduct.tmul, AddCon.Quotient, TensorProduct.lift, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
f : M →ₗ[R] M'
a :
  ∀ (x : M) (x_1 : N),
    Eq («α» := M' ⊗[R] R ⊗[R] N)
      (((((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹) : M →ₗ[R] N →ₗ[R] M' ⊗[R] R ⊗[R] N) :
                  (a : M) → N →ₗ[R] M' ⊗[R] R ⊗[R] N)
                x :
              N →ₗ[R] M' ⊗[R] R ⊗[R] N) :
            (a : N) → M' ⊗[R] R ⊗[R] N)
          x_1 :
        M' ⊗[R] R ⊗[R] N)
      (((((AlgebraTensorModule.curry ((f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id) : M →ₗ[R] N →ₗ[R] M' ⊗[R] R ⊗[R] N) :
                  (a : M) → N →ₗ[R] M' ⊗[R] R ⊗[R] N)
                x :
              N →ₗ[R] M' ⊗[R] R ⊗[R] N) :
            (a : N) → M' ⊗[R] R ⊗[R] N)
          x_1 :
        M' ⊗[R] R ⊗[R] N)
⊢ Eq («α» := M ⊗[R] N →ₗ[R] M' ⊗[R] R ⊗[R] N) (α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹) ((f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
f : M →ₗ[R] M'
x : M
x_1 : N
⊢ Eq («α» := M' ⊗[R] R ⊗[R] N)
    (((((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹) : M →ₗ[R] N →ₗ[R] M' ⊗[R] R ⊗[R] N) :
                (a : M) → N →ₗ[R] M' ⊗[R] R ⊗[R] N)
              x :
            N →ₗ[R] M' ⊗[R] R ⊗[R] N) :
          (a : N) → M' ⊗[R] R ⊗[R] N)
        x_1 :
      M' ⊗[R] R ⊗[R] N)
    (((((AlgebraTensorModule.curry ((f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id) : M →ₗ[R] N →ₗ[R] M' ⊗[R] R ⊗[R] N) :
                (a : M) → N →ₗ[R] M' ⊗[R] R ⊗[R] N)
              x :
            N →ₗ[R] M' ⊗[R] R ⊗[R] N) :
          (a : N) → M' ⊗[R] R ⊗[R] N)
        x_1 :
      M' ⊗[R] R ⊗[R] N)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid M'
inst_8 : Module R M'
f : M →ₗ[R] M'
g : P →ₗ[R] M ⊗[R] N
simp_rw : (α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹) ∘ₗ g = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id ∘ₗ g
⊢ α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹ ∘ₗ g = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id ∘ₗ g

Tactic:
simp_rw [← LinearMap.comp_assoc, ← assoc_symm_comp_map_lid_symm]

Premises used: LinearMap.comp_assoc, CoassocSimps.assoc_symm_comp_map_lid_symm
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
f : M →ₗ[R] M'
a :
  ∀ (x : M) (x_1 : N),
    Eq («α» := M' ⊗[R] N ⊗[R] R)
      (((((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹) : M →ₗ[R] N →ₗ[R] M' ⊗[R] N ⊗[R] R) :
                  (a : M) → N →ₗ[R] M' ⊗[R] N ⊗[R] R)
                x :
              N →ₗ[R] M' ⊗[R] N ⊗[R] R) :
            (a : N) → M' ⊗[R] N ⊗[R] R)
          x_1 :
        M' ⊗[R] N ⊗[R] R)
      (((((AlgebraTensorModule.curry ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) : M →ₗ[R] N →ₗ[R] M' ⊗[R] N ⊗[R] R) :
                  (a : M) → N →ₗ[R] M' ⊗[R] N ⊗[R] R)
                x :
              N →ₗ[R] M' ⊗[R] N ⊗[R] R) :
            (a : N) → M' ⊗[R] N ⊗[R] R)
          x_1 :
        M' ⊗[R] N ⊗[R] R)
⊢ Eq («α» := M ⊗[R] N →ₗ[R] M' ⊗[R] N ⊗[R] R) (α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹) ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
f : M →ₗ[R] M'
x : M
x_1 : N
⊢ Eq («α» := M' ⊗[R] N ⊗[R] R)
    (((((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹) : M →ₗ[R] N →ₗ[R] M' ⊗[R] N ⊗[R] R) :
                (a : M) → N →ₗ[R] M' ⊗[R] N ⊗[R] R)
              x :
            N →ₗ[R] M' ⊗[R] N ⊗[R] R) :
          (a : N) → M' ⊗[R] N ⊗[R] R)
        x_1 :
      M' ⊗[R] N ⊗[R] R)
    (((((AlgebraTensorModule.curry ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) : M →ₗ[R] N →ₗ[R] M' ⊗[R] N ⊗[R] R) :
                (a : M) → N →ₗ[R] M' ⊗[R] N ⊗[R] R)
              x :
            N →ₗ[R] M' ⊗[R] N ⊗[R] R) :
          (a : N) → M' ⊗[R] N ⊗[R] R)
        x_1 :
      M' ⊗[R] N ⊗[R] R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
inst_7 : AddCommMonoid M'
inst_8 : Module R M'
f : M →ₗ[R] M'
g : P →ₗ[R] M ⊗[R] N
simp_rw : (α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹) ∘ₗ g = ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ∘ₗ g
⊢ α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹ ∘ₗ g = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹ ∘ₗ g

Tactic:
simp_rw [← LinearMap.comp_assoc, ← assoc_symm_comp_map_rid_symm]

Premises used: LinearMap.comp_assoc, CoassocSimps.assoc_symm_comp_map_rid_symm
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
a :
  ∀ (x : M) (x_1 : N),
    Eq («α» := M ⊗[R] (N ⊗[R] R))
      (((((AlgebraTensorModule.curry (α ∘ₗ ρ⁻¹) : M →ₗ[R] N →ₗ[R] M ⊗[R] (N ⊗[R] R)) :
                  (a : M) → N →ₗ[R] M ⊗[R] (N ⊗[R] R))
                x :
              N →ₗ[R] M ⊗[R] (N ⊗[R] R)) :
            (a : N) → M ⊗[R] (N ⊗[R] R))
          x_1 :
        M ⊗[R] (N ⊗[R] R))
      (((((AlgebraTensorModule.curry (LinearMap.id ⊗ₘ ρ⁻¹) : M →ₗ[R] N →ₗ[R] M ⊗[R] (N ⊗[R] R)) :
                  (a : M) → N →ₗ[R] M ⊗[R] (N ⊗[R] R))
                x :
              N →ₗ[R] M ⊗[R] (N ⊗[R] R)) :
            (a : N) → M ⊗[R] (N ⊗[R] R))
          x_1 :
        M ⊗[R] (N ⊗[R] R))
⊢ Eq («α» := M ⊗[R] N →ₗ[R] M ⊗[R] (N ⊗[R] R)) (α ∘ₗ ρ⁻¹) (LinearMap.id ⊗ₘ ρ⁻¹)

Tactic:
ext