awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ)
    (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ)
have h₁ : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (fst B B) =
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (fst B B)
Tactic: apply CartesianMonoidalCategory.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
A B : C
inst_2 : GrpObj A
inst_3 : GrpObj B
f : A ⟶ B
inst_4 : IsMonHom f
h₁ :
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (fst B B) =
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
      (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (fst B B)
⊢ Eq (α := A ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ)
    (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ)
have h₂ : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (lift (lift f (@inv _ _ inst_1 _ _ ≫ f)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (snd B B) =
  CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B)
    (lift (lift f (f ≫ @inv _ _ inst_1 _ _)) f ≫ Iso.hom (α_ B B B) ≫ B ◁ μ) (snd B B)
Tactic: apply CartesianMonoidalCategory.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
this : Eq.{v₁ + 1} (α := X ⟶ X) (@inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)
⊢ h₁ = h₂
have mk : ∀ [toMonObj : MonObj X] (inv : X ⟶ X)
  (left_inv :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift inv (𝟙 X)) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)
  (right_inv :
    CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (𝟙 X) inv) μ =
      CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)
  (e : Eq.{v₁ + 1} (α := MonObj X) GrpObj.toMonObj GrpObj.toMonObj)
  (this : Eq.{v₁ + 1} (α := X ⟶ X) (@GrpObj.inv _ _ inst_1 _ _) (@GrpObj.inv _ _ inst_1 _ _)),
  { toMonObj := toMonObj, inv := inv, left_inv := left_inv, right_inv := right_inv : GrpObj X } = h₂
Tactic: cases h₁
Cleared hypotheses: h₁, e, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
⊢ h₁ = h₂
have suffices : Eq.{v₁ + 1} (α := X ⟶ X) (@inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)
Tactic: suffices h₁.inv = h₂.inv by cases h₁; congr!
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
⊢ Eq.{v₁ + 1} (α := X ⟶ X) (@inv _ _ inst_1 _ _) (@inv _ _ inst_1 _ _)
have apply : Eq.{v₁ + 1} (α := X ⟶ X)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
Tactic: apply lift_left_mul_ext (𝟙 _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
⊢ Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
have rw : Eq.{v₁ + 1} (α := X ⟶ X)
  (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)
Tactic: rw [left_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
⊢ Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)
have h : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ
Tactic: convert! @left_inv _ _ _ _ h₁ using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
X : C
h₁ h₂ : GrpObj X
e : Eq.{v₁ + 1} (α := MonObj X) toMonObj toMonObj
h : Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X X ⟶ X) μ μ
⊢ Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) X X) (lift (@inv _ _ inst_1 _ _) (𝟙 X)) μ)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (toUnit X) η)
have h₃ : Eq.{v₁ + 1} (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ X) η η
Tactic: convert! @left_inv _ _ _ _ h₁ using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G_1 X_1 : C
inst_2 : GrpObj G_1
A B G : C
inst_3 : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ Eq (α := Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) Y)
    (Functor.map (Functor.obj yoneda G) f ≫
      (fun (X : Cᵒᵖ) ↦
          (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
            Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
        Y)
    ((fun (X : Cᵒᵖ) ↦
          (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
            Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
        X ≫
      Functor.map (Functor.obj yoneda G) f)
have h₁ : ∀ (g : Functor.obj (Functor.obj yoneda G) X),
  Eq (α := Functor.obj (Functor.obj yoneda G) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj yoneda G) f ≫
          (fun (X : Cᵒᵖ) ↦
              (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
                Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
            Y))
      g)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (X : Cᵒᵖ) ↦
              (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
                Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
            X ≫
          Functor.map (Functor.obj yoneda G) f))
      g)
Tactic: ext g
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G_1 X_1 : C
inst_2 : GrpObj G_1
A B G : C
inst_3 : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
g : Functor.obj (Functor.obj yoneda G) X
⊢ Eq (α := Functor.obj (Functor.obj yoneda G) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj yoneda G) f ≫
          (fun (X : Cᵒᵖ) ↦
              (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
                Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
            Y))
      g)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((fun (X : Cᵒᵖ) ↦
              (↾fun (f : Functor.obj (Functor.obj yoneda G) X) ↦ @Invertible.invOf _ MulOne.toMul MulOne.toOne f _ :
                Functor.obj (Functor.obj yoneda G) X ⟶ Functor.obj (Functor.obj yoneda G) X))
            X ≫
          Functor.map (Functor.obj yoneda G) f))
      g)
