awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.CatCommSq
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
T : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
L : Equivalence.{v_1, v_3, u_1, u_3} C₁ C₃
R : Equivalence.{v_2, v_4, u_2, u_4} C₂ C₄
B : Functor.{v_3, v_4, u_3, u_4} C₃ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ R.functor.map (T.map (L.unitIso.hom.app X)) ≫
      R.functor.map (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
        R.counit.app (R.functor.obj (T.obj (L.inverse.obj (L.functor.obj X)))) ≫
          (iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X)) ≫
            B.map (𝟙 (L.functor.obj ((L.functor ⋙ L.inverse).obj X))) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
X Y : C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ X
h : Z ⟶ Y
⊢ h ≫ g ≫ f = (h ≫ g) ≫ f

Tactic:
(Category.assoc h g f).symm

Premises used: CategoryTheory.Category.assoc, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
w : f = g
h : Y ⟶ Z
rw rw₁ : g ≫ h = g ≫ h
⊢ f ≫ h = g ≫ h

Tactic:
rw [w]
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f ≫ 𝟙 Y = g ≫ 𝟙 Y

Tactic:
w (𝟙 Y)

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
h : f = f ≫ 𝟙 Y
h₁ : g = g ≫ 𝟙 Y
⊢ f = g

Tactic:
convert! w (𝟙 Y)

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = f ≫ 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ g = g ≫ 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : Eq (α := {Z : C} → (h : Y ⟶ Z) → X ⟶ Z) (fun {Z : C} (h : Y ⟶ Z) ↦ f ≫ h) fun {Z : C} (h : Y ⟶ Z) ↦ g ≫ h
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
congr_fun (congr_fun w Z) h

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : Eq (α := {Z : C} → (h : Y ⟶ Z) → X ⟶ Z) (fun {Z : C} (h : Y ⟶ Z) ↦ f ≫ h) fun {Z : C} (h : Y ⟶ Z) ↦ g ≫ h
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h

Tactic:
convert! congr_fun (congr_fun w Z) h

Premises used: congr_fun
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f ≫ 𝟙 X = 𝟙 X

Tactic:
w (𝟙 X)

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
h : f = f ≫ 𝟙 X
⊢ f = 𝟙 X

