awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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₃)
⊢ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ f = α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ f
have rw : ((f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹) ∘ₗ f = α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ f
Tactic: rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_symm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
⊢ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ f = α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ f
have rw₁ : ((f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹) ∘ₗ f = (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ f
Tactic: rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_symm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
⊢ (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ f = α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ f
have rw₂ : (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ f = (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ f
Tactic: rw [← LinearMap.comp_assoc, ← LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_symm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ = f₁ ⊗ₘ (f₂ ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id
have rw : α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id
Tactic: rw [← LinearMap.comp_assoc, map_map_comp_assoc_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃ = (α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id
have 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₃))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
have rw : α ∘ₗ f₁₂ ⊗ₘ f₃ = (α ∘ₗ (LinearMap.id ⊗ₘ LinearMap.id) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id
Tactic: rw [← LinearMap.comp_assoc, map_map_comp_assoc_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
have rw : (α ∘ₗ f₁₂ ⊗ₘ f₃) ∘ₗ f = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f₃) ∘ₗ α ∘ₗ f₁₂ ⊗ₘ LinearMap.id ∘ₗ f
Tactic: rw [← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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₂₃
have rw : α⁻¹ ∘ₗ f₁ ⊗ₘ f₂₃ = (α⁻¹ ∘ₗ f₁ ⊗ₘ (LinearMap.id ⊗ₘ LinearMap.id)) ∘ₗ LinearMap.id ⊗ₘ f₂₃
Tactic: rw [← LinearMap.comp_assoc, map_map_comp_assoc_symm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
have rw : (α⁻¹ ∘ₗ f₁ ⊗ₘ f₂₃) ∘ₗ f = (f₁ ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃ ∘ₗ f
Tactic: rw [← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) = (f₁ ⊗ₘ f₂) ⊗ₘ f₃ ∘ₗ α⁻¹ ∘ₗ LinearMap.id ⊗ₘ f₂₃
have rw : α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) = (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ LinearMap.id ⊗ₘ f₂₃
Tactic: rw [← LinearMap.comp_assoc, map_map_comp_assoc_symm_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃) = (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ LinearMap.id ⊗ₘ f₂₃
have 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₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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'
⊢ Eq («α» := M ⊗[R] N →ₗ[R] M' ⊗[R] R ⊗[R] N) (α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹) ((f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
⊢ α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹ ∘ₗ g = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id ∘ₗ g
have simp_rw : (α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹) ∘ₗ g = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id ∘ₗ g
Tactic: simp_rw [← LinearMap.comp_assoc, ← assoc_symm_comp_map_lid_symm]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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'
⊢ Eq («α» := M ⊗[R] N →ₗ[R] M' ⊗[R] N ⊗[R] R) (α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹) ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
⊢ α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹ ∘ₗ g = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹ ∘ₗ g
have simp_rw : (α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹) ∘ₗ g = ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ∘ₗ g
Tactic: simp_rw [← LinearMap.comp_assoc, ← assoc_symm_comp_map_rid_symm]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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] M ⊗[R] (N ⊗[R] R)) (α ∘ₗ ρ⁻¹) (LinearMap.id ⊗ₘ ρ⁻¹)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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
have simp_rw : α ∘ₗ ρ⁻¹ ∘ₗ f = (α ∘ₗ ρ⁻¹) ∘ₗ f
Tactic: simp_rw [← assoc_comp_rid_symm, LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
N' : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid N'
inst_6 : Module R N'
f : N →ₗ[R] N'
⊢ Eq («α» := M ⊗[R] N →ₗ[R] R ⊗[R] (M ⊗[R] N')) (α ∘ₗ λ⁻¹ ⊗ₘ f) (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹)
have a : ∀ (x : M) (x_1 : N),
  Eq («α» := R ⊗[R] (M ⊗[R] N'))
    (((((AlgebraTensorModule.curry (α ∘ₗ λ⁻¹ ⊗ₘ f) : M →ₗ[R] N →ₗ[R] R ⊗[R] (M ⊗[R] N')) :
                (a : M) → N →ₗ[R] R ⊗[R] (M ⊗[R] N'))
              x :
            N →ₗ[R] R ⊗[R] (M ⊗[R] N')) :
          (a : N) → R ⊗[R] (M ⊗[R] N'))
        x_1 :
      R ⊗[R] (M ⊗[R] N'))
    (((((AlgebraTensorModule.curry (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹) : M →ₗ[R] N →ₗ[R] R ⊗[R] (M ⊗[R] N')) :
                (a : M) → N →ₗ[R] R ⊗[R] (M ⊗[R] N'))
              x :
            N →ₗ[R] R ⊗[R] (M ⊗[R] N')) :
          (a : N) → R ⊗[R] (M ⊗[R] N'))
        x_1 :
      R ⊗[R] (M ⊗[R] N'))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
N' : Type u_7
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 N'
inst_8 : Module R N'
f : N →ₗ[R] N'
g : P →ₗ[R] M ⊗[R] N
⊢ α ∘ₗ λ⁻¹ ⊗ₘ f ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹ ∘ₗ g
have simp_rw : (α ∘ₗ λ⁻¹ ⊗ₘ f) ∘ₗ g = (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹) ∘ₗ g
Tactic: simp_rw [← LinearMap.comp_assoc, ← assoc_comp_map_lid_symm]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
N' : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid N'
inst_6 : Module R N'
f : N →ₗ[R] N'
⊢ Eq («α» := M ⊗[R] N →ₗ[R] M ⊗[R] (R ⊗[R] N')) (α ∘ₗ ρ⁻¹ ⊗ₘ f) (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹))
have 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 (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ 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'))
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
N' : Type u_7
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 N'
inst_8 : Module R N'
f : N →ₗ[R] N'
g : P →ₗ[R] M ⊗[R] N
⊢ α ∘ₗ ρ⁻¹ ⊗ₘ f ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) ∘ₗ g
have simp_rw : (α ∘ₗ ρ⁻¹ ⊗ₘ f) ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) ∘ₗ g
Tactic: simp_rw [← LinearMap.comp_assoc, ← assoc_comp_map_rid_symm]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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] R
g : N →ₗ[R] M'
⊢ λ ∘ₗ f ⊗ₘ g = g ∘ₗ λ ∘ₗ f ⊗ₘ LinearMap.id
have a : ∀ (x : M) (x_1 : N),
  Eq.{u_6 + 1} («α» := M')
    (((((AlgebraTensorModule.curry (λ ∘ₗ f ⊗ₘ g) : M →ₗ[R] N →ₗ[R] M') : (a : M) → N →ₗ[R] M') x : N →ₗ[R] M') :
          (a : N) → M')
        x_1 :
      M')
    (((((AlgebraTensorModule.curry (g ∘ₗ λ ∘ₗ f ⊗ₘ LinearMap.id) : M →ₗ[R] N →ₗ[R] M') : (a : M) → N →ₗ[R] M') x :
            N →ₗ[R] M') :
          (a : N) → M')
        x_1 :
      M')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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'
g : N →ₗ[R] R
⊢ ρ ∘ₗ f ⊗ₘ g = f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g
have a : ∀ (x : M) (x_1 : N),
  Eq.{u_6 + 1} («α» := M')
    (((((AlgebraTensorModule.curry (ρ ∘ₗ f ⊗ₘ g) : M →ₗ[R] N →ₗ[R] M') : (a : M) → N →ₗ[R] M') x : N →ₗ[R] M') :
          (a : N) → M')
        x_1 :
      M')
    (((((AlgebraTensorModule.curry (f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g) : M →ₗ[R] N →ₗ[R] M') : (a : M) → N →ₗ[R] M') x :
            N →ₗ[R] M') :
          (a : N) → M')
        x_1 :
      M')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
⊢ λ⁻¹ ∘ₗ f = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹
have h : ∀ (x : M),
  Eq («α» := R ⊗[R] M') ((λ⁻¹ ∘ₗ f : (a : M) → R ⊗[R] M') x : R ⊗[R] M')
    ((LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹ : (a : M) → R ⊗[R] M') x : R ⊗[R] M')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
f : M →ₗ[R] M'
⊢ ρ⁻¹ ∘ₗ f = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹
have h : ∀ (x : M),
  Eq («α» := M' ⊗[R] R) ((ρ⁻¹ ∘ₗ f : (a : M) → M' ⊗[R] R) x : M' ⊗[R] R)
    ((f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹ : (a : M) → M' ⊗[R] R) x : M' ⊗[R] R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
N' : Type u_7
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'
inst_7 : AddCommMonoid N'
inst_8 : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
⊢ β ∘ₗ f ⊗ₘ g = g ⊗ₘ f ∘ₗ β
have a : ∀ (x : M) (x_1 : N),
  Eq («α» := N' ⊗[R] M')
    (((((AlgebraTensorModule.curry (β ∘ₗ f ⊗ₘ g) : M →ₗ[R] N →ₗ[R] N' ⊗[R] M') : (a : M) → N →ₗ[R] N' ⊗[R] M') x :
            N →ₗ[R] N' ⊗[R] M') :
          (a : N) → N' ⊗[R] M')
        x_1 :
      N' ⊗[R] M')
    (((((AlgebraTensorModule.curry (g ⊗ₘ f ∘ₗ β) : M →ₗ[R] N →ₗ[R] N' ⊗[R] M') : (a : M) → N →ₗ[R] N' ⊗[R] M') x :
            N →ₗ[R] N' ⊗[R] M') :
          (a : N) → N' ⊗[R] M')
        x_1 :
      N' ⊗[R] M')
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : Coalgebra R M
f : M →ₗ[R] M'
⊢ α ∘ₗ δ ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ ∘ₗ δ
have simp_rw : (α ∘ₗ δ ⊗ₘ f) ∘ₗ δ = ((α ∘ₗ (LinearMap.id ⊗ₘ LinearMap.id) ⊗ₘ f) ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ
Tactic: simp_rw [← LinearMap.lTensor_def, ← coassoc, ← LinearMap.comp_assoc, LinearMap.lTensor_def,
    map_map_comp_assoc_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
⊢ α ∘ₗ δ ⊗ₘ f ∘ₗ δ ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ ∘ₗ δ ∘ₗ g
have simp : ((α ∘ₗ δ ⊗ₘ f) ∘ₗ δ) ∘ₗ g = ((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ) ∘ₗ δ) ∘ₗ g
Tactic: simp only [← LinearMap.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
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'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
⊢ ((α ∘ₗ δ ⊗ₘ f) ∘ₗ δ) ∘ₗ g = ((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ) ∘ₗ δ) ∘ₗ g
have e_f : (α ∘ₗ δ ⊗ₘ f) ∘ₗ δ = (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ) ∘ₗ δ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Coalgebra.CoassocSimps (goal)
Goal:
R : Type u_1
M : Type u_3
M' : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
inst_5 : Coalgebra R M
f : M →ₗ[R] M'
⊢ α⁻¹ ∘ₗ f ⊗ₘ δ ∘ₗ δ = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ δ
have simp_rw : (α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ = ((α⁻¹ ∘ₗ f ⊗ₘ (LinearMap.id ⊗ₘ LinearMap.id)) ∘ₗ LinearMap.lTensor M δ) ∘ₗ δ
Tactic: simp_rw [← LinearMap.rTensor_def, ← coassoc_symm, ← LinearMap.comp_assoc, LinearMap.rTensor_def,
    map_map_comp_assoc_symm_eq]