awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
x : X
w : Y
left : ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾f ≫ ↾g)).toFun x, f x) ∈ r.rel
right : (f x, (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x) ∈ (inv r).rel
⊢ ∃ (y : Y),
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾f ≫ ↾g)).toFun x, y) ∈ r.rel ∧
      (y, (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)).toFun x) ∈ (inv r).rel

Tactic:
use f x, (hg _).2, (hf _).2

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
h₁ :
  ∀ (y : Y),
    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾g ≫ ↾f)).toFun y =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 Y)).toFun y
⊢ ↾g ≫ ↾f = 𝟙 Y

Tactic:
ext y
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
y : Y
h₁ :
  ∃ (y_1 : X),
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾g ≫ ↾f)).toFun y, y_1) ∈ (inv r).rel ∧
      (y_1, (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 Y)).toFun y) ∈ r.rel
⊢ (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾g ≫ ↾f)).toFun y =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 Y)).toFun y

Tactic:
apply (h2 _ _).mp

Premises used: Iff.mp
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ (y : Y), (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ (y : X), (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : (x : X) → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : (x : Y) → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
y : Y
w : X
left : ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾g ≫ ↾f)).toFun y, g y) ∈ (inv r).rel
right : (g y, (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 Y)).toFun y) ∈ r.rel
⊢ ∃ (y_1 : X),
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (↾g ≫ ↾f)).toFun y, y_1) ∈ (inv r).rel ∧
      (y_1, (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 Y)).toFun y) ∈ r.rel

Tactic:
use g y, (hf (g y)).2, (hg y).2

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y : RelCat
f : X ≅ Y
⊢ IsIso (graphFunctor.map f.hom)

Tactic:
apply graphFunctor.map_isIso

Premises used: CategoryTheory.RelCat.graphFunctor, CategoryTheory.Functor.map_isIso
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
⊢ opFunctor ⋙ unopFunctor = 𝟭 RelCat

Tactic:
rfl

Premises used: Set.Mem, SetRel.inv, setOf, CategoryTheory.Functor.id, Set.preimage, Prod.swap, rfl
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
⊢ unopFunctor ⋙ opFunctor = 𝟭 RelCatᵒᵖ

Tactic:
rfl

Premises used: Set.Mem, Quiver.Hom.op, SetRel.inv, setOf, CategoryTheory.Functor.id, Set.preimage, Prod.swap, rfl
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y Z : RelCat
⊢ opEquivalence.functor.IsEquivalence

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Category.RelCat
Goal:
X Y Z : RelCat
⊢ opEquivalence.inverse.IsEquivalence

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
X : Type u_3
toTwoPointing : TwoPointing X
⊢ (of toTwoPointing).X = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
X : TwoP
⊢ X.toBipointed.X = X.X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
X Y : TwoP
f g : X ⟶ Y
h : f.hom = g.hom
⊢ f = g

Tactic:
InducedCategory.hom_ext h

Premises used: CategoryTheory.InducedCategory.hom_ext
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
⊢ swapEquiv.symm = swapEquiv

Tactic:
rfl

Premises used: TwoPointing.swap, Prod.Bipointed, CategoryTheory.InducedCategory.homMk, CategoryTheory.Functor.comp, TwoP.toBipointed, CategoryTheory.Functor.id, CategoryTheory.Iso.refl, TwoP.swap, TwoP.swapEquiv, CategoryTheory.Equivalence.symm, rfl
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
⊢ TwoP.swap ⋙
      forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC := fun (X : TwoP.{u_3}) ↦
        X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD := Bipointed.X) =
    forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC := fun (X : TwoP.{u_3}) ↦
        X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD := Bipointed.X) ⋙
      Bipointed.swap

Tactic:
rfl

Premises used: Prod.Bipointed, CategoryTheory.Functor.comp, TwoP.toBipointed, TwoP.swap, CategoryTheory.inducedFunctor, Prod.swap, rfl
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
⊢ pointedToTwoPFst ⋙ TwoP.swap = pointedToTwoPSnd

Tactic:
rfl

Premises used: TwoPointing.swap, CategoryTheory.InducedCategory.homMk, CategoryTheory.Functor.comp, pointedToTwoPSnd, rfl
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
⊢ pointedToTwoPSnd ⋙ TwoP.swap = pointedToTwoPFst

Tactic:
rfl

