mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case some
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
val✝ : X'✝.X
⊢ ({ toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
              invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
              left_inv := ⋯, right_inv := ⋯ }.symm
          (f ≫ g)).toFun
      (some val✝) =
    (pointedToBipointedSnd.map f ≫
          { toFun := fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ },
                invFun := fun f ↦ { toFun := fun o ↦ Option.elim o Y✝.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ },
                left_inv := ⋯, right_inv := ⋯ }.symm
            g).toFun
      (some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Category.BddLat

Goal state before:
pp: X : Lat
x✝ : BddLat
f : latToBddLat.obj X ⟶ x✝
a b : ↑X
⊢ (some ∘ some) (a ⊔ b) = (some ∘ some) a ⊔ (some ∘ some) b

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Category.BddLat

Goal state before:
pp: X : Lat
x✝ : BddLat
f : latToBddLat.obj X ⟶ x✝
a b : ↑X
⊢ (some ∘ some) (a ⊓ b) = (some ∘ some) a ⊓ (some ∘ some) b

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: 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✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₁₂ : M →ₗ[R] M₁ ⊗[R] M₂
x✝¹ : M
x✝ : M₃
⊢ ((AlgebraTensorModule.curry (α ∘ₗ (f₁ ⊗ₘ f₂ ∘ₗ f₁₂) ⊗ₘ f₃)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((α ∘ₗ (f₁ ⊗ₘ f₂) ⊗ₘ f₃) ∘ₗ f₁₂ ⊗ₘ LinearMap.id)) x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: 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✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid N₁
inst✝⁷ : AddCommMonoid N₂
inst✝⁶ : AddCommMonoid N₃
inst✝⁵ : Module R M₁
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] N₁
f₂ : M₂ →ₗ[R] N₂
f₃ : M₃ →ₗ[R] N₃
f₂₃ : M →ₗ[R] M₂ ⊗[R] M₃
x✝¹ : M₁
x✝ : M
⊢ ((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃ ∘ₗ f₂₃))) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((α⁻¹ ∘ₗ f₁ ⊗ₘ (f₂ ⊗ₘ f₃)) ∘ₗ LinearMap.id ⊗ₘ f₂₃)) x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id)) x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
g : P →ₗ[R] M ⊗[R] N
⊢ (α⁻¹ ∘ₗ f ⊗ₘ λ⁻¹) ∘ₗ g = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ⊗ₘ LinearMap.id ∘ₗ g

Tactic:
← assoc_symm_comp_map_lid_symm

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹)) x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (α ∘ₗ ρ⁻¹)) x✝¹) x✝ = ((AlgebraTensorModule.curry (LinearMap.id ⊗ₘ ρ⁻¹)) x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
N' : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : N →ₗ[R] N'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (α ∘ₗ λ⁻¹ ⊗ₘ f)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ λ⁻¹)) x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
N' : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : N →ₗ[R] N'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (α ∘ₗ ρ⁻¹ ⊗ₘ f)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry (LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹))) x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x✝ : M
⊢ (λ⁻¹ ∘ₗ f) x✝ = (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
x✝ : M
⊢ (ρ⁻¹ ∘ₗ f) x✝ = (f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
N' : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
inst✝¹ : AddCommMonoid N'
inst✝ : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry (β ∘ₗ f ⊗ₘ g)) x✝¹) x✝ = ((AlgebraTensorModule.curry (g ⊗ₘ f ∘ₗ β)) x✝¹) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (λ_ A.X).inv.op = (λ_ (op A.X)).hom

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (ρ_ A.X).inv.op = (ρ_ (op A.X)).hom

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Comon C
⊢ (α_ A.X A.X A.X).inv.op ≫ (A.X ◁ Δ).op ≫ Δ.op = (α_ A.X A.X A.X).inv.op ≫ (Δ ≫ A.X ◁ Δ).op

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ (λ_ A.X).hom.unop = (λ_ (unop A.X)).inv

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ μ.unop ≫ η.unop ▷ unop A.X = (λ_ (unop A.X)).inv

