awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M : Comon.{v₁, u₁} C
⊢ Hom.hom (𝟙 M) = 𝟙 M.X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N K : Comon.{v₁, u₁} C
f : M ⟶ N
g : N ⟶ K
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A B : Comon.{v₁, u₁} C
f : A ⟶ B
e : IsIso (X := Functor.obj (forget C) A) (Functor.map (forget C) f)
⊢ IsIso f.hom

Tactic:
e
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α := A.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (X.{v₁, u₁} (trivial C)) (X.{v₁, u₁} (trivial C))) (ε ≫ Δ)
    (Δ ≫ (ε ⊗ₘ ε))

Tactic:
simp [unitors_inv_equal]

Premises used: CategoryTheory.MonoidalCategory.unitors_inv_equal
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
f : A ⟶ trivial C
w : f.hom = Hom.hom { hom := ε, isComonHom_hom := ⋯ }
⊢ f = { hom := ε, isComonHom_hom := ⋯ }

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
f : A ⟶ trivial C
w : f.hom ≫ 𝟙 (X.{v₁, u₁} (trivial C)) = Hom.hom { hom := ε, isComonHom_hom := ⋯ }
⊢ f.hom = Hom.hom { hom := ε, isComonHom_hom := ⋯ }

Tactic:
rw [← Category.comp_id f.hom]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Comon.Hom.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
f : A ⟶ trivial C
w : f.hom ≫ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) = ε
⊢ f.hom ≫ 𝟙 (X.{v₁, u₁} (trivial C)) = Hom.hom { hom := ε, isComonHom_hom := ⋯ }

Tactic:
dsimp only [trivial_X]

Premises used: CategoryTheory.Comon.trivial_X
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
f : A ⟶ trivial C
w : Eq (α := A.X ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (f.hom ≫ ε) ε
w₁ w₂ : Eq.{v₁ + 1} (α := A.X ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε ε
⊢ f.hom ≫ 𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)) = ε

Tactic:
rw [← trivial_comon_counit, IsComonHom.hom_counit]

Premises used: CategoryTheory.IsComonHom.hom_counit, CategoryTheory.Comon.trivial_comon_counit
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
⊢ HasTerminal (Comon.{v₁, u₁} C)

Tactic:
hasTerminal_of_unique (trivial C)

Premises used: CategoryTheory.Limits.hasTerminal_of_unique, CategoryTheory.Comon.trivial
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
rw :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)) (op A.X) ⟶ op A.X)
    (Quiver.Hom.op (Iso.inv (λ_ A.X))) (Iso.hom (λ_ (op A.X)))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)) (op A.X) ⟶ op A.X)
    (Quiver.Hom.op ε ▷ op A.X ≫ Quiver.Hom.op Δ) (Iso.hom (λ_ (op A.X)))

Tactic:
rw [← op_whiskerRight, ← op_comp, counit_comul]

Premises used: CategoryTheory.op_comp, CategoryTheory.op_whiskerRight, CategoryTheory.ComonObj.counit_comul
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)) (op A.X) ⟶ op A.X)
    (Quiver.Hom.op (Iso.inv (λ_ A.X))) (Iso.hom (λ_ (op A.X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
rw :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (op A.X) (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)) ⟶ op A.X)
    (Quiver.Hom.op (Iso.inv (ρ_ A.X))) (Iso.hom (ρ_ (op A.X)))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (op A.X) (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)) ⟶ op A.X)
    (op A.X ◁ Quiver.Hom.op ε ≫ Quiver.Hom.op Δ) (Iso.hom (ρ_ (op A.X)))

Tactic:
rw [← op_whiskerLeft, ← op_comp, comul_counit]

Premises used: CategoryTheory.op_comp, CategoryTheory.ComonObj.comul_counit, CategoryTheory.op_whiskerLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (op A.X) (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)) ⟶ op A.X)
    (Quiver.Hom.op (Iso.inv (ρ_ A.X))) (Iso.hom (ρ_ (op A.X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
rw :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (op A.X) (op A.X))
        (op A.X) ⟶
      op A.X)
    (Quiver.Hom.op (Iso.inv (α_ A.X A.X A.X)) ≫ Quiver.Hom.op (A.X ◁ Δ) ≫ Quiver.Hom.op Δ)
    (Quiver.Hom.op (Iso.inv (α_ A.X A.X A.X)) ≫ Quiver.Hom.op (Δ ≫ A.X ◁ Δ))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (op A.X) (op A.X))
        (op A.X) ⟶
      op A.X)
    (Quiver.Hom.op Δ ▷ op A.X ≫ Quiver.Hom.op Δ)
    (Iso.hom (α_ (op A.X) (op A.X) (op A.X)) ≫ op A.X ◁ Quiver.Hom.op Δ ≫ Quiver.Hom.op Δ)

Tactic:
rw [← op_inv_associator, ← op_whiskerRight, ← op_comp, ← op_whiskerLeft, ← op_comp,
      comul_assoc_flip, op_comp, op_comp_assoc]

Premises used: CategoryTheory.op_comp, CategoryTheory.op_inv_associator, CategoryTheory.op_whiskerRight, CategoryTheory.op_whiskerLeft, CategoryTheory.op_comp_assoc, CategoryTheory.ComonObj.comul_assoc_flip
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Comon.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (op A.X) (op A.X))
        (op A.X) ⟶
      op A.X)
    (Quiver.Hom.op (Iso.inv (α_ A.X A.X A.X)) ≫ Quiver.Hom.op (A.X ◁ Δ) ≫ Quiver.Hom.op Δ)
    (Quiver.Hom.op (Iso.inv (α_ A.X A.X A.X)) ≫ Quiver.Hom.op (Δ ≫ A.X ◁ Δ))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
X Y : Comon.{v₁, u₁} C
f : X ⟶ Y
a :
  Eq.{v₁ + 1} (α := unop (unop (op X.ComonToMonOpOpObj)).X ⟶ unop (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)))
    (Quiver.Hom.unop (η ≫ f.hom.op)) (Quiver.Hom.unop η)
⊢ Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite) ⟶ (unop (op X.ComonToMonOpOpObj)).X) (η ≫ f.hom.op)
    η

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
X Y : Comon.{v₁, u₁} C
f : X ⟶ Y
⊢ Eq.{v₁ + 1} (α := unop (unop (op X.ComonToMonOpOpObj)).X ⟶ unop (tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite)))
    (Quiver.Hom.unop (η ≫ f.hom.op)) (Quiver.Hom.unop η)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
X Y : Comon.{v₁, u₁} C
f : X ⟶ Y
a :
  Eq.{v₁ + 1} (α :=
    unop (unop (op X.ComonToMonOpOpObj)).X ⟶
      unop
        (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (unop (op Y.ComonToMonOpOpObj)).X
          (unop (op Y.ComonToMonOpOpObj)).X))
    (Quiver.Hom.unop (μ ≫ f.hom.op)) (Quiver.Hom.unop ((f.hom.op ⊗ₘ f.hom.op) ≫ μ))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (unop (op Y.ComonToMonOpOpObj)).X (unop (op Y.ComonToMonOpOpObj)).X ⟶
      (unop (op X.ComonToMonOpOpObj)).X)
    (μ ≫ f.hom.op) ((f.hom.op ⊗ₘ f.hom.op) ≫ μ)

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
X Y : Comon.{v₁, u₁} C
f : X ⟶ Y
⊢ Eq.{v₁ + 1} (α :=
    unop (unop (op X.ComonToMonOpOpObj)).X ⟶
      unop
        (tensorObj.{v₁, u₁} (𝒞 := Category.opposite) (unop (op Y.ComonToMonOpOpObj)).X
          (unop (op Y.ComonToMonOpOpObj)).X))
    (Quiver.Hom.unop (μ ≫ f.hom.op)) (Quiver.Hom.unop ((f.hom.op ⊗ₘ f.hom.op) ≫ μ))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Mon.{v₁, u₁} Cᵒᵖ
rw :
  Eq.{v₁ + 1} (α := unop A.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (unop A.X))
    (Quiver.Hom.unop (Iso.hom (λ_ A.X))) (Iso.inv (λ_ (unop A.X)))
⊢ Eq.{v₁ + 1} (α := unop A.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (unop A.X))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (unop A.X)) (Quiver.Hom.unop μ)
      (Quiver.Hom.unop η ▷ unop A.X))
    (Iso.inv (λ_ (unop A.X)))

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

Premises used: CategoryTheory.unop_whiskerRight, CategoryTheory.unop_comp, CategoryTheory.MonObj.one_mul
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Mon.{v₁, u₁} Cᵒᵖ
⊢ Eq.{v₁ + 1} (α := unop A.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (unop A.X))
    (Quiver.Hom.unop (Iso.hom (λ_ A.X))) (Iso.inv (λ_ (unop A.X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Mon.{v₁, u₁} Cᵒᵖ
rw :
  Eq.{v₁ + 1} (α := unop A.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Quiver.Hom.unop (Iso.hom (ρ_ A.X))) (Iso.inv (ρ_ (unop A.X)))
⊢ Eq.{v₁ + 1} (α := unop A.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (unop A.X)) (Quiver.Hom.unop μ)
      (unop A.X ◁ Quiver.Hom.unop η))
    (Iso.inv (ρ_ (unop A.X)))

Tactic:
rw [← unop_whiskerLeft, ← unop_comp, MonObj.mul_one]

Premises used: CategoryTheory.unop_comp, CategoryTheory.MonObj.mul_one, CategoryTheory.unop_whiskerLeft
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Mon.{v₁, u₁} Cᵒᵖ
⊢ Eq.{v₁ + 1} (α := unop A.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Quiver.Hom.unop (Iso.hom (ρ_ A.X))) (Iso.inv (ρ_ (unop A.X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Mon.{v₁, u₁} Cᵒᵖ
rw :
  Eq.{v₁ + 1} (α :=
    unop A.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (unop A.X)))
    (Quiver.Hom.unop (Iso.inv (α_ A.X A.X A.X) ≫ μ ▷ A.X ≫ μ))
    (Quiver.Hom.unop (μ ▷ A.X ≫ μ) ≫ Iso.hom (α_ (unop A.X) (unop A.X) (unop A.X)))
⊢ Eq.{v₁ + 1} (α :=
    unop A.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (unop A.X)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (unop A.X)) (Quiver.Hom.unop μ)
      (unop A.X ◁ Quiver.Hom.unop μ))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (unop A.X)) (Quiver.Hom.unop μ)
      (Quiver.Hom.unop μ ▷ unop A.X ≫ Iso.hom (α_ (unop A.X) (unop A.X) (unop A.X))))

Tactic:
rw [← unop_whiskerRight, ← unop_whiskerLeft, ← unop_comp_assoc, ← unop_comp,
      MonObj.mul_assoc_flip]

Premises used: CategoryTheory.unop_whiskerRight, CategoryTheory.unop_comp, CategoryTheory.unop_comp_assoc, CategoryTheory.unop_whiskerLeft, CategoryTheory.MonObj.mul_assoc_flip
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
A : Mon.{v₁, u₁} Cᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    unop A.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (tensorObj.{v₁, u₁} (𝒞 := inst) (unop A.X) (unop A.X)))
    (Quiver.Hom.unop (Iso.inv (α_ A.X A.X A.X) ≫ μ ▷ A.X ≫ μ))
    (Quiver.Hom.unop (μ ▷ A.X ≫ μ) ≫ Iso.hom (α_ (unop A.X) (unop A.X) (unop A.X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
X Y : (Mon.{v₁, u₁} Cᵒᵖ)ᵒᵖ
f : X ⟶ Y
a :
  Eq (α := op (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ op (MonOpOpToComonObj (unop X)).X)
    (Quiver.Hom.op (f.unop.hom.unop ≫ ε)) (Quiver.Hom.op ε)
⊢ Eq (α := (MonOpOpToComonObj (unop X)).X ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (f.unop.hom.unop ≫ ε) ε

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_inj
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
X Y : (Mon.{v₁, u₁} Cᵒᵖ)ᵒᵖ
f : X ⟶ Y
⊢ Eq (α := op (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ op (MonOpOpToComonObj (unop X)).X)
    (Quiver.Hom.op (f.unop.hom.unop ≫ ε)) (Quiver.Hom.op ε)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
X Y : (Mon.{v₁, u₁} Cᵒᵖ)ᵒᵖ
f : X ⟶ Y
a :
  Eq (α :=
    op (tensorObj.{v₁, u₁} (𝒞 := inst) (MonOpOpToComonObj (unop Y)).X (MonOpOpToComonObj (unop Y)).X) ⟶
      op (MonOpOpToComonObj (unop X)).X)
    (Quiver.Hom.op (f.unop.hom.unop ≫ Δ)) (Quiver.Hom.op (Δ ≫ (f.unop.hom.unop ⊗ₘ f.unop.hom.unop)))
⊢ Eq (α :=
    (MonOpOpToComonObj (unop X)).X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (MonOpOpToComonObj (unop Y)).X (MonOpOpToComonObj (unop Y)).X)
    (f.unop.hom.unop ≫ Δ) (Δ ≫ (f.unop.hom.unop ⊗ₘ f.unop.hom.unop))

Tactic:
apply Quiver.Hom.op_inj

Premises used: Quiver.Hom.op_inj
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
X Y : (Mon.{v₁, u₁} Cᵒᵖ)ᵒᵖ
f : X ⟶ Y
⊢ Eq (α :=
    op (tensorObj.{v₁, u₁} (𝒞 := inst) (MonOpOpToComonObj (unop Y)).X (MonOpOpToComonObj (unop Y)).X) ⟶
      op (MonOpOpToComonObj (unop X)).X)
    (Quiver.Hom.op (f.unop.hom.unop ≫ Δ)) (Quiver.Hom.op (Δ ≫ (f.unop.hom.unop ⊗ₘ f.unop.hom.unop)))

Tactic:
simp [op_tensorHom]

Premises used: CategoryTheory.op_tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : Comon.{v₁, u₁} C
⊢ (tensorObj (𝒞 := instCategory) A B).X = tensorObj.{v₁, u₁} (𝒞 := inst) A.X B.X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : ComonObj A
inst_4 : ComonObj B
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : ComonObj A
inst_4 : ComonObj B
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
    Δ
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A A) (tensorObj.{v₁, u₁} (𝒞 := inst) B B)) (Δ ⊗ₘ Δ)
      (Quiver.Hom.unop (tensorμ (op A) (op B) (op A) (op B))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
A B : C
inst_3 : ComonObj A
inst_4 : ComonObj B
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) A B ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) (tensorObj.{v₁, u₁} (𝒞 := inst) A B))
    Δ ((Δ ⊗ₘ Δ) ≫ tensorμ A A B B)

Tactic:
simp [tensorObj_comul']

Premises used: CategoryTheory.Comon.tensorObj_comul'
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶
      Functor.obj (C := Comon.{v₁, u₁} C) (forget C) ((𝟙_ (Comon.{v₁, u₁} C)) (𝒞 := instCategory)))
    («ε» (forget C)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj (C := Comon.{v₁, u₁} C) (forget C) ((𝟙_ (Comon.{v₁, u₁} C)) (𝒞 := instCategory)) ⟶
      tensorUnit.{v₁, u₁} C (𝒞 := inst))
    («η» (forget C)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : Comon.{v₁, u₁} C
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj (forget C) X) (Functor.obj (forget C) Y) ⟶
      Functor.obj (forget C) (tensorObj (𝒞 := instCategory) X Y))
    («μ» (forget C) X Y) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X.X Y.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X Y : Comon.{v₁, u₁} C
⊢ Eq (α :=
    Functor.obj (forget C) (tensorObj (𝒞 := instCategory) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (Functor.obj (forget C) X) (Functor.obj (forget C) Y))
    (δ (forget C) X Y) (𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X.X Y.X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X : C
inst_5 : ComonObj X
⊢ Eq (α := F.obj X ⟶ tensorUnit.{v₂, u₂} D (𝒞 := inst_2)) ε
    (CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map ε) (η F))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.OplaxMonoidal
X : C
inst_5 : ComonObj X
⊢ Eq (α := F.obj X ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_2) (F.obj X) (F.obj X)) Δ
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X X)) (F.map Δ) (δ F X X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.OplaxMonoidal
A : Comon.{v₁, u₁} C
w :
  Eq.{v₂ + 1} (α :=
    Comon.X.{v₂, u₂} { X := F.obj A.X, comon := obj.instComonObj A.X F : Comon.{v₂, u₂} D } ⟶
      Comon.X.{v₂, u₂} { X := F.obj A.X, comon := obj.instComonObj A.X F })
    (Comon.Hom.hom { hom := F.map (Comon.Hom.hom (𝟙 A)), isComonHom_hom := ⋯ })
    (Comon.Hom.hom (𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F }))
