awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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:
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
simp_rw : α ∘ₗ ρ⁻¹ ∘ₗ f = (α ∘ₗ ρ⁻¹) ∘ₗ f
⊢ α ∘ₗ ρ⁻¹ ∘ₗ f = LinearMap.id ⊗ₘ ρ⁻¹ ∘ₗ f

Tactic:
simp_rw [← assoc_comp_rid_symm, LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc, CoassocSimps.assoc_comp_rid_symm
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
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'))
⊢ Eq («α» := M ⊗[R] N →ₗ[R] R ⊗[R] (M ⊗[R] N')) (α ∘ₗ λ⁻¹ ⊗ₘ f) (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹)

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
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:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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
simp_rw : (α ∘ₗ λ⁻¹ ⊗ₘ f) ∘ₗ g = (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹) ∘ₗ g
⊢ α ∘ₗ λ⁻¹ ⊗ₘ f ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹ ∘ₗ g

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

Premises used: LinearMap.comp_assoc, CoassocSimps.assoc_comp_map_lid_symm
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
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'))
⊢ Eq («α» := M ⊗[R] N →ₗ[R] M ⊗[R] (R ⊗[R] N')) (α ∘ₗ ρ⁻¹ ⊗ₘ f) (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹))

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
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:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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
simp_rw : (α ∘ₗ ρ⁻¹ ⊗ₘ f) ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) ∘ₗ g
⊢ α ∘ₗ ρ⁻¹ ⊗ₘ f ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) ∘ₗ g

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

Premises used: LinearMap.comp_assoc, CoassocSimps.assoc_comp_map_rid_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] R
g : N →ₗ[R] M'
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')
⊢ λ ∘ₗ f ⊗ₘ g = g ∘ₗ λ ∘ₗ f ⊗ₘ 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] R
g : N →ₗ[R] M'
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:
simp
-- 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] R
g : N →ₗ[R] M'
h : P →ₗ[R] M ⊗[R] N
⊢ λ ∘ₗ f ⊗ₘ g ∘ₗ h = g ∘ₗ λ ∘ₗ f ⊗ₘ LinearMap.id ∘ₗ h

Tactic:
simp only [← LinearMap.comp_assoc, lid_comp_map _ g]

Premises used: LinearMap.comp_assoc, CoassocSimps.lid_comp_map
-- 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'
g : N →ₗ[R] R
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')
⊢ ρ ∘ₗ f ⊗ₘ g = f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g

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'
g : N →ₗ[R] R
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:
simp
-- 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 : N →ₗ[R] R
h : P →ₗ[R] M ⊗[R] N
⊢ ρ ∘ₗ f ⊗ₘ g ∘ₗ h = f ∘ₗ ρ ∘ₗ LinearMap.id ⊗ₘ g ∘ₗ h

Tactic:
simp only [← LinearMap.comp_assoc, rid_comp_map f]

Premises used: LinearMap.comp_assoc, CoassocSimps.rid_comp_map
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
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')
⊢ λ⁻¹ ∘ₗ f = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
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:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
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)
⊢ ρ⁻¹ ∘ₗ f = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
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:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq («α» := M →ₗ[R] M ⊗[R] R) (β ∘ₗ λ⁻¹) ρ⁻¹

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Quotient, 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
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq («α» := M →ₗ[R] R ⊗[R] M) (β ∘ₗ ρ⁻¹) λ⁻¹

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Quotient, 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
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'
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')
⊢ β ∘ₗ f ⊗ₘ g = g ⊗ₘ f ∘ₗ β

Tactic:
ext
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
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:
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
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 M'
inst_8 : Module R M'
inst_9 : AddCommMonoid N'
inst_10 : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
h : P →ₗ[R] M ⊗[R] N
⊢ β ∘ₗ f ⊗ₘ g ∘ₗ h = g ⊗ₘ f ∘ₗ β ∘ₗ h

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

Premises used: LinearMap.comp_assoc, CoassocSimps.symm_comp_map
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
simp_rw : (α ∘ₗ δ ⊗ₘ f) ∘ₗ δ = ((α ∘ₗ (LinearMap.id ⊗ₘ LinearMap.id) ⊗ₘ f) ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ
⊢ α ∘ₗ δ ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ ∘ₗ δ

Tactic:
simp_rw [← LinearMap.lTensor_def, ← coassoc, ← LinearMap.comp_assoc, LinearMap.lTensor_def,
    map_map_comp_assoc_eq]

Premises used: LinearMap.comp_assoc, TensorProduct.map_map_comp_assoc_eq, Coalgebra.coassoc, LinearMap.lTensor_def
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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.rTensor M δ) ∘ₗ δ