have h₁ : f.unop ≫ @Invertible.invOf _ MulOne.toMul MulOne.toOne g _ * f.unop ≫ g = 1
Tactic: simp only [yoneda_obj_obj, yoneda_obj_map, TypeCat.Fun.toFun_apply, comp_apply,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, invOf_eq_iff_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G_1 X_1 : C
inst_2 : GrpObj G_1
A B G : C
inst_3 : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
g : Functor.obj (Functor.obj yoneda G) X
⊢ f.unop ≫ @Invertible.invOf _ MulOne.toMul MulOne.toOne g _ * f.unop ≫ g = 1
have h₁ : f.unop ≫ (@Invertible.invOf _ MulOne.toMul MulOne.toOne g _ * g) = 1
Tactic: rw [← comp_mul, invOf_mul_self, comp_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G_1 X_1 : C
inst_2 : GrpObj G_1
A B G : C
inst_3 : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
g : Functor.obj (Functor.obj yoneda G) X
h₁ : f.unop ≫ (@Invertible.invOf _ MulOne.toMul MulOne.toOne g _ * g) = 1
⊢ f.unop ≫ @Invertible.invOf _ MulOne.toMul MulOne.toOne g _ * f.unop ≫ g = 1
have h₂ : Eq (α := Opposite.unop Y ⟶ G) (f.unop ≫ 1) 1
Tactic: rw [← comp_mul, invOf_mul_self, comp_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
G_1 X_1 : C
inst_2 : GrpObj G_1
A B G : C
inst_3 : MonObj G
h : (X : C) → (f : X ⟶ G) → Invertible f
X Y : Cᵒᵖ
f : X ⟶ Y
g : Functor.obj (Functor.obj yoneda G) X
h₁ : f.unop ≫ (@Invertible.invOf _ MulOne.toMul MulOne.toOne g _ * g) = 1
h₂ : Eq (α := Opposite.unop Y ⟶ G) (f.unop ≫ 1) 1
⊢ f.unop ≫ @Invertible.invOf _ MulOne.toMul MulOne.toOne g _ * f.unop ≫ g = 1
have h₃ : Eq.{v₁ + 1} (α := Opposite.unop Y ⟶ G) 1 1
Tactic: rw [← comp_mul, invOf_mul_self, comp_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H H₁ H₂ X₁ Y₁ X₂ Y₂ : Grp.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α := tensorObj (𝒞 := instCategory) X₁ X₂ ⟶ tensorObj (𝒞 := instCategory) Y₁ Y₂) (f ⊗ₘ g) (f ▷ X₂ ≫ Y₁ ◁ g)
have h : Eq (α := (tensorObj (𝒞 := instCategory) X₁ X₂).toMon.X ⟶ (tensorObj (𝒞 := instCategory) Y₁ Y₂).toMon.X)
  (Hom.hom (InducedCategory.Hom.hom (f ⊗ₘ g))) (Hom.hom (InducedCategory.Hom.hom (f ▷ X₂ ≫ Y₁ ◁ g)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G H H₁ H₂ x x_1 : Grp.{v₁, u₁} C
⊢ Eq (α :=
    tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))) x_1 ⟶
      tensorObj (𝒞 := instCategory) x x_1)
    (Iso.hom (α_ x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)) x_1) ≫ x ◁ Iso.hom (λ_ x_1)) (Iso.hom (ρ_ x) ▷ x_1)