Tactic:
convert! w (𝟙 X)

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X : C
f : X ⟶ X
w : ∀ {Y : C} (g : X ⟶ Y), f ≫ g = g
⊢ f = f ≫ 𝟙 X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : Prop
inst_1 : Decidable P
X Y Z : C
f : X ⟶ Y
g g' : Y ⟶ Z
⊢ (f ≫ if P then g else g') = if P then f ≫ g else f ≫ g'

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
P : Prop
inst_1 : Decidable P
X Y Z : C
f : X ⟶ Y
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
⊢ Eq (α := X ⟶ Z) (f ≫ if h : P then g h else g' h) (if h : P then f ≫ g h else f ≫ g' h)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y Z X Z_1 : C
g h : X ⟶ Z_1
w : 𝟙 X ≫ g = 𝟙 X ≫ h
⊢ g = h

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : Epi f
g h : Y ⟶ Z
⊢ f ≫ g = f ≫ h ↔ g = h

Tactic:
⟨fun p => Epi.left_cancellation g h p, congr_arg _⟩

Premises used: CategoryTheory.Epi.left_cancellation, congr_arg, Iff.intro
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : Epi f
g h : Y ⟶ Z
W : C
k l : Z ⟶ W
p : (f ≫ g) ≫ k = (f ≫ h) ≫ l
⊢ f ≫ g ≫ k = f ≫ h ≫ l

Tactic:
simpa using p
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : Epi f
g h : Y ⟶ Z
W : C
k l : Z ⟶ W
p : g ≫ k = h ≫ l
⊢ (f ≫ g) ≫ k = (f ≫ h) ≫ l

Tactic:
simp only [Category.assoc, p]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
h : Y ⟶ Y
⊢ f ≫ h = f ≫ 𝟙 Y ↔ h = 𝟙 Y

Tactic:
cancel_epi f

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
h : Y ⟶ Y
h₁ : f = f ≫ 𝟙 Y
⊢ f ≫ h = f ↔ h = 𝟙 Y

Tactic:
convert! cancel_epi f

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : Epi f
h : Y ⟶ Y
⊢ f = f ≫ 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst_1 : Epi f
g : Y ⟶ Z
inst_2 : Epi g
⊢ Epi (f ≫ g)

Tactic:
⟨fun _ _ w => (cancel_epi g).1 <| (cancel_epi_assoc_iff f).1 w⟩

Premises used: CategoryTheory.Epi.mk, CategoryTheory.cancel_epi_assoc_iff, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
⊢ Epi (f ≫ g)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : Epi (f ≫ g)
Z_1 : C
x x_1 : Z ⟶ Z_1
w : g ≫ x = g ≫ x_1
⊢ (f ≫ g) ≫ x = (f ≫ g) ≫ x_1

Tactic:
simp only [Category.assoc, w]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst_1 : Epi h
w : f ≫ g = h
⊢ Epi (f ≫ g)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : Epi (f ≫ g)
⊢ Epi g

Tactic:
epi_of_epi f g

Premises used: CategoryTheory.epi_of_epi
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : Epi (f ≫ g)
⊢ Epi g

Tactic:
exact epi_of_epi f g

Premises used: CategoryTheory.epi_of_epi
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ ∀ (Z : C), Function.Injective (β := X ⟶ Z) fun (g : Y ⟶ Z) ↦ f ≫ g

Tactic:
⟨fun _ _ _ _ hg ↦ (cancel_epi f).1 hg, fun h ↦ ⟨fun _ _ hg ↦ h _ hg⟩⟩

Premises used: CategoryTheory.Epi.mk, Iff.intro, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Category.Basic
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u
inst_1 : SmallCategory D
⊢ LargeCategory (ULift.{u + 1, u} D)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Type u_1
to_prod : X × X
⊢ (of to_prod).X = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
rw : g.toFun (f.toFun X.toProd.1) = Z.toProd.1
rw₁ : g.toFun Y.toProd.1 = Z.toProd.1
rw₂ rw₃ : Z.toProd.1 = Z.toProd.1
⊢ (g.toFun ∘ f.toFun) X.toProd.1 = Z.toProd.1

Tactic:
rw [Function.comp_apply, f.map_fst, g.map_fst]

Premises used: Function.comp_apply, Bipointed.Hom.map_fst
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
rw : g.toFun (f.toFun X.toProd.2) = Z.toProd.2
rw₁ : g.toFun Y.toProd.2 = Z.toProd.2
rw₂ rw₃ : Z.toProd.2 = Z.toProd.2
⊢ (g.toFun ∘ f.toFun) X.toProd.2 = Z.toProd.2

Tactic:
rw [Function.comp_apply, f.map_snd, g.map_snd]

Premises used: Bipointed.Hom.map_snd, Function.comp_apply
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
⊢ swapEquiv.symm = swapEquiv

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Iso.refl, Bipointed.swap, Bipointed.swapEquiv, Prod.swap, CategoryTheory.Equivalence.symm, rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
⊢ bipointedToPointedFst ⋙
      forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X) =
    forget Bipointed (FC := Bipointed.HomSubtype) (CC := Bipointed.X)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
⊢ bipointedToPointedSnd ⋙
      forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X) =
    forget Bipointed (FC := Bipointed.HomSubtype) (CC := Bipointed.X)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
⊢ Bipointed.swap ⋙ bipointedToPointedFst = bipointedToPointedSnd

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, bipointedToPointedSnd, Prod.swap, rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
⊢ Bipointed.swap ⋙ bipointedToPointedSnd = bipointedToPointedFst

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, Prod.swap, rfl, bipointedToPointedFst
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
⊢ pointedToBipointedFst ⋙ Bipointed.swap = pointedToBipointedSnd

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, pointedToBipointedSnd, Prod.swap, rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
⊢ pointedToBipointedSnd ⋙ Bipointed.swap = pointedToBipointedFst

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, pointedToBipointedFst, Prod.swap, rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
toFun :
  Bipointed.Hom.toFun
      ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedFst.obj X).Hom Y))
        ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
          f)) =
    f.toFun
