awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
⊢ IsZero G

Tactic:
⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩

Premises used: Unique.mk, Nonempty.intro, OfNat.ofNat, CategoryTheory.Limits.IsZero.mk, Inhabited.mk
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
refine_1 : ∀ (X : GrpCat.{u_1}) (f : G ⟶ X), f = default
refine_2 : ∀ (X : GrpCat.{u_1}) (f : X ⟶ G), f = default
⊢ IsZero G

Tactic:
refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : G ⟶ X
refine_1 :
  ∀ (x : (↑G : Type u_1)),
    Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
      ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
⊢ f = default

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : G ⟶ X
x : (↑G : Type u_1)
⊢ x = 1

Tactic:
have : x = 1 := Subsingleton.elim _ _
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : G ⟶ X
x : (↑G : Type u_1)
this : x = 1
refine_1 :
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
refine_1₁ :
  Eq.{u_1 + 1} (α := (↑X : Type u_1)) (1 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
refine_1₂ refine_1₃ : Eq.{u_1 + 1} (α := (↑X : Type u_1)) 1 1
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))

Tactic:
rw [this, map_one, map_one]

Premises used: map_one
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : X ⟶ G
refine_2 :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑G : Type u_1)) ((Hom.hom f : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))
      ((Hom.hom default : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))
⊢ f = default

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : GrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : GrpCat
f : X ⟶ G
x : (↑X : Type u_1)
⊢ Eq (α := (↑G : Type u_1)) ((Hom.hom f : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))
    ((Hom.hom default : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
⊢ HasZeroObject GrpCat

Tactic:
⟨⟨of PUnit, isZero_of_subsingleton _⟩⟩

Premises used: CategoryTheory.Limits.HasZeroObject.mk, GrpCat.isZero_of_subsingleton, PUnit, Exists.intro, GrpCat.of
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : GrpCat
h : IsZero G
⊢ Subsingleton.{u_1 + 1} (↑G : Type u_1)

Tactic:
(h.iso (isZero_of_subsingleton <| .of PUnit)).groupIsoToMulEquiv.subsingleton

Premises used: GrpCat.isZero_of_subsingleton, CategoryTheory.Iso.groupIsoToMulEquiv, MulEquiv.toEquiv, CategoryTheory.Limits.IsZero.iso, PUnit, Equiv.subsingleton, GrpCat.of
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : GrpCat
⊢ IsZero G ↔ Subsingleton.{u_1 + 1} (↑G : Type u_1)

Tactic:
⟨fun h ↦ subsingleton_of_isZero h, fun _ ↦ isZero_of_subsingleton G⟩

Premises used: GrpCat.isZero_of_subsingleton, GrpCat.subsingleton_of_isZero, Iff.intro
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : Type u_1
inst : Group G
⊢ IsZero (of G) ↔ Subsingleton G

Tactic:
isZero_iff_subsingleton

Premises used: GrpCat.isZero_iff_subsingleton
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
⊢ IsZero G

Tactic:
⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩

Premises used: Unique.mk, Nonempty.intro, OfNat.ofNat, CategoryTheory.Limits.IsZero.mk, Inhabited.mk
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
refine_1 : ∀ (X : CommGrpCat.{u_1}) (f : G ⟶ X), f = default
refine_2 : ∀ (X : CommGrpCat.{u_1}) (f : X ⟶ G), f = default
⊢ IsZero G

Tactic:
refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : G ⟶ X
refine_1 :
  ∀ (x : (↑G : Type u_1)),
    Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
      ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
⊢ f = default

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : G ⟶ X
x : (↑G : Type u_1)
⊢ x = 1

Tactic:
have : x = 1 := Subsingleton.elim _ _
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : G ⟶ X
x : (↑G : Type u_1)
this : x = 1
refine_1 :
  Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
refine_1₁ :
  Eq.{u_1 + 1} (α := (↑X : Type u_1)) (1 : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) 1 : (↑X : Type u_1))
refine_1₂ refine_1₃ : Eq.{u_1 + 1} (α := (↑X : Type u_1)) 1 1
⊢ Eq (α := (↑X : Type u_1)) ((Hom.hom f : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))
    ((Hom.hom default : (a : (↑G : Type u_1)) → (↑X : Type u_1)) x : (↑X : Type u_1))

Tactic:
rw [this, map_one, map_one]

Premises used: map_one
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : X ⟶ G
refine_2 :
  ∀ (x : (↑X : Type u_1)),
    Eq (α := (↑G : Type u_1)) ((Hom.hom f : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))
      ((Hom.hom default : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))
⊢ f = default

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : CommGrpCat
inst : Subsingleton.{u_1 + 1} (↑G : Type u_1)
X : CommGrpCat
f : X ⟶ G
x : (↑X : Type u_1)
⊢ Eq (α := (↑G : Type u_1)) ((Hom.hom f : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))
    ((Hom.hom default : (a : (↑X : Type u_1)) → (↑G : Type u_1)) x : (↑G : Type u_1))

Tactic:
subsingleton
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
⊢ HasZeroObject CommGrpCat

Tactic:
⟨⟨of PUnit, isZero_of_subsingleton _⟩⟩

Premises used: CommGrpCat.isZero_of_subsingleton, CategoryTheory.Limits.HasZeroObject.mk, CommGrpCat.of, PUnit, Exists.intro
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : CommGrpCat
h : IsZero G
⊢ Subsingleton.{u_1 + 1} (↑G : Type u_1)

Tactic:
(h.iso (isZero_of_subsingleton <| .of PUnit)).commGroupIsoToMulEquiv.subsingleton

Premises used: CommGrpCat.isZero_of_subsingleton, MulEquiv.toEquiv, CategoryTheory.Iso.commGroupIsoToMulEquiv, CommGrpCat.of, CategoryTheory.Limits.IsZero.iso, PUnit, Equiv.subsingleton
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : CommGrpCat
⊢ IsZero G ↔ Subsingleton.{u_1 + 1} (↑G : Type u_1)

Tactic:
⟨fun h ↦ subsingleton_of_isZero h, fun _ ↦ isZero_of_subsingleton G⟩

Premises used: CommGrpCat.isZero_of_subsingleton, CommGrpCat.subsingleton_of_isZero, Iff.intro
-- Module: Mathlib.Algebra.Category.Grp.Zero
Goal:
G : Type u_1
inst : CommGroup G
⊢ IsZero (of G) ↔ Subsingleton G

Tactic:
isZero_iff_subsingleton

Premises used: CommGrpCat.isZero_iff_subsingleton
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
X : GrpWithZero
⊢ ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u_1}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (𝟙 X) =
    MonoidWithZeroHom.id X.carrier

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
X Y Z : GrpWithZero
f : X ⟶ Y
g : Y ⟶ Z
⊢ ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u_1}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (f ≫ g) =
    MonoidWithZeroHom.comp g f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