Tactic:
by rw [← unop_whiskerRight, ← unop_comp, MonObj.one_mul]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ (ρ_ A.X).hom.unop = (ρ_ (unop A.X)).inv

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
A : Mon Cᵒᵖ
⊢ ((α_ A.X A.X A.X).inv ≫ μ ▷ A.X ≫ μ).unop = (μ ▷ A.X ≫ μ).unop ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ LinearMap.lTensor R f ∘ₗ (TensorProduct.mk R R M) 1 = LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : BraidedCategory C
A B : C
inst✝¹ : ComonObj A
inst✝ : ComonObj B
⊢ Δ = (Δ ⊗ₘ Δ) ≫ (tensorμ (op A) (op B) (op A) (op B)).unop

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
M' : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
⊢ LinearMap.rTensor R f ∘ₗ (TensorProduct.mk R M R).flip 1 = f ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: case e_f.e_f
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
x✝² x✝¹ x✝ : M
⊢ (((AlgebraTensorModule.curry (AlgebraTensorModule.curry (α ∘ₗ β ⊗ₘ f))) x✝²) x✝¹) x✝ =
    (((AlgebraTensorModule.curry
            (AlgebraTensorModule.curry
              (((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α)))
          x✝²)
        x✝¹)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X✝ Y✝ : CoalgCat R
x✝ : X✝ ⟶ Y✝
⊢ (𝟭 (CoalgCat R)).map x✝ ≫ (Iso.refl ((𝟭 (CoalgCat R)).obj Y✝)).hom =
    (Iso.refl ((𝟭 (CoalgCat R)).obj X✝)).hom ≫ (toComon R ⋙ ofComon R).map x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X✝ Y✝ : Comon (ModuleCat R)
x✝ : X✝ ⟶ Y✝
⊢ (ofComon R ⋙ toComon R).map x✝ ≫ (Iso.refl ((ofComon R ⋙ toComon R).obj Y✝)).hom =
    (Iso.refl ((ofComon R ⋙ toComon R).obj X✝)).hom ≫ (𝟭 (Comon (ModuleCat R))).map x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
K L : CoalgCat R
⊢ ↑(TensorProduct.tensorTensorTensorComm R ↑((comonEquivalence R).symm.inverse.obj K).X
          ↑((comonEquivalence R).symm.inverse.obj K).X ↑((comonEquivalence R).symm.inverse.obj L).X
          ↑((comonEquivalence R).symm.inverse.obj L).X) ∘ₗ
      ModuleCat.Hom.hom (MonObj.mul.unop ⊗ₘ MonObj.mul.unop) =
    ↑(TensorProduct.tensorTensorTensorComm R ↑K.toModuleCat ↑K.toModuleCat ↑L.toModuleCat ↑L.toModuleCat) ∘ₗ
      TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
x✝² :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
x✝¹ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R N)))).X)
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R P)))).X)
⊢ ((((TensorProduct.mk R
                ↑(Opposite.unop
                    (Opposite.unop
                        ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                          ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
                ↑(Opposite.unop
                    (Opposite.unop
                        ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                          ((comonEquivalence R).symm.inverse.obj (of R N)))).X)).compr₂ₛₗ
            ((TensorProduct.mk R
                  ↑(Opposite.unop
                      (Opposite.unop
                          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                            ((comonEquivalence R).symm.inverse.obj (of R M ⊗ of R N)))).X)
                  ↑(Opposite.unop
                      (Opposite.unop
                          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                            ((comonEquivalence R).symm.inverse.obj (of R P)))).X)).compr₂ₛₗ
              (α_ (of R M) (of R N) (of R P)).hom.toCoalgHom'.toLinearMap))
          x✝²)
        x✝¹)
      x✝ =
    ((((TensorProduct.mk R
                ↑(Opposite.unop
                    (Opposite.unop
                        ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                          ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
                ↑(Opposite.unop
                    (Opposite.unop
                        ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                          ((comonEquivalence R).symm.inverse.obj (of R N)))).X)).compr₂ₛₗ
            ((TensorProduct.mk R
                  ↑(Opposite.unop
                      (Opposite.unop
                          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                            ((comonEquivalence R).symm.inverse.obj (of R M ⊗ of R N)))).X)
                  ↑(Opposite.unop
                      (Opposite.unop
                          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                            ((comonEquivalence R).symm.inverse.obj (of R P)))).X)).compr₂ₛₗ
              ↑(TensorProduct.assoc R M N P)))
          x✝²)
        x✝¹)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
⊢ (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)).compr₂ₛₗ
          (λ_ (of R M)).hom.toCoalgHom'.toLinearMap)
        1)
      x✝ =
    (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)).compr₂ₛₗ
          ↑(TensorProduct.lid R M))
        1)
      x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
