awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Limit (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ m = limitConeLift F s
have symm : limitConeLift F s = m
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Limit (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ limitConeLift F s = m
have h : (limitConeLift F s).toFunctor = m.toFunctor
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Limit (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
⊢ (limitConeLift F s).toFunctor = m.toFunctor
have h : ∀ (X : (↑s.pt : Type v)), (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X
Tactic: refine CategoryTheory.Functor.ext ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Limit (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
h : ∀ (X : (↑s.pt : Type v)), (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X
⊢ (limitConeLift F s).toFunctor = m.toFunctor
have h₁ : ∀ (X Y : (↑s.pt : Type v)) (f : X ⟶ Y), (limitConeLift F s).toFunctor.map f = eqToHom sorry ≫ m.toFunctor.map f ≫ eqToHom sorry
Tactic: refine CategoryTheory.Functor.ext ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Limit (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X : (↑s.pt : Type v)
⊢ (limitConeLift F s).toFunctor.obj X = m.toFunctor.obj X
have h : ∀ (j : J),
  Eq (α := (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
        ((limitConeLift F s).toFunctor.obj X) :
      (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
    ((hom (FC := TypeCat.Fun) (limit.π (F ⋙ objects) j) :
          (a : (fun (X : Type v) ↦ X) (limit (F ⋙ objects))) → (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
        (m.toFunctor.obj X) :
      (fun (X : Type v) ↦ X) ((F ⋙ objects).obj j))
Tactic: apply Types.limit_ext.{v, v}
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Limit (hypothesis)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ Cat
s : Cone F
m : s.pt ⟶ (limitCone F).pt
w : ∀ (j : J), m ≫ (limitCone F).π.app j = s.π.app j
X Y : (↑s.pt : Type v)
f : X ⟶ Y
⊢ (limitConeLift F s).toFunctor.map f = eqToHom ⋯ ≫ m.toFunctor.map f ≫ eqToHom ⋯
have this : ∀ (j : J),
  Eq (α :=
    Quiver.Hom (V := (↑(F.obj j) : Type v)) (Functor.obj (Hom.toFunctor (s.π.app j)) X)
      (Functor.obj (Hom.toFunctor (s.π.app j)) Y))
    (Functor.map (Hom.toFunctor (s.π.app j)) f)
    (eqToHom sorry ≫ Functor.map (Hom.toFunctor (m ≫ (limitCone F).π.app j)) f ≫ eqToHom sorry)
Tactic: have (j : _) := Functor.congr_hom congr($((w j).symm).toFunctor) f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat.Terminal (hypothesis)
Goal:
⊢ HasTerminal Cat
have this : IsDiscrete.{v, u} (ShrinkHoms.{u} PUnit.{u + 1})
Tactic: have : IsDiscrete (ShrinkHoms.{u} PUnit.{u + 1}) := {
    subsingleton _ _ := { allEq _ _ := eq_of_comp_right_eq (congrFun rfl) }
    eq_of_hom _ := rfl
  }
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
C D : Cat
F : C ⟶ D
⊢ 𝟙 C ≫ F = F
have ofFunctor : ∀ (toFunctor : Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u)),
  𝟙 C ≫ { toFunctor := toFunctor : C.Hom D } = { toFunctor := toFunctor }
Tactic: cases F
Cleared hypotheses: F
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
C D : Cat
F : C ⟶ D
⊢ F ≫ 𝟙 D = F
have ofFunctor : ∀ (toFunctor : Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u)),
  { toFunctor := toFunctor : C.Hom D } ≫ 𝟙 D = { toFunctor := toFunctor : C.Hom D }
Tactic: cases F
Cleared hypotheses: F
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
C D : Cat
F G : C ⟶ D
h : F = G
⊢ toNatTrans (eqToHom h) = eqToHom ⋯
have refl : toNatTrans (eqToHom sorry) = eqToHom sorry
Tactic: cases h
Cleared hypotheses: G, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
B C : Cat
F : B ⟶ C
⊢ toNatIso (ρ_ F) = eqToIso ⋯ ≪≫ F.toFunctor.rightUnitor ≪≫ eqToIso ⋯
have simp : toNatIso (ρ_ F) = F.toFunctor.rightUnitor
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X : Type u
⊢ toCatHom
      (Discrete.functor
        (Discrete.mk ∘
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) :
            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X))) =
    𝟙 (Cat.of (Discrete X))
have h : Cat.Hom.toFunctor
    (toCatHom
      (Discrete.functor
        (Discrete.mk ∘
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) :
            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X)))) =
  Cat.Hom.toFunctor (𝟙 (Cat.of (Discrete X)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X : Type u
⊢ Cat.Hom.toFunctor
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) X)))) =
    Cat.Hom.toFunctor (𝟙 (Cat.of (Discrete X)))
have h : Eq (α := Discrete X ⥤ Discrete X)
  (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) (𝟭 (Discrete X))
Tactic: simp only [Cat.of_α, toCatHom_toFunctor, Cat.Hom.id_toFunctor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X : Type u
⊢ Eq (α := Discrete X ⥤ Discrete X)
    (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X)))
    (𝟭 (Discrete X))
have h : ∀ (X_1 : Discrete X),
  obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) X_1 =
    obj (𝟭 (Discrete X)) X_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X : Type u
h :
  ∀ (X_1 : Discrete X),
    obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) X_1 =
      obj (𝟭 (Discrete X)) X_1