X : GrpWithZero
⊢ Eq (α := (a : X.carrier) → X.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u_1}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (𝟙 X)) :
      (a : X.carrier) → X.carrier)
    id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
X Y Z : GrpWithZero
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := (a : X.carrier) → Z.carrier)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u_1}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier)
          (f ≫ g)) :
      (a : X.carrier) → Z.carrier)
    (Function.comp (β := Y.carrier)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u_1}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) g) :
        (a : Y.carrier) → Z.carrier)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u_1}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) f) :
        (a : X.carrier) → Y.carrier))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
X Y : GrpWithZero
f : X ⟶ Y
⊢ Eq (α :=
    (a :
        (fun (X : Type u_1) ↦ X)
          (Functor.obj
            (forget GrpWithZero (FC := fun (x1 x2 : GrpWithZero.{u_1}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier))
            X)) →
      (fun (X : Type u_1) ↦ X)
        (Functor.obj
          (forget GrpWithZero (FC := fun (x1 x2 : GrpWithZero.{u_1}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier)) Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map
            (forget GrpWithZero (FC := fun (x1 x2 : GrpWithZero.{u_1}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier))
            f)) :
      (a : (fun (X : Type u_1) ↦ X) ((forget GrpWithZero).obj X)) →
        (fun (X : Type u_1) ↦ X) ((forget GrpWithZero).obj Y))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u_1}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) f) :
      (a : X.carrier) → Y.carrier)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
α β : GrpWithZero
e : α.carrier ≃* β.carrier
h :
  ∀ (x : α.carrier),
    Eq (α := α.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (X := α)
              (Y := α)
              (CategoryStruct.comp (Y := β) (ofHom (↑e : α.carrier →*₀ β.carrier))
                (ofHom (↑e.symm : β.carrier →*₀ α.carrier))) :
            (a : α.carrier) → α.carrier)
          x :
        α.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (𝟙 α) :
            (a : α.carrier) → α.carrier)
          x :
        α.carrier)