Premises used: TwoPointing.swap, CategoryTheory.InducedCategory.homMk, CategoryTheory.Functor.comp, pointedToTwoPFst, rfl
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
⊢ pointedToTwoPFst ⋙
      forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC := fun (X : TwoP.{u_3}) ↦
        X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD := Bipointed.X) =
    pointedToBipointedFst

Tactic:
rfl

Premises used: Prod.Bipointed, CategoryTheory.Functor.comp, TwoP.toBipointed, pointedToBipointedFst, rfl
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
⊢ pointedToTwoPSnd ⋙
      forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC := fun (X : TwoP.{u_3}) ↦
        X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD := Bipointed.X) =
    pointedToBipointedSnd

Tactic:
rfl

Premises used: Prod.Bipointed, CategoryTheory.Functor.comp, TwoP.toBipointed, pointedToBipointedSnd, rfl
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
            (InducedCategory.Hom.hom
              ((fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedFst)
                          Y) ↦
                  ({
                      hom :=
                        {
                          toFun := fun (o : (pointedToTwoPFst.obj X).toBipointed.X) ↦
                            Option.elim o Y.toTwoPointing.toProd.2 f.toFun,
                          map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPFst.obj X).toBipointed.Hom Y.toBipointed } } :
                    InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPFst.obj X) Y))
                ((fun (f : pointedToTwoPFst.obj X ⟶ Y) ↦
                    { toFun := f.hom.toFun ∘ some, map_point := ⋯ :
                      X.Hom
                        (Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedFst)
                          Y) })
                  f)))) :
        (pointedToTwoPFst.obj X).toBipointed.X → Y.toBipointed.X)
      none =
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X) f.hom) :
        (pointedToTwoPFst.obj X).toBipointed.X → Y.toBipointed.X)
      none

Tactic:
f.hom.map_snd.symm

Premises used: Bipointed.Hom.map_snd, CategoryTheory.InducedCategory.Hom.hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
⊢ (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
            (InducedCategory.Hom.hom
              ((fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedFst)
                          Y) ↦
                  ({
                      hom :=
                        {
                          toFun := fun (o : (pointedToTwoPFst.obj X).toBipointed.X) ↦
                            Option.elim o Y.toTwoPointing.toProd.2 f.toFun,
                          map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPFst.obj X).toBipointed.Hom Y.toBipointed } } :
                    InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPFst.obj X) Y))
                ((fun (f : pointedToTwoPFst.obj X ⟶ Y) ↦
                    { toFun := f.hom.toFun ∘ some, map_point := ⋯ :
                      X.Hom
                        (Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedFst)
                          Y) })
                  f)))) :
        (pointedToTwoPFst.obj X).toBipointed.X → Y.toBipointed.X)
      none =
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X) f.hom) :
        (pointedToTwoPFst.obj X).toBipointed.X → Y.toBipointed.X)
      none

Tactic:
exact f.hom.map_snd.symm

Premises used: Bipointed.Hom.map_snd, CategoryTheory.InducedCategory.Hom.hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPFst.obj X ⟶ Y
val : X.X
⊢ (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
            (InducedCategory.Hom.hom
              ((fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedFst)
                          Y) ↦
                  ({
                      hom :=
                        {
                          toFun := fun (o : (pointedToTwoPFst.obj X).toBipointed.X) ↦
                            Option.elim o Y.toTwoPointing.toProd.2 f.toFun,
                          map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPFst.obj X).toBipointed.Hom Y.toBipointed } } :
                    InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPFst.obj X) Y))
                ((fun (f : pointedToTwoPFst.obj X ⟶ Y) ↦
                    { toFun := f.hom.toFun ∘ some, map_point := ⋯ :
                      X.Hom
                        (Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedFst)
                          Y) })
                  f)))) :
        (pointedToTwoPFst.obj X).toBipointed.X → Y.toBipointed.X)
      (some val) =
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X) f.hom) :
        (pointedToTwoPFst.obj X).toBipointed.X → Y.toBipointed.X)
      (some val)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
            (InducedCategory.Hom.hom
              ((fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedSnd)
                          Y) ↦
                  ({
                      hom :=
                        {
                          toFun := fun (o : (pointedToTwoPSnd.obj X).toBipointed.X) ↦
                            Option.elim o Y.toTwoPointing.toProd.1 f.toFun,
                          map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPSnd.obj X).toBipointed.Hom Y.toBipointed } } :
                    InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPSnd.obj X) Y))
                ((fun (f : pointedToTwoPSnd.obj X ⟶ Y) ↦
                    { toFun := f.hom.toFun ∘ some, map_point := ⋯ :
                      X.Hom
                        (Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedSnd)
                          Y) })
                  f)))) :
        (pointedToTwoPSnd.obj X).toBipointed.X → Y.toBipointed.X)
      none =
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X) f.hom) :
        (pointedToTwoPSnd.obj X).toBipointed.X → Y.toBipointed.X)
      none