have h : Eq (α :=
  (tensorObj (𝒞 := instCategory) (tensorObj (𝒞 := instCategory) x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)))
          x_1).toMon.X ⟶
    (tensorObj (𝒞 := instCategory) x x_1).toMon.X)
  (Hom.hom
    (InducedCategory.Hom.hom (Iso.hom (α_ x ((𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)) x_1) ≫ x ◁ Iso.hom (λ_ x_1))))
  (Hom.hom (InducedCategory.Hom.hom (Iso.hom (ρ_ x) ▷ x_1)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G_1 H H₁ H₂ G : Grp.{v₁, u₁} C
f : G ⟶ (𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory)
⊢ f = (fun (G : Grp.{v₁, u₁} C) ↦ (homMk' (toUnit G.toMon) : G ⟶ (𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))) G
have h : f.hom.hom =
  Hom.hom
    (InducedCategory.Hom.hom
      ((fun (G : Grp.{v₁, u₁} C) ↦ (homMk' (toUnit G.toMon) : G ⟶ (𝟙_ (Grp.{v₁, u₁} C)) (𝒞 := instCategory))) G))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G_1 H_1 H₁ H₂ G H : Grp.{v₁, u₁} C
⊢ Eq (α := tensorObj (𝒞 := instCategory) G H ⟶ G) (homMk' (fst G.toMon H.toMon))
    (G ◁ IsTerminal.from (IsTerminal.ofUniqueHom (fun (G : Grp.{v₁, u₁} C) ↦ homMk' (toUnit G.toMon)) ⋯) H ≫
      Iso.hom (ρ_ G))
have h : Eq (α := (tensorObj (𝒞 := instCategory) G H).toMon.X ⟶ G.toMon.X)
  (Hom.hom (InducedCategory.Hom.hom (homMk' (fst G.toMon H.toMon))))
  (Hom.hom
    (InducedCategory.Hom.hom
      (G ◁ IsTerminal.from (IsTerminal.ofUniqueHom (fun (G : Grp.{v₁, u₁} C) ↦ homMk' (toUnit G.toMon)) sorry) H ≫
        Iso.hom (ρ_ G))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
G_1 H_1 H₁ H₂ G H : Grp.{v₁, u₁} C
⊢ Eq (α := tensorObj (𝒞 := instCategory) G H ⟶ H) (homMk' (snd G.toMon H.toMon))
    (IsTerminal.from (IsTerminal.ofUniqueHom (fun (G : Grp.{v₁, u₁} C) ↦ homMk' (toUnit G.toMon)) ⋯) G ▷ H ≫
      Iso.hom (λ_ H))
have h : Eq (α := (tensorObj (𝒞 := instCategory) G H).toMon.X ⟶ H.toMon.X)
  (Hom.hom (InducedCategory.Hom.hom (homMk' (snd G.toMon H.toMon))))
  (Hom.hom
    (InducedCategory.Hom.hom
      (IsTerminal.from (IsTerminal.ofUniqueHom (fun (G : Grp.{v₁, u₁} C) ↦ homMk' (toUnit G.toMon)) sorry) G ▷ H ≫
        Iso.hom (λ_ H))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
G : Grp.{v₂, u₂} D
H : C
e : F.obj H ≅ G.X
this_1 : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
⊢ essImage (C := Grp.{v₁, u₁} C) F.mapGrp G
have refine_1 : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.X) (η ≫ e.hom) η
Tactic: refine ⟨⟨H⟩, ⟨Grp.mkIso e ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Grp (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : CartesianMonoidalCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.Monoidal
inst_5 : F.Full
inst_6 : F.Faithful
G : Grp.{v₂, u₂} D
H : C
e : F.obj H ≅ G.X
this_1 : GrpObj (F.obj H) := GrpObj.ofIso e.symm
this : GrpObj H := (FullyFaithful.ofFullyFaithful F).grpObj H
refine_1 : Eq (α := tensorUnit.{v₂, u₂} D (𝒞 := inst_2) ⟶ G.X) (η ≫ e.hom) η
⊢ essImage (C := Grp.{v₁, u₁} C) F.mapGrp G
have refine_2 : Eq (α :=
  tensorObj.{v₂, u₂} (𝒞 := inst_2) (Grp.X (obj (C := Grp.{v₁, u₁} C) F.mapGrp { X := H, grp := this : Grp.{v₁, u₁} C }))
      (Grp.X (obj (C := Grp.{v₁, u₁} C) F.mapGrp { X := H, grp := this : Grp.{v₁, u₁} C })) ⟶
    G.X)
  (μ ≫ e.hom) ((e.hom ⊗ₘ e.hom) ≫ μ)
Tactic: refine ⟨⟨H⟩, ⟨Grp.mkIso e ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ f ≫ @antipode _ _ inst_1 inst_2 _ _ = @antipode _ _ inst_1 inst_2 _ _ ≫ f
have hba : f ≫ @antipode _ _ inst_1 inst_2 _ _ * f = 1
Tactic: apply left_inv_eq_right_inv
    (M := Conv A B)
    (a := f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
hba : f ≫ @antipode _ _ inst_1 inst_2 _ _ * f = 1
⊢ f ≫ @antipode _ _ inst_1 inst_2 _ _ = @antipode _ _ inst_1 inst_2 _ _ ≫ f
have hac : f * @antipode _ _ inst_1 inst_2 _ _ ≫ f = 1
Tactic: apply left_inv_eq_right_inv
    (M := Conv A B)
    (a := f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ f ≫ @antipode _ _ inst_1 inst_2 _ _ * f = 1
have hba : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    ((f ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ B ◁ f ≫ μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: rw [Conv.mul_eq, Conv.one_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      ((f ≫ @antipode _ _ inst_1 inst_2 _ _) ▷ A ≫ B ◁ f ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hba : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (f ▷ A ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ B ◁ f ≫ μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: simp only [comp_whiskerRight, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
| @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ B ◁ f
have a : B ◁ f ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B
Tactic: rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ A ≫ B ◁ f ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hba : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
    (f ▷ A ≫ (B ◁ f ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) ≫ μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: slice_lhs 3 4 =>
      rw [← whisker_exchange]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
| f ▷ A ≫ B ◁ f
have a : f ⊗ₘ f
Tactic: rw [← tensorHom_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (f ▷ A ≫ (B ◁ f ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hba : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ (((f ⊗ₘ f) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) ≫ μ) =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: slice_lhs 2 3 =>
      rw [← tensorHom_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
| Δ ≫ (f ⊗ₘ f)
have a : f ≫ Δ
Tactic: rw [← IsComonHom.hom_comul f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) A A) Δ
      (((f ⊗ₘ f) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) ≫ μ) =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hba : CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) ((f ≫ Δ) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) μ =
  CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: slice_lhs 1 2 =>
      rw [← IsComonHom.hom_comul f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
| CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) Δ (@antipode _ _ inst_1 inst_2 _ _ ▷ B ≫ μ)
have a : CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
Tactic: rw [antipode_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) B B) ((f ≫ Δ) ≫ @antipode _ _ inst_1 inst_2 _ _ ▷ B) μ =
    CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η
have hba : Eq (α := Conv A B) (f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: slice_lhs 2 4 =>
      rw [antipode_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
| f ≫ ε
have a : ε
Tactic: rw [IsComonHom.hom_counit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Hopf_ (goal)
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 : HopfObj A
inst_4 : HopfObj B
f : A ⟶ B
inst_5 : IsBimonHom f
⊢ Eq (α := Conv A B) (f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
    (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
have slice_lhs : Eq (α := Conv A B) (f ≫ CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
  (CategoryStruct.comp (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) ε η)
Tactic: slice_lhs 1 2 =>
      rw [IsComonHom.hom_counit]