⊢ CategoryStruct.comp (Y := β) (ofHom (↑e : α.carrier →*₀ β.carrier)) (ofHom (↑e.symm : β.carrier →*₀ α.carrier)) = 𝟙 α

Tactic:
ext
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
α β : GrpWithZero
e : α.carrier ≃* β.carrier
x : α.carrier
⊢ Eq (α := α.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (X := α)
            (Y := α)
            (CategoryStruct.comp (Y := β) (ofHom (↑e : α.carrier →*₀ β.carrier))
              (ofHom (↑e.symm : β.carrier →*₀ α.carrier))) :
          (a : α.carrier) → α.carrier)
        x :
      α.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (𝟙 α) :
          (a : α.carrier) → α.carrier)
        x :
      α.carrier)

Tactic:
e.symm_apply_apply _

Premises used: MulEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
α β : GrpWithZero
e : α.carrier ≃* β.carrier
x : α.carrier
⊢ Eq (α := α.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (X := α)
            (Y := α)
            (CategoryStruct.comp (Y := β) (ofHom (↑e : α.carrier →*₀ β.carrier))
              (ofHom (↑e.symm : β.carrier →*₀ α.carrier))) :
          (a : α.carrier) → α.carrier)
        x :
      α.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (𝟙 α) :
          (a : α.carrier) → α.carrier)
        x :
      α.carrier)

Tactic:
exact e.symm_apply_apply _

Premises used: MulEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
α β : GrpWithZero
e : α.carrier ≃* β.carrier
h :
  ∀ (x : β.carrier),
    Eq (α := β.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (X := β)
              (Y := β)
              (CategoryStruct.comp (Y := α) (ofHom (↑e.symm : β.carrier →*₀ α.carrier))
                (ofHom (↑e : α.carrier →*₀ β.carrier))) :
            (a : β.carrier) → β.carrier)
          x :
        β.carrier)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (𝟙 β) :
            (a : β.carrier) → β.carrier)
          x :
        β.carrier)
⊢ CategoryStruct.comp (Y := α) (ofHom (↑e.symm : β.carrier →*₀ α.carrier)) (ofHom (↑e : α.carrier →*₀ β.carrier)) = 𝟙 β

Tactic:
ext
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
α β : GrpWithZero
e : α.carrier ≃* β.carrier
x : β.carrier
⊢ Eq (α := β.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (X := β)
            (Y := β)
            (CategoryStruct.comp (Y := α) (ofHom (↑e.symm : β.carrier →*₀ α.carrier))
              (ofHom (↑e : α.carrier →*₀ β.carrier))) :
          (a : β.carrier) → β.carrier)
        x :
      β.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (𝟙 β) :
          (a : β.carrier) → β.carrier)
        x :
      β.carrier)

Tactic:
e.apply_symm_apply _

Premises used: MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Category.GrpWithZero
Goal:
α β : GrpWithZero
e : α.carrier ≃* β.carrier
x : β.carrier
⊢ Eq (α := β.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (X := β)
            (Y := β)
            (CategoryStruct.comp (Y := α) (ofHom (↑e.symm : β.carrier →*₀ α.carrier))
              (ofHom (↑e : α.carrier →*₀ β.carrier))) :
          (a : β.carrier) → β.carrier)
        x :
      β.carrier)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpWithZero.{u}) ↦ x1.carrier →*₀ x2.carrier) (CC := carrier) (𝟙 β) :
          (a : β.carrier) → β.carrier)
        x :
      β.carrier)

Tactic:
exact e.apply_symm_apply _

Premises used: MulEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : Ring X
inst_2 : HopfAlgebra R X
⊢ Eq.{v + 1} (α := carrier (of R X) →ₗ[R] TensorProduct R (carrier (of R X)) (carrier (of R X))) CoalgebraStruct.comul
    CoalgebraStruct.comul

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : Ring X
inst_2 : HopfAlgebra R X
⊢ Eq (α := LinearMap.{u, u, v, u} (RingHom.id R) (carrier (of R X)) R) CoalgebraStruct.counit CoalgebraStruct.counit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
V W : HopfAlgCat.{v, u} R
x x_1 : V.Hom W
f g : V.carrier →ₐc[R] W.carrier
h : { toBialgHom' := f : V.Hom W }.toBialgHom = { toBialgHom' := g }.toBialgHom
⊢ { toBialgHom' := f : V.Hom W } = { toBialgHom' := g }