⊢ Eq (α := Discrete X ⥤ Discrete X)
    (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X)))
    (𝟭 (Discrete X))
have h₁ : autoParam
  (∀ (X_1 Y : Discrete X) (f : X_1 ⟶ Y),
    Eq (α :=
      Quiver.Hom (V := Discrete X)
        (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) X_1)
        (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) Y))
      (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X)) : (a : X) → X))) f)
      (CategoryStruct.comp (Y := obj (𝟭 (Discrete X)) X_1) (eqToHom sorry) (map (𝟭 (Discrete X)) f ≫ eqToHom sorry)))
  ext._auto_1
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X_1 : Type u
X Y : Discrete X_1
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := Discrete X_1)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1))) X)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
        Y))
    (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1))) f)
    (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) X) (eqToHom ⋯) (map (𝟭 (Discrete X_1)) f ≫ eqToHom ⋯))
have h : ∀ (down : PLift (X.as = Y.as)),
  Eq (α :=
    Quiver.Hom (V := Discrete X_1)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1))) X)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
        Y))
    (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
      { down := down })
    (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) X) (eqToHom sorry)
      (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) Y) (map (𝟭 (Discrete X_1)) { down := down }) (eqToHom sorry)))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X_1 : Type u
X Y : Discrete X_1
down : PLift (X.as = Y.as)
⊢ Eq (α :=
    Quiver.Hom (V := Discrete X_1)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1))) X)
      (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
        Y))
    (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
      { down := down })
    (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) X) (eqToHom ⋯)
      (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) Y) (map (𝟭 (Discrete X_1)) { down := down }) (eqToHom ⋯)))
have h : Eq (α :=
  PLift
    (Eq (α := (fun (X : Type u) ↦ X) X_1)
      (Discrete.as
        (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
          X))
      (Discrete.as
        (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
          Y))))
  (ULift.down.{u, 0}
    (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X_1)) : (a : X_1) → X_1)))
      { down := down }))
  (ULift.down.{u, 0}
    (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) X) (eqToHom sorry)
      (CategoryStruct.comp (Y := obj (𝟭 (Discrete X_1)) Y) (map (𝟭 (Discrete X_1)) { down := down }) (eqToHom sorry))))
Tactic: apply ULift.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := Cat.of (Discrete X) ⟶ Cat.of (Discrete Z))
    (toCatHom
      (Discrete.functor
        (Discrete.mk ∘
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) :
            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z))))
    (CategoryStruct.comp (Y := Cat.of (Discrete Y))
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))))
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))))
have h : Eq (α :=
  (↑(Cat.of (Discrete ((fun (X : Type u) ↦ X) X))) : Type u) ⥤
    (↑(Cat.of (Discrete ((fun (X : Type u) ↦ X) Z))) : Type u))
  (Cat.Hom.toFunctor
    (toCatHom
      (Discrete.functor
        (Discrete.mk ∘
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) :
            (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))))
  (Cat.Hom.toFunctor
    (CategoryStruct.comp (Y := Cat.of (Discrete Y))
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))))
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
              (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z))))))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    (↑(Cat.of (Discrete ((fun (X : Type u) ↦ X) X))) : Type u) ⥤
      (↑(Cat.of (Discrete ((fun (X : Type u) ↦ X) Z))) : Type u))
    (Cat.Hom.toFunctor
      (toCatHom
        (Discrete.functor
          (Discrete.mk ∘
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)))))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := Cat.of (Discrete Y))
        (toCatHom
          (Discrete.functor
            (Discrete.mk ∘
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))))
        (toCatHom
          (Discrete.functor
            (Discrete.mk ∘
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) :
                (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z))))))
have h : Eq (α := Discrete X ⥤ Discrete Z)
  (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z)))
  (comp (D := Discrete Y)
    (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
    (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
Tactic: simp only [Cat.of_α, toCatHom_toFunctor, Cat.Hom.comp_toFunctor]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := Discrete X ⥤ Discrete Z)
    (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z)))
    (comp (D := Discrete Y)
      (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
      (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
have h : autoParam
  (∀ (X_1 Y_1 : Discrete X) (f_1 : X_1 ⟶ Y_1),
    Eq (α :=
      Quiver.Hom (V := Discrete Z)
        (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z))) X_1)
        (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z)))
          Y_1))
      (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z))) f_1)
      (CategoryStruct.comp (Y :=
        obj
          (comp (D := Discrete Y)
            (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
            (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
          X_1)
        (eqToHom sorry)
        (map
            (comp (D := Discrete Y)
              (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
              (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
            f_1 ≫
          eqToHom sorry)))
  ext._auto_1
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X Y Z : Type u
f : X ⟶ Y
g : Y ⟶ Z
h :
  autoParam
    (∀ (X_1 Y_1 : Discrete X) (f_1 : X_1 ⟶ Y_1),
      Eq (α :=
        Quiver.Hom (V := Discrete Z)
          (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z)))
            X_1)
          (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z)))
            Y_1))
        (map (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z))) f_1)
        (CategoryStruct.comp (Y :=
          obj
            (comp (D := Discrete Y)
              (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
              (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
            X_1)
          (eqToHom ⋯)
          (map
              (comp (D := Discrete Y)
                (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
                (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
              f_1 ≫
            eqToHom ⋯)))
    ext._auto_1
⊢ Eq (α := Discrete X ⥤ Discrete Z)
    (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z)))
    (comp (D := Discrete Y)
      (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
      (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
have h₁ : ∀ (X_1 : Discrete X),
  Eq (α := Discrete Z)
    (obj (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ g)) : (a : X) → Z))) X_1)
    (obj
      (comp (D := Discrete Y)
        (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : X) → Y)))
        (Discrete.functor (Discrete.mk ∘ (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) g) : (a : Y) → Z))))
      X_1)
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
_X _Y : Type u
_f _g : _X ⟶ _Y
h : typeToCat.map _f = typeToCat.map _g
⊢ _f = _g
have h₁ : ∀ (x : _X),
  (ConcreteCategory.hom (FC := TypeCat.Fun) _f).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) _g).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