⊢ (fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
        ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
            map_snd := ⋯ } :
          (pointedToBipointedFst.obj X).Hom Y))
      ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
          { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
        f) =
    f

Tactic:
apply Bipointed.Hom.ext

Premises used: Bipointed.Hom.ext
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
toFun :
  ∀ (x : (pointedToBipointedFst.obj X).X),
    Bipointed.Hom.toFun
        ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
            ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
                map_snd := ⋯ } :
              (pointedToBipointedFst.obj X).Hom Y))
          ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
              { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
            f))
        x =
      f.toFun x
⊢ Bipointed.Hom.toFun
      ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedFst.obj X).Hom Y))
        ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
          f)) =
    f.toFun

Tactic:
funext x
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
x : (pointedToBipointedFst.obj X).X
toFun :
  Bipointed.Hom.toFun (X := pointedToBipointedFst.obj X)
      ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedFst.obj X).Hom Y))
        ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
          f))
      none =
    f.toFun none
toFun₁ :
  ∀ (val : X.X),
    Bipointed.Hom.toFun (X := pointedToBipointedFst.obj X)
        ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
            ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
                map_snd := ⋯ } :
              (pointedToBipointedFst.obj X).Hom Y))
          ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
              { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
            f))
        (some val) =
      f.toFun (some val)
⊢ Bipointed.Hom.toFun
      ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedFst.obj X).Hom Y))
        ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
          f))
      x =
    f.toFun x

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ Bipointed.Hom.toFun (X := pointedToBipointedFst.obj X)
      ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedFst.obj X).Hom Y))
        ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
          f))
      none =
    f.toFun none

Tactic:
f.map_snd.symm

Premises used: Bipointed.Hom.map_snd, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ Bipointed.Hom.toFun (X := pointedToBipointedFst.obj X)
      ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedFst.obj X).Hom Y))
        ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
          f))
      none =
    f.toFun none

Tactic:
exact f.map_snd.symm

Premises used: Bipointed.Hom.map_snd, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
val : X.X
⊢ Bipointed.Hom.toFun (X := pointedToBipointedFst.obj X)
      ((fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedFst.obj X).Hom Y))
        ((fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) })
          f))
      (some val) =
    f.toFun (some val)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X' X : Pointed