Tactic:
congr
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : HopfAlgCat.{v, u} R
f g : X ⟶ Y
h : Hom.toBialgHom f = Hom.toBialgHom g
⊢ f = g

Tactic:
Hom.ext h

Premises used: HopfAlgCat.Hom.ext
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : HopfAlgCat.{v, u} R
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.toBialgHom (f ≫ g) = (Hom.toBialgHom g).comp (Hom.toBialgHom f)

Tactic:
rfl

Premises used: BialgHom.comp, rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
M : HopfAlgCat.{v, u} R
⊢ Hom.toBialgHom (𝟙 M) = BialgHom.id R M.carrier

Tactic:
rfl

Premises used: BialgHom.id, rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : HopfAlgCat.{u_1, u} R
⊢ Functor.obj
      (forget₂ (HopfAlgCat.{u_1, u} R) (FC := fun (x1 x2 : HopfAlgCat.{u_1, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier) (BialgCat.{u_1, u} R) (FD := fun (x1 x2 : BialgCat.{u_1, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
        BialgCat.carrier))
      X =
    BialgCat.of R X.carrier

Tactic:
rfl

Premises used: BialgCat.of, rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : HopfAlgCat.{u_1, u} R
f : X ⟶ Y
⊢ CategoryTheory.Functor.map
      (forget₂ (HopfAlgCat.{u_1, u} R) (FC := fun (x1 x2 : HopfAlgCat.{u_1, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier) (BialgCat.{u_1, u} R) (FD := fun (x1 x2 : BialgCat.{u_1, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CD :=
        BialgCat.carrier))
      f =
    BialgCat.ofHom (Hom.toBialgHom f)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : Ring X
inst_2 : HopfAlgebra R X
⊢ Eq (α := Iso (C := HopfAlgCat.{v, u} R) (of R X) (of R X)) (toHopfAlgIso (refl R X)) (Iso.refl (of R X))

Tactic:
rfl

Premises used: BialgEquiv.toHopfAlgIso, BialgHom.id, CategoryTheory.Iso.refl, BialgHomClass.toBialgHom, CoalgHom.id, rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : Type v
inst_1 : Ring X
inst_2 : Ring Y
inst_3 : HopfAlgebra R X
inst_4 : HopfAlgebra R Y
e : X ≃ₐc[R] Y
⊢ e.symm.toHopfAlgIso = e.toHopfAlgIso.symm

Tactic:
rfl

Premises used: BialgEquiv.toHopfAlgIso, CoalgHomClass.toCoalgHom, CoalgEquiv.symm, BialgEquiv.symm, CategoryTheory.Iso.symm, rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : Type v
inst_1 : Ring X
inst_2 : Ring Y
inst_3 : Ring Z
inst_4 : HopfAlgebra R X
inst_5 : HopfAlgebra R Y
inst_6 : HopfAlgebra R Z
e : X ≃ₐc[R] Y
f : Y ≃ₐc[R] Z
⊢ (e.trans f).toHopfAlgIso = e.toHopfAlgIso ≪≫ f.toHopfAlgIso

Tactic:
rfl

Premises used: BialgEquiv.toHopfAlgIso, CoalgHom.comp, CategoryTheory.Iso.trans, BialgHom.comp, BialgHomClass.toBialgHom, rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : HopfAlgCat.{v, u} R
i : X ≅ Y
⊢ (↑i.toHopfAlgEquiv : X.carrier →ₐc[R] Y.carrier) = i.hom.toBialgHom'

Tactic:
rfl

Premises used: BialgHomClass.toBialgHom, rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : HopfAlgCat.{v, u} R
⊢ toHopfAlgEquiv (refl X) = BialgEquiv.refl R X.carrier

Tactic:
rfl

Premises used: CoalgEquiv.refl, CategoryTheory.Iso.toHopfAlgEquiv, CoalgHom.id, rfl, BialgEquiv.refl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : HopfAlgCat.{v, u} R
e : X ≅ Y
⊢ e.symm.toHopfAlgEquiv = e.toHopfAlgEquiv.symm

Tactic:
rfl

Premises used: CoalgEquiv.symm, BialgEquiv.symm, CategoryTheory.Iso.toHopfAlgEquiv, rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y Z : HopfAlgCat.{v, u} R
e : X ≅ Y
f : Y ≅ Z
⊢ (e ≪≫ f).toHopfAlgEquiv = e.toHopfAlgEquiv.trans f.toHopfAlgEquiv

Tactic:
rfl

Premises used: BialgEquiv.trans, CoalgEquivClass.toCoalgEquiv, CoalgHom.comp, CoalgHomClass.toCoalgHom, CategoryTheory.Iso.toHopfAlgEquiv, CoalgEquiv.trans, rfl
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : HopfAlgCat.{v, u} R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget (HopfAlgCat.{v, u} R) (FC := fun (x1 x2 : HopfAlgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      X)
    (CategoryTheory.Functor.map
      (forget (HopfAlgCat.{v, u} R) (FC := fun (x1 x2 : HopfAlgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      f)
i : Functor.obj
    (forget (HopfAlgCat.{v, u} R) (FC := fun (x1 x2 : HopfAlgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
      carrier))
    X ≅
  Functor.obj
    (forget (HopfAlgCat.{v, u} R) (FC := fun (x1 x2 : HopfAlgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
      carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (HopfAlgCat.{v, u} R) (FC := fun (x1 x2 : HopfAlgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      f)
e : X.carrier ≃ₐc[R] Y.carrier :=
  let __src := Hom.toBialgHom f;
  let __src_1 := i.toEquiv;
  { toCoalgHom := __src.toCoalgHom, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
⟨e.toHopfAlgIso.isIso_hom.1⟩

Premises used: CategoryTheory.IsIso.mk, CategoryTheory.IsIso.out
-- Module: Mathlib.Algebra.Category.HopfAlgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : HopfAlgCat.{v, u} R
f : X ⟶ Y
h :
  IsIso (X :=
    Functor.obj
      (forget (HopfAlgCat.{v, u} R) (FC := fun (x1 x2 : HopfAlgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      X)
    (CategoryTheory.Functor.map
      (forget (HopfAlgCat.{v, u} R) (FC := fun (x1 x2 : HopfAlgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      f)
i : Functor.obj
    (forget (HopfAlgCat.{v, u} R) (FC := fun (x1 x2 : HopfAlgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
      carrier))
    X ≅
  Functor.obj
    (forget (HopfAlgCat.{v, u} R) (FC := fun (x1 x2 : HopfAlgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
      carrier))
    Y :=
  asIso
    (CategoryTheory.Functor.map
      (forget (HopfAlgCat.{v, u} R) (FC := fun (x1 x2 : HopfAlgCat.{v, u} R) ↦ x1.carrier →ₐc[R] x2.carrier) (CC :=
        carrier))
      f)
e : X.carrier ≃ₐc[R] Y.carrier :=
  let __src := Hom.toBialgHom f;
  let __src_1 := i.toEquiv;
  { toCoalgHom := __src.toCoalgHom, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
⊢ IsIso f

Tactic:
exact ⟨e.toHopfAlgIso.isIso_hom.1⟩
-- Module: Mathlib.Algebra.Category.ModuleCat.AB
Goal:
R : Type u
inst : Ring R
⊢ AB4.{u, u + 1} (ModuleCat R)

Tactic:
AB4.of_AB5 _

Premises used: CategoryTheory.AB4.of_AB5
-- Module: Mathlib.Algebra.Category.ModuleCat.AB
Goal:
R : Type u
inst : Ring R
inst_1 : Small.{v, u} R
X Y : ModuleCat.{v, u} R
f g : X ⟶ Y
h : ∀ (G : ModuleCat.{v, u} R), ObjectProperty.singleton (of R (Shrink.{v, u} R)) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ ∀ (h : of R (Shrink.{v, u} R) ⟶ X) (x : Shrink.{v, u} R),
    Eq (α := (↑Y : Type v))
      ((Hom.hom f : (a : (↑X : Type v)) → (↑Y : Type v))
          ((Hom.hom h : (a : Shrink.{v, u} R) → (↑X : Type v)) x : (↑X : Type v)) :
        (↑Y : Type v))
      ((Hom.hom g : (a : (↑X : Type v)) → (↑Y : Type v))
          ((Hom.hom h : (a : Shrink.{v, u} R) → (↑X : Type v)) x : (↑X : Type v)) :
        (↑Y : Type v))

Tactic:
simp only [ObjectProperty.singleton_iff, ModuleCat.hom_ext_iff, hom_comp,
    LinearMap.ext_iff, LinearMap.coe_comp, Function.comp_apply, forall_eq'] at h

Premises used: LinearMap.ext_iff, forall_eq', ModuleCat.hom_ext_iff, CategoryTheory.ObjectProperty.singleton_iff, LinearMap.coe_comp, Function.comp_apply, ModuleCat.hom_comp