M : Type u
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Coalgebra R M
x✝ :
  ↑(Opposite.unop
      (Opposite.unop
          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
            ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
⊢ (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)).compr₂ₛₗ
          (ρ_ (of R M)).hom.toCoalgHom'.toLinearMap)
        x✝)
      1 =
    (((TensorProduct.mk R
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (of R M)))).X)
              ↑(Opposite.unop
                  (Opposite.unop
                      ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).symm.inverse.obj
                        ((comonEquivalence R).symm.inverse.obj (𝟙_ (CoalgCat R))))).X)).compr₂ₛₗ
          ↑(TensorProduct.rid R M))
        x✝)
      1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ ↑(tensorTensorTensorComm R ↑((comonEquivalence R).functor.obj (of R M)).X
          ↑((comonEquivalence R).functor.obj (of R M)).X ↑((comonEquivalence R).functor.obj (of R N)).X
          ↑((comonEquivalence R).functor.obj (of R N)).X) ∘ₗ
      ModuleCat.Hom.hom (ModuleCat.ofHom CoalgebraStruct.comul ⊗ₘ ModuleCat.ofHom CoalgebraStruct.comul) =
    ↑(tensorTensorTensorComm R M M N N) ∘ₗ AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ↑(tensorTensorTensorComm R ↑((comonEquivalence R).functor.obj (of R M)).X
          ↑((comonEquivalence R).functor.obj (of R M)).X ↑((comonEquivalence R).functor.obj (of R N ⊗ of R P)).X
          ↑((comonEquivalence R).functor.obj (of R N ⊗ of R P)).X) ∘ₗ
      ModuleCat.Hom.hom
        (ModuleCat.ofHom CoalgebraStruct.comul ⊗ₘ
          (ModuleCat.ofHom CoalgebraStruct.comul ⊗ₘ ModuleCat.ofHom CoalgebraStruct.comul) ≫
            ModuleCat.ofHom
              ↑(tensorTensorTensorComm R
                  ↑(Opposite.unop
                      (Opposite.unop
                          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).functor.obj
                            ((comonEquivalence R).functor.obj (of R N)))).X)
                  ↑(Opposite.unop
                      (Opposite.unop
                          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).functor.obj
                            ((comonEquivalence R).functor.obj (of R N)))).X)
                  ↑(Opposite.unop
                      (Opposite.unop
                          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).functor.obj
                            ((comonEquivalence R).functor.obj (of R P)))).X)
                  ↑(Opposite.unop
                      (Opposite.unop
                          ((Comon.Comon_EquivMon_OpOp (ModuleCat R)).functor.obj
                            ((comonEquivalence R).functor.obj (of R P)))).X))) =
    ↑(tensorTensorTensorComm R M M (N ⊗[R] P) (N ⊗[R] P)) ∘ₗ
      AlgebraTensorModule.map CoalgebraStruct.comul
        (↑(tensorTensorTensorComm R N N P P) ∘ₗ AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ↑(tensorTensorTensorComm R (↑(of R M ⊗ of R N).toModuleCat) (↑(of R M ⊗ of R N).toModuleCat) P P) ∘ₗ
      ModuleCat.Hom.hom
        ((MonObj.mul.unop ⊗ₘ MonObj.mul.unop) ≫ ModuleCat.ofHom ↑(tensorTensorTensorComm R M M N N) ⊗ₘ
          MonObj.mul.unop) =
    ↑(tensorTensorTensorComm R (M ⊗[R] N) (M ⊗[R] N) P P) ∘ₗ
      AlgebraTensorModule.map
        (↑(tensorTensorTensorComm R M M N N) ∘ₗ AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul)
        CoalgebraStruct.comul

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
M N : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Coalgebra R M
inst✝ : Coalgebra R N
⊢ ModuleCat.Hom.hom (λ_ (𝟙_ (ModuleCat R))).hom ∘ₗ
      ModuleCat.Hom.hom (ModuleCat.ofHom CoalgebraStruct.counit ⊗ₘ ModuleCat.ofHom CoalgebraStruct.counit) =
    ↑(TensorProduct.lid R R) ∘ₗ AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom (λ_ (𝟙_ (ModuleCat R))).hom ∘ₗ
      ModuleCat.Hom.hom
        (ModuleCat.ofHom CoalgebraStruct.counit ⊗ₘ
          (ModuleCat.ofHom CoalgebraStruct.counit ⊗ₘ ModuleCat.ofHom CoalgebraStruct.counit) ≫
            (λ_ (𝟙_ (ModuleCat R))).hom) =
    ↑(TensorProduct.lid R R) ∘ₗ
      AlgebraTensorModule.map CoalgebraStruct.counit
        (↑(TensorProduct.lid R R) ∘ₗ AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝⁹ : CommRing R
M N P : Type u
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : AddCommGroup P
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Coalgebra R M
inst✝¹ : Coalgebra R N
inst✝ : Coalgebra R P
⊢ ModuleCat.Hom.hom (λ_ (𝟙_ (ModuleCat R))).hom ∘ₗ
      ModuleCat.Hom.hom
        ((ModuleCat.ofHom CoalgebraStruct.counit ⊗ₘ ModuleCat.ofHom CoalgebraStruct.counit) ≫
            (λ_ (𝟙_ (ModuleCat R))).hom ⊗ₘ
          ModuleCat.ofHom CoalgebraStruct.counit) =
    ↑(TensorProduct.lid R R) ∘ₗ
      AlgebraTensorModule.map
        (↑(TensorProduct.lid R R) ∘ₗ AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit)
        CoalgebraStruct.counit

Tactic:
rfl

Goal state after: