awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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 ε ▷ op A.X ≫ Quiver.Hom.op Δ) (Iso.hom (λ_ (op A.X)))
have 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)))
Tactic: rw [← op_whiskerRight, ← op_comp, counit_comul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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)
    (op A.X ◁ Quiver.Hom.op ε ≫ Quiver.Hom.op Δ) (Iso.hom (ρ_ (op A.X)))
have 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)))
Tactic: rw [← op_whiskerLeft, ← op_comp, comul_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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 Δ ▷ 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 Δ)
have 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 ◁ Δ))
Tactic: rw [← op_inv_associator, ← op_whiskerRight, ← op_comp, ← op_whiskerLeft, ← op_comp,
      comul_assoc_flip, op_comp, op_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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} (α := tensorUnit.{v₁, u₁} Cᵒᵖ (𝒞 := Category.opposite) ⟶ (unop (op X.ComonToMonOpOpObj)).X) (η ≫ f.hom.op)
    η
have 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 η)
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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} (α :=
    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) ≫ μ)
have 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) ≫ μ))
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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))
    (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)))
have 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)))
Tactic: rw [← unop_whiskerRight, ← unop_comp, MonObj.one_mul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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)))
    (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)))
have 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)))
Tactic: rw [← unop_whiskerLeft, ← unop_comp, MonObj.mul_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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)))
    (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))))
have 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)))
Tactic: rw [← unop_whiskerRight, ← unop_whiskerLeft, ← unop_comp_assoc, ← unop_comp,
      MonObj.mul_assoc_flip]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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 (α := (MonOpOpToComonObj (unop X)).X ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (f.unop.hom.unop ≫ ε) ε
have a : Eq (α := op (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ op (MonOpOpToComonObj (unop X)).X)
  (Quiver.Hom.op (f.unop.hom.unop ≫ ε)) (Quiver.Hom.op ε)
Tactic: apply Quiver.Hom.op_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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 (α :=
    (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))
have 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)))
Tactic: apply Quiver.Hom.op_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map ε) (η F) ▷ F.obj A)
    (Iso.inv (λ_ (F.obj A)))
have simp_rw : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj A))
      (F.map ε ▷ F.obj A) (η F ▷ F.obj A))
  (Iso.inv (λ_ (F.obj A)))
Tactic: simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc, left_unitality,
      ← F.map_comp_assoc, counit_comul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
simp_rw :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj A))
        (F.map ε ▷ F.obj A) (η F ▷ F.obj A))
    (Iso.inv (λ_ (F.obj A)))
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map ε) (η F) ▷ F.obj A)
    (Iso.inv (λ_ (F.obj A)))
have simp_rw₁ : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
    (δ F A A ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj A))
        (F.map ε ▷ F.obj A) (η F ▷ F.obj A)))
  (Iso.inv (λ_ (F.obj A)))
Tactic: simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc, left_unitality,
      ← F.map_comp_assoc, counit_comul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
simp_rw :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj A))
        (F.map ε ▷ F.obj A) (η F ▷ F.obj A))
    (Iso.inv (λ_ (F.obj A)))
simp_rw₁ :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
      (δ F A A ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj A)) (F.map ε ▷ F.obj A)
          (η F ▷ F.obj A)))
    (Iso.inv (λ_ (F.obj A)))
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map ε) (η F) ▷ F.obj A)
    (Iso.inv (λ_ (F.obj A)))
have simp_rw₂ : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
      (F.map (ε ▷ A)) (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A ≫ η F ▷ F.obj A)))
  (Iso.inv (λ_ (F.obj A)))
Tactic: simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc, left_unitality,
      ← F.map_comp_assoc, counit_comul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
simp_rw :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj A))
        (F.map ε ▷ F.obj A) (η F ▷ F.obj A))
    (Iso.inv (λ_ (F.obj A)))
simp_rw₁ :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
      (δ F A A ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.obj A)) (F.map ε ▷ F.obj A)
          (η F ▷ F.obj A)))
    (Iso.inv (λ_ (F.obj A)))
simp_rw₂ :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
        (F.map (ε ▷ A)) (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A ≫ η F ▷ F.obj A)))
    (Iso.inv (λ_ (F.obj A)))
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map ε) (η F) ▷ F.obj A)
    (Iso.inv (λ_ (F.obj A)))
have simp_rw₃ : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)) (F.obj A))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
      (F.map (ε ▷ A)) (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A ≫ η F ▷ F.obj A)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A))
    (F.map (Iso.inv (λ_ A))) (δ F (tensorUnit.{v₁, u₁} C (𝒞 := inst)) A ≫ η F ▷ F.obj A))
Tactic: simp_rw [comp_whiskerRight, Category.assoc, δ_natural_left_assoc, left_unitality,
      ← F.map_comp_assoc, counit_comul]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map ε) (η F))
    (Iso.inv (ρ_ (F.obj A)))
have simp_rw : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
    CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (F.obj A ◁ F.map ε) (F.obj A ◁ η F))
  (Iso.inv (ρ_ (F.obj A)))
Tactic: simp_rw [MonoidalCategory.whiskerLeft_comp, Category.assoc, δ_natural_right_assoc,
      right_unitality, ← F.map_comp_assoc, comul_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
simp_rw :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (F.obj A ◁ F.map ε) (F.obj A ◁ η F))
    (Iso.inv (ρ_ (F.obj A)))
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map ε) (η F))
    (Iso.inv (ρ_ (F.obj A)))
have simp_rw₁ : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
    (δ F A A ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (F.obj A ◁ F.map ε) (F.obj A ◁ η F)))
  (Iso.inv (ρ_ (F.obj A)))
Tactic: simp_rw [MonoidalCategory.whiskerLeft_comp, Category.assoc, δ_natural_right_assoc,
      right_unitality, ← F.map_comp_assoc, comul_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
simp_rw :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (F.obj A ◁ F.map ε) (F.obj A ◁ η F))
    (Iso.inv (ρ_ (F.obj A)))
simp_rw₁ :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
      (δ F A A ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (F.obj A ◁ F.map ε)
          (F.obj A ◁ η F)))
    (Iso.inv (ρ_ (F.obj A)))
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map ε) (η F))
    (Iso.inv (ρ_ (F.obj A)))
have simp_rw₂ : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (F.map (A ◁ ε)) (δ F A (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj A ◁ η F)))
  (Iso.inv (ρ_ (F.obj A)))
Tactic: simp_rw [MonoidalCategory.whiskerLeft_comp, Category.assoc, δ_natural_right_assoc,
      right_unitality, ← F.map_comp_assoc, comul_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Comon_ (goal)
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
A : C
inst_7 : ComonObj A
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_8 : F.OplaxMonoidal
simp_rw :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (F.obj A ◁ F.map ε) (F.obj A ◁ η F))
    (Iso.inv (ρ_ (F.obj A)))
simp_rw₁ :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
      (δ F A A ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (F.obj A ◁ F.map ε)
          (F.obj A ◁ η F)))
    (Iso.inv (ρ_ (F.obj A)))
simp_rw₂ :
  Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
      (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
        (F.map (A ◁ ε)) (δ F A (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj A ◁ η F)))
    (Iso.inv (ρ_ (F.obj A)))
⊢ Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ) (δ F A A) ≫
      F.obj A ◁ CategoryStruct.comp (Y := F.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (F.map ε) (η F))
    (Iso.inv (ρ_ (F.obj A)))
have simp_rw₃ : Eq (α := F.obj A ⟶ tensorObj.{v₂, u₂} (𝒞 := inst_5) (F.obj A) (tensorUnit.{v₂, u₂} D (𝒞 := inst_5)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A A)) (F.map Δ)
    (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
      (F.map (A ◁ ε)) (δ F A (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj A ◁ η F)))
  (CategoryStruct.comp (Y := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) A (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (F.map (Iso.inv (ρ_ A))) (δ F A (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ≫ F.obj A ◁ η F))
Tactic: simp_rw [MonoidalCategory.whiskerLeft_comp, Category.assoc, δ_natural_right_assoc,
      right_unitality, ← F.map_comp_assoc, comul_counit]