⊢ typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk)) = F
have h : (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor = F.toFunctor
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
⊢ (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor = F.toFunctor
have h : ∀ (X_1 Y_1 : (↑(typeToCat.obj X) : Type u)) (f : X_1 ⟶ Y_1),
  (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f =
    eqToHom sorry ≫ F.toFunctor.map f ≫ eqToHom sorry
Tactic: refine Functor.ext (by cat_disch) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Cat (goal)
Goal:
X Y : Type u
F : typeToCat.obj X ⟶ typeToCat.obj Y
x y : (↑(typeToCat.obj X) : Type u)
f : x ⟶ y
⊢ (typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f =
    eqToHom ⋯ ≫ F.toFunctor.map f ≫ eqToHom ⋯
have h : ULift.down.{u, 0} ((typeToCat.map (↾(Discrete.as ∘ F.toFunctor.obj ∘ Discrete.mk))).toFunctor.map f) =
  ULift.down.{u, 0} (eqToHom sorry ≫ F.toFunctor.map f ≫ eqToHom sorry)
Tactic: apply ULift.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Factorisation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
d : Factorisation f_1
f : Factorisation.initial ⟶ d
⊢ f = d.initialHom
have h : f.h = d.initialHom.h
Tactic: apply Factorisation.Hom.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Factorisation (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 : X ⟶ Y
d : Factorisation f_1
f : d ⟶ Factorisation.terminal
⊢ f = d.terminalHom
have h : f.h = d.terminalHom.h
Tactic: apply Factorisation.Hom.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.KleisliCat (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
⊢ Category.{max u v, u + 1} (KleisliCat m)
have refine_1 : ∀ {X Y : KleisliCat m} (f : X ⟶ Y), 𝟙 X ≫ f = f
Tactic: refine { id_comp := ?_, comp_id := ?_, assoc := ?_ }
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.KleisliCat (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
refine_1 : ∀ {X Y : KleisliCat m} (f : X ⟶ Y), 𝟙 X ≫ f = f
⊢ Category.{max u v, u + 1} (KleisliCat m)
have refine_2 : ∀ {X Y : KleisliCat m} (f : X ⟶ Y), f ≫ 𝟙 Y = f
Tactic: refine { id_comp := ?_, comp_id := ?_, assoc := ?_ }
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.KleisliCat (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
refine_1 : ∀ {X Y : KleisliCat m} (f : X ⟶ Y), 𝟙 X ≫ f = f
refine_2 : ∀ {X Y : KleisliCat m} (f : X ⟶ Y), f ≫ 𝟙 Y = f
⊢ Category.{max u v, u + 1} (KleisliCat m)
have refine_3 : ∀ {W X Y Z : KleisliCat m} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
Tactic: refine { id_comp := ?_, comp_id := ?_, assoc := ?_ }
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.KleisliCat (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
X Y : KleisliCat m
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f
have refine_1 : ∀ (x : X), (𝟙 X ≫ f) x = f x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.KleisliCat (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
X Y : KleisliCat m
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f
have refine_2 : ∀ (x : X), (f ≫ 𝟙 Y) x = f x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.KleisliCat (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
W X Y Z : KleisliCat m
f : W ⟶ X
g : X ⟶ Y
h : Y ⟶ Z
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h
have refine_3 : ∀ (x : W), ((f ≫ g) ≫ h) x = (f ≫ g ≫ h) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Pairwise (goal)
Goal:
ι : Type v
α : Type u
U : ι → α
inst : CompleteLattice α
s : Cocone (diagram U)
⊢ Cocone.pt (cocone U) ≤ s.pt
have h : ∀ b ∈ Set.range U, b ≤ s.pt
Tactic: apply sSup_le
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
α β : PartialFun
e : α ≃ β
⊢ (↑(Function.comp (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) : α →. α) = 𝟙 α
have simp : PFun.id α = 𝟙 α
Tactic: simp only [Equiv.symm_comp_self, PFun.coe_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
α β : PartialFun
e : α ≃ β
⊢ (↑(Function.comp (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) : β →. β) = 𝟙 β
have simp : PFun.id β = 𝟙 β
Tactic: simp only [Equiv.self_comp_symm, PFun.coe_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y : Type u_1
a₁ a₂ : X ⟶ Y
h : typeToPartialFun.map a₁ = typeToPartialFun.map a₂
⊢ a₁ = a₂
have h₁ : ∀ (x : X), (ConcreteCategory.hom (FC := TypeCat.Fun) a₁).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) a₂).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := PartialFun.of { x : X.X // x ≠ X.point } ⟶ PartialFun.of { x : Z.X // x ≠ Z.point })
    (PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) (f ≫ g).toFun ∘ Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
    (CategoryStruct.comp (Y := PartialFun.of { x : Y.X // x ≠ Y.point })
      (PFun.toSubtype (fun (x : Y.X) ↦ x ≠ Y.point) f.toFun ∘ Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
      (PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) g.toFun ∘ Subtype.val (p := fun (x : Y.X) ↦ x ≠ Y.point)))
have refine : ∀ (x : PartialFun.of { x : X.X // x ≠ X.point }) (x : PartialFun.of { x : Z.X // x ≠ Z.point }) (a : X.X)
  (ha : a ≠ X.point) (c : Z.X) (hc : c ≠ Z.point),
  (↑(Subtype.mk (p := fun (x : Z.X) ↦ x ≠ Z.point) c hc) : Z.X) =
      (f ≫ g).toFun (↑(Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha) : X.X) ↔
    ∃ (a_1 : PartialFun.of { x : Y.X // x ≠ Y.point }),
      Membership.mem (γ := Part (PartialFun.of { x : Y.X // x ≠ Y.point }))
          (Function.comp (α := PartialFun.of { x : X.X // x ≠ X.point })
            (PFun.toSubtype (fun (x : Y.X) ↦ x ≠ Y.point) f.toFun) (Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
            (Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha))
          a_1 ∧
        Membership.mem (γ := Part (PartialFun.of { x : Z.X // x ≠ Z.point }))
          ((PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) g.toFun ∘ Subtype.val (p := fun (x : Y.X) ↦ x ≠ Y.point)) a_1)
          (Subtype.mk (p := fun (x : Z.X) ↦ x ≠ Z.point) c hc)
Tactic: refine PFun.ext fun ⟨a, ha⟩ ⟨c, hc⟩ =>
      (PFun.mem_toSubtype_iff.trans ?_).trans Part.mem_bind_iff.symm