Tactic:
f.hom.map_fst.symm

Premises used: CategoryTheory.InducedCategory.Hom.hom, Bipointed.Hom.map_fst, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
⊢ (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
            (InducedCategory.Hom.hom
              ((fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedSnd)
                          Y) ↦
                  ({
                      hom :=
                        {
                          toFun := fun (o : (pointedToTwoPSnd.obj X).toBipointed.X) ↦
                            Option.elim o Y.toTwoPointing.toProd.1 f.toFun,
                          map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPSnd.obj X).toBipointed.Hom Y.toBipointed } } :
                    InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPSnd.obj X) Y))
                ((fun (f : pointedToTwoPSnd.obj X ⟶ Y) ↦
                    { toFun := f.hom.toFun ∘ some, map_point := ⋯ :
                      X.Hom
                        (Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedSnd)
                          Y) })
                  f)))) :
        (pointedToTwoPSnd.obj X).toBipointed.X → Y.toBipointed.X)
      none =
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X) f.hom) :
        (pointedToTwoPSnd.obj X).toBipointed.X → Y.toBipointed.X)
      none

Tactic:
exact f.hom.map_fst.symm

Premises used: CategoryTheory.InducedCategory.Hom.hom, Bipointed.Hom.map_fst, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.TwoP
Goal:
α : Type u_1
β : Type u_2
X : Pointed
Y : TwoP
f : pointedToTwoPSnd.obj X ⟶ Y
val : X.X
⊢ (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X)
            (InducedCategory.Hom.hom
              ((fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedSnd)
                          Y) ↦
                  ({
                      hom :=
                        {
                          toFun := fun (o : (pointedToTwoPSnd.obj X).toBipointed.X) ↦
                            Option.elim o Y.toTwoPointing.toProd.1 f.toFun,
                          map_fst := ⋯, map_snd := ⋯ : (pointedToTwoPSnd.obj X).toBipointed.Hom Y.toBipointed } } :
                    InducedCategory.Hom (D := Bipointed) (F := TwoP.toBipointed) (pointedToTwoPSnd.obj X) Y))
                ((fun (f : pointedToTwoPSnd.obj X ⟶ Y) ↦
                    { toFun := f.hom.toFun ∘ some, map_point := ⋯ :
                      X.Hom
                        (Functor.obj
                          (forget₂ TwoP (FC := fun (X Y : TwoP.{u_3}) ↦ X.toBipointed.HomSubtype Y.toBipointed) (CC :=
                              fun (X : TwoP.{u_3}) ↦ X.toBipointed.X) Bipointed (FD := Bipointed.HomSubtype) (CD :=
                              Bipointed.X) ⋙
                            bipointedToPointedSnd)
                          Y) })
                  f)))) :
        (pointedToTwoPSnd.obj X).toBipointed.X → Y.toBipointed.X)
      (some val) =
    (↑(ConcreteCategory.hom (FC := Bipointed.HomSubtype) (CC := Bipointed.X) f.hom) :
        (pointedToTwoPSnd.obj X).toBipointed.X → Y.toBipointed.X)
      (some val)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.ULift
Goal:
C : Type u_1
A : C
⊢ ULiftHom.objDown.{u_1, u_2} (ULiftHom.objUp A) = A

Tactic:
rfl

Premises used: CategoryTheory.ULiftHom.objUp, CategoryTheory.ULiftHom.objDown, rfl
-- Module: Mathlib.CategoryTheory.Category.ULift
Goal:
C : Type u_1
A : ULiftHom C
⊢ ULiftHom.objUp A.objDown = A

Tactic:
rfl