Y : Bipointed
f : X' ⟶ X
g : X ⟶ bipointedToPointedFst.obj Y
⊢ Eq (α := Y.X)
    (Bipointed.Hom.toFun (X := pointedToBipointedFst.obj X')
      (({
              toFun := fun (f : pointedToBipointedFst.obj X' ⟶ Y) ↦
                { toFun := f.toFun ∘ some, map_point := ⋯ : X'.Hom (bipointedToPointedFst.obj Y) },
              invFun := fun (f : X' ⟶ bipointedToPointedFst.obj Y) ↦
                { toFun := fun (o : (pointedToBipointedFst.obj X').X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
                  map_snd := ⋯ : (pointedToBipointedFst.obj X').Hom Y },
              left_inv := ⋯, right_inv := ⋯ :
              (pointedToBipointedFst.obj X' ⟶ Y) ≃ (X' ⟶ bipointedToPointedFst.obj Y) }.symm :
          (a : X' ⟶ bipointedToPointedFst.obj Y) → pointedToBipointedFst.obj X' ⟶ Y)
        (f ≫ g))
      none)
    (Bipointed.Hom.toFun
      (pointedToBipointedFst.map f ≫
        ({
                toFun := fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
                  { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) },
                invFun := fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
                  { toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
                    map_snd := ⋯ : (pointedToBipointedFst.obj X).Hom Y },
                left_inv := ⋯, right_inv := ⋯ :
                (pointedToBipointedFst.obj X ⟶ Y) ≃ (X ⟶ bipointedToPointedFst.obj Y) }.symm :
            (a : X ⟶ bipointedToPointedFst.obj Y) → pointedToBipointedFst.obj X ⟶ Y)
          g)
      none)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X' X : Pointed
Y : Bipointed
f : X' ⟶ X
g : X ⟶ bipointedToPointedFst.obj Y
val : X'.X
⊢ Eq (α := Y.X)
    (Bipointed.Hom.toFun (X := pointedToBipointedFst.obj X')
      (({
              toFun := fun (f : pointedToBipointedFst.obj X' ⟶ Y) ↦
                { toFun := f.toFun ∘ some, map_point := ⋯ : X'.Hom (bipointedToPointedFst.obj Y) },
              invFun := fun (f : X' ⟶ bipointedToPointedFst.obj Y) ↦
                { toFun := fun (o : (pointedToBipointedFst.obj X').X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
                  map_snd := ⋯ : (pointedToBipointedFst.obj X').Hom Y },
              left_inv := ⋯, right_inv := ⋯ :
              (pointedToBipointedFst.obj X' ⟶ Y) ≃ (X' ⟶ bipointedToPointedFst.obj Y) }.symm :
          (a : X' ⟶ bipointedToPointedFst.obj Y) → pointedToBipointedFst.obj X' ⟶ Y)
        (f ≫ g))
      (some val))
    (Bipointed.Hom.toFun
      (pointedToBipointedFst.map f ≫
        ({
                toFun := fun (f : pointedToBipointedFst.obj X ⟶ Y) ↦
                  { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedFst.obj Y) },
                invFun := fun (f : X ⟶ bipointedToPointedFst.obj Y) ↦
                  { toFun := fun (o : (pointedToBipointedFst.obj X).X) ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯,
                    map_snd := ⋯ : (pointedToBipointedFst.obj X).Hom Y },
                left_inv := ⋯, right_inv := ⋯ :
                (pointedToBipointedFst.obj X ⟶ Y) ≃ (X ⟶ bipointedToPointedFst.obj Y) }.symm :
            (a : X ⟶ bipointedToPointedFst.obj Y) → pointedToBipointedFst.obj X ⟶ Y)
          g)
      (some val))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
toFun :
  Bipointed.Hom.toFun
      ((fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedSnd.obj X).Hom Y))
        ((fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) })
          f)) =
    f.toFun
⊢ (fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
        ({ toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
            map_snd := ⋯ } :
          (pointedToBipointedSnd.obj X).Hom Y))
      ((fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
          { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) })
        f) =
    f

Tactic:
apply Bipointed.Hom.ext

Premises used: Bipointed.Hom.ext
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
toFun :
  ∀ (x : (pointedToBipointedSnd.obj X).X),
    Bipointed.Hom.toFun
        ((fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
            ({ toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
                map_snd := ⋯ } :
              (pointedToBipointedSnd.obj X).Hom Y))
          ((fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
              { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) })
            f))
        x =
      f.toFun x
⊢ Bipointed.Hom.toFun
      ((fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedSnd.obj X).Hom Y))
        ((fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) })
          f)) =
    f.toFun

Tactic:
funext x
-- Module: Mathlib.CategoryTheory.Category.Bipointed
Goal:
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
x : (pointedToBipointedSnd.obj X).X
toFun :
  Bipointed.Hom.toFun (X := pointedToBipointedSnd.obj X)
      ((fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedSnd.obj X).Hom Y))
        ((fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) })
          f))
      none =
    f.toFun none
toFun₁ :
  ∀ (val : X.X),
    Bipointed.Hom.toFun (X := pointedToBipointedSnd.obj X)
        ((fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
            ({ toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
                map_snd := ⋯ } :
              (pointedToBipointedSnd.obj X).Hom Y))
          ((fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
              { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) })
            f))
        (some val) =
      f.toFun (some val)
⊢ Bipointed.Hom.toFun
      ((fun (f : X ⟶ bipointedToPointedSnd.obj Y) ↦
          ({ toFun := fun (o : (pointedToBipointedSnd.obj X).X) ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯,
              map_snd := ⋯ } :
            (pointedToBipointedSnd.obj X).Hom Y))
        ((fun (f : pointedToBipointedSnd.obj X ⟶ Y) ↦
            { toFun := f.toFun ∘ some, map_point := ⋯ : X.Hom (bipointedToPointedSnd.obj Y) })
          f))
      x =
    f.toFun x

Tactic:
cases x