Tactic:
simp only [coassoc_simps]
-- 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'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
simp : ((α ∘ₗ δ ⊗ₘ f) ∘ₗ δ) ∘ₗ g = ((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ) ∘ₗ δ) ∘ₗ g
⊢ α ∘ₗ δ ⊗ₘ f ∘ₗ δ ∘ₗ g = LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ ∘ₗ δ ∘ₗ g

Tactic:
simp only [← LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc
-- 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'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
e_f : (α ∘ₗ δ ⊗ₘ f) ∘ₗ δ = (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ) ∘ₗ δ
⊢ ((α ∘ₗ δ ⊗ₘ f) ∘ₗ δ) ∘ₗ g = ((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ) ∘ₗ δ) ∘ₗ g

Tactic:
congr 1
-- 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'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
⊢ (α ∘ₗ δ ⊗ₘ f) ∘ₗ δ = (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ) ∘ₗ δ

Tactic:
simp only [coassoc_simps]
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
simp_rw : (α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ = ((α⁻¹ ∘ₗ f ⊗ₘ (LinearMap.id ⊗ₘ LinearMap.id)) ∘ₗ LinearMap.lTensor M δ) ∘ₗ δ
⊢ α⁻¹ ∘ₗ f ⊗ₘ δ ∘ₗ δ = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ δ

Tactic:
simp_rw [← LinearMap.rTensor_def, ← coassoc_symm, ← LinearMap.comp_assoc, LinearMap.rTensor_def,
    map_map_comp_assoc_symm_eq]

Premises used: LinearMap.comp_assoc, LinearMap.rTensor_def, Coalgebra.coassoc_symm, TensorProduct.map_map_comp_assoc_symm_eq
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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.lTensor M δ) ∘ₗ δ

Tactic:
simp only [coassoc_simps]
-- 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'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
simp : ((α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ) ∘ₗ g = (((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ δ) ∘ₗ g
⊢ α⁻¹ ∘ₗ f ⊗ₘ δ ∘ₗ δ ∘ₗ g = (f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id ∘ₗ δ ∘ₗ g

Tactic:
simp only [← LinearMap.comp_assoc]

Premises used: LinearMap.comp_assoc
-- 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'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
e_f : (α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ = ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ δ
⊢ ((α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ) ∘ₗ g = (((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ δ) ∘ₗ g

Tactic:
congr 1
-- 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'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
⊢ (α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ = ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ δ

Tactic:
simp only [coassoc_simps]
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
rw : LinearMap.lTensor R f ∘ₗ (TensorProduct.mk R R M : (a : R) → M →ₗ[R] R ⊗[R] M) 1 = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹
⊢ ε ⊗ₘ f ∘ₗ δ = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
rw [← LinearMap.lTensor_comp_rTensor, LinearMap.comp_assoc, Coalgebra.rTensor_counit_comp_comul]

Premises used: LinearMap.comp_assoc, Coalgebra.rTensor_counit_comp_comul, LinearMap.lTensor_comp_rTensor
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
⊢ LinearMap.lTensor R f ∘ₗ (TensorProduct.mk R R M : (a : R) → M →ₗ[R] R ⊗[R] M) 1 = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
rfl
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
Goal:
R : Type u_1
M : Type u_3
P : Type u_5
M' : Type u_6
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 : Module R M'
inst_7 : Coalgebra R M
f : M →ₗ[R] M'
g : P →ₗ[R] M
simp_rw : (ε ⊗ₘ f ∘ₗ δ) ∘ₗ g = (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) ∘ₗ g
⊢ ε ⊗ₘ f ∘ₗ δ ∘ₗ g = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹ ∘ₗ g

Tactic:
simp_rw [← LinearMap.comp_assoc, map_counit_comp_comul_left]

Premises used: LinearMap.comp_assoc, CoassocSimps.map_counit_comp_comul_left
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
rw :
  LinearMap.rTensor R f ∘ₗ (LinearMap.flip (TensorProduct.mk R M R) : (a : R) → M →ₗ[R] M ⊗[R] R) 1 =
    f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹
⊢ f ⊗ₘ ε ∘ₗ δ = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
rw [← LinearMap.rTensor_comp_lTensor, LinearMap.comp_assoc, Coalgebra.lTensor_counit_comp_comul]

Premises used: LinearMap.rTensor_comp_lTensor, LinearMap.comp_assoc, Coalgebra.lTensor_counit_comp_comul
-- Module: Mathlib.RingTheory.Coalgebra.CoassocSimps
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'
⊢ LinearMap.rTensor R f ∘ₗ (LinearMap.flip (TensorProduct.mk R M R) : (a : R) → M →ₗ[R] M ⊗[R] R) 1 =
    f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
rfl