Premises used: CategoryTheory.ULiftHom.objUp, CategoryTheory.ULiftHom.objDown, rfl
-- Module: Mathlib.CategoryTheory.Category.ULift
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : AsSmall.{u_1, v₁, u₁} C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).down = f.down ≫ g.down

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.ULift
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : AsSmall.{u_1, v₁, u₁} C
h : X = Y
subst : ULift.down (eqToHom ⋯) = eqToHom ⋯
⊢ ULift.down (eqToHom h) = eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Category.ULift
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : AsSmall.{u_1, v₁, u₁} C
⊢ ULift.down (eqToHom ⋯) = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x y : CatCenter.{v, u} C
h : ∀ (X : C), x.app X = y.app X
⊢ x = y

Tactic:
NatTrans.ext (funext h)

Premises used: CategoryTheory.NatTrans.ext, CategoryTheory.End, funext
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
z : CatCenter.{v, u} C
X Y : C
f : X ⟶ Y
⊢ f ≫ z.app Y = z.app X ≫ f

Tactic:
NatTrans.naturality z f

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x y : CatCenter.{v, u} C
X : C
⊢ (x * y).app X = y.app X ≫ x.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x y : CatCenter.{v, u} C
X : C
rw : y.app X ≫ x.app X = x.app X ≫ y.app X
⊢ (x * y).app X = x.app X ≫ y.app X

Tactic:
rw [mul_app']

Premises used: CategoryTheory.CatCenter.mul_app'
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x y : CatCenter.{v, u} C
X : C
⊢ y.app X ≫ x.app X = x.app X ≫ y.app X

Tactic:
x.naturality (y.app X)

Premises used: CategoryTheory.CatCenter.naturality, CategoryTheory.CatCenter.app
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x y : CatCenter.{v, u} C
X : C
⊢ y.app X ≫ x.app X = x.app X ≫ y.app X

Tactic:
exact x.naturality (y.app X)

Premises used: CategoryTheory.CatCenter.naturality, CategoryTheory.CatCenter.app
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x y : CatCenter.{v, u} C
h : ∀ (X : C), (x * y).app X = (y * x).app X
⊢ x * y = y * x

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
x y : CatCenter.{v, u} C
X : C
h : y.app X ≫ x.app X = (y * x).app X
h₁ h₂ : y.app X ≫ x.app X = y.app X ≫ x.app X
⊢ (x * y).app X = (y * x).app X

Tactic:
rw [mul_app' x y, mul_app y x]

Premises used: CategoryTheory.CatCenter.mul_app, CategoryTheory.CatCenter.mul_app'
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
z : CatCenter.{v, u} C
X Y : C
f : X ⟶ Y
⊢ z • f = f ≫ z.app Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
z : CatCenter.{v, u} C
X Y : C
f : X ⟶ Y
⊢ z • f = z.app X ≫ f

Tactic:
z.naturality f

Premises used: CategoryTheory.CatCenter.naturality
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
z : (CatCenter.{v, u} C)ˣ
e : X ≅ Y
rw : e.hom ≫ ((↑z : CatCenter C) * (↑z⁻¹ : CatCenter C)).app Y ≫ e.inv = 𝟙 X
⊢ ((↑z : CatCenter C) • e.hom) ≫ ((↑z⁻¹ : CatCenter C) • e.inv) = 𝟙 X

Tactic:
rw [smul_eq, smul_eq', Category.assoc, ← mul_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CatCenter.mul_app_assoc, CategoryTheory.CatCenter.smul_eq', CategoryTheory.CatCenter.smul_eq
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
z : (CatCenter.{v, u} C)ˣ
e : X ≅ Y
⊢ e.hom ≫ ((↑z : CatCenter C) * (↑z⁻¹ : CatCenter C)).app Y ≫ e.inv = 𝟙 X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
z : (CatCenter.{v, u} C)ˣ
e : X ≅ Y
rw : e.inv ≫ ((↑z⁻¹ : CatCenter C) * (↑z : CatCenter C)).app X ≫ e.hom = 𝟙 Y
⊢ ((↑z⁻¹ : CatCenter C) • e.inv) ≫ ((↑z : CatCenter C) • e.hom) = 𝟙 Y

Tactic:
rw [smul_eq, smul_eq', Category.assoc, ← mul_app_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CatCenter.mul_app_assoc, CategoryTheory.CatCenter.smul_eq', CategoryTheory.CatCenter.smul_eq
-- Module: Mathlib.CategoryTheory.Center.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
z : (CatCenter.{v, u} C)ˣ
e : X ≅ Y
⊢ e.inv ≫ ((↑z⁻¹ : CatCenter C) * (↑z : CatCenter C)).app X ≫ e.hom = 𝟙 Y

Tactic:
simp