⊢ Eq.{v₂ + 1} (α :=
    Quiver.Hom (V := Comon.{v₂, u₂} D) { X := F.obj A.X, comon := obj.instComonObj A.X F }
      { X := F.obj A.X, comon := obj.instComonObj A.X F })
    { hom := F.map (Comon.Hom.hom (𝟙 A)), isComonHom_hom := ⋯ } (𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F })

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.OplaxMonoidal
A : Comon.{v₁, u₁} C
⊢ Eq.{v₂ + 1} (α :=
    Comon.X.{v₂, u₂} { X := F.obj A.X, comon := obj.instComonObj A.X F : Comon.{v₂, u₂} D } ⟶
      Comon.X.{v₂, u₂} { X := F.obj A.X, comon := obj.instComonObj A.X F })
    (Comon.Hom.hom { hom := F.map (Comon.Hom.hom (𝟙 A)), isComonHom_hom := ⋯ })
    (Comon.Hom.hom (𝟙 { X := F.obj A.X, comon := obj.instComonObj A.X F }))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Comon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
M N O : C
inst_2 : ComonObj M
inst_3 : ComonObj N
inst_4 : ComonObj O
D : Type u₂
inst_5 : Category.{v₂, u₂} D
inst_6 : MonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.OplaxMonoidal
X Y Z : Comon.{v₁, u₁} C
f : X ⟶ Y
g : Y ⟶ Z
w :
  Eq.{v₂ + 1} (α :=
    Comon.X.{v₂, u₂} { X := F.obj X.X, comon := obj.instComonObj X.X F : Comon.{v₂, u₂} D } ⟶
      Comon.X.{v₂, u₂} { X := F.obj Z.X, comon := obj.instComonObj Z.X F })
    (Comon.Hom.hom { hom := F.map (f ≫ g).hom, isComonHom_hom := ⋯ })
    (Comon.Hom.hom
      (CategoryStruct.comp (Y := { X := F.obj Y.X, comon := obj.instComonObj Y.X F })
        { hom := F.map f.hom, isComonHom_hom := ⋯ } { hom := F.map g.hom, isComonHom_hom := ⋯ }))
⊢ Eq.{v₂ + 1} (α :=
    Quiver.Hom (V := Comon.{v₂, u₂} D) { X := F.obj X.X, comon := obj.instComonObj X.X F }
      { X := F.obj Z.X, comon := obj.instComonObj Z.X F })
    { hom := F.map (f ≫ g).hom, isComonHom_hom := ⋯ }
    (CategoryStruct.comp (Y := { X := F.obj Y.X, comon := obj.instComonObj Y.X F })
      { hom := F.map f.hom, isComonHom_hom := ⋯ } { hom := F.map g.hom, isComonHom_hom := ⋯ })

Tactic:
ext