awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (goal)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
i : J
hi hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
⊢ Eq (α := (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J)))
    (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
      (d.lift i hj
        (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
          Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
            (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F)) x)
          (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯))
have inr : ∀ (l : J) (hl : l ∈ Set.Iio i),
  Eq (α := F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
    (val (e (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J) sorry))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op i)) → F.obj (op (↑(op ⟨l, hl⟩).1 : J)))
      (d.lift i hj
        (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
          Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
            (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) sorry) ⋙ F)) x)
          (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) sorry)) sorry)))
Tactic: ext ⟨⟨l, hl⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (goal)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
i : J
hi hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
l : J
hl : l ∈ Set.Iio i
⊢ Eq (α := F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
    (val (e (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J) ⋯))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : F.obj (op i)) → F.obj (op (↑(op ⟨l, hl⟩).1 : J)))
      (d.lift i hj
        (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
          Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
            (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F)) x)
          (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)))
have inr : Eq (α := F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
  (val (e (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J) sorry))
  ((↑(Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
          Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
            (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) sorry) ⋙ F)) x)
          (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) sorry)) sorry) :
      (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → (sorry.functor.op ⋙ F).obj j)
    (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)))
Tactic: rw [d.map_lift _ _ _ _ hl]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (goal)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
i : J
hi : IsMin i
⊢ Nonempty.{v + 1} (d.Extension val₀ i)
have isMin : ∀ (hi : IsMin.{u} (α := J) ⊥), Nonempty.{v + 1} (d.Extension val₀ ⊥)
Tactic: obtain rfl : i = ⊥ := by simpa using hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (goal)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
j : J
⊢ Nonempty.{v + 1} (d.Extension val₀ j)
have isMin : ∀ (i : J) (hi : IsMin i), Nonempty.{v + 1} (d.Extension val₀ i)
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin i hi =>
    obtain rfl : i = ⊥ := by simpa using hi
    exact ⟨zero d val₀⟩
  | succ i hi hi' => exact ⟨hi'.some.succ hi⟩
  | isSuccLimit i hi hi' => exact ⟨limit i hi (fun l hl ↦ (hi' l hl).some)⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (goal)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
j : J
isMin : ∀ (i : J) (hi : IsMin i), Nonempty.{v + 1} (d.Extension val₀ i)
⊢ Nonempty.{v + 1} (d.Extension val₀ j)
have succ : ∀ (i : J) (hi : ¬IsMax i) (hi' : Nonempty.{v + 1} (d.Extension val₀ i)),
  Nonempty.{v + 1} (d.Extension val₀ (Order.succ i))
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin i hi =>
    obtain rfl : i = ⊥ := by simpa using hi
    exact ⟨zero d val₀⟩
  | succ i hi hi' => exact ⟨hi'.some.succ hi⟩
  | isSuccLimit i hi hi' => exact ⟨limit i hi (fun l hl ↦ (hi' l hl).some)⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (goal)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
j : J
isMin : ∀ (i : J) (hi : IsMin i), Nonempty.{v + 1} (d.Extension val₀ i)
succ :
  ∀ (i : J) (hi : ¬IsMax i) (hi' : Nonempty.{v + 1} (d.Extension val₀ i)),
    Nonempty.{v + 1} (d.Extension val₀ (Order.succ i))
⊢ Nonempty.{v + 1} (d.Extension val₀ j)
have isSuccLimit : ∀ (i : J) (hi : Order.IsSuccLimit i) (hi' : ∀ b < i, Nonempty.{v + 1} (d.Extension val₀ b)),
  Nonempty.{v + 1} (d.Extension val₀ i)
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin i hi =>
    obtain rfl : i = ⊥ := by simpa using hi
    exact ⟨zero d val₀⟩
  | succ i hi hi' => exact ⟨hi'.some.succ hi⟩
  | isSuccLimit i hi hi' => exact ⟨limit i hi (fun l hl ↦ (hi' l hl).some)⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x : (↑h.smallCategoryOfSet.obj : Type w)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
    (((h.homEquiv :
            Equiv.{w + 1, v + 1} (↑(h.hom x x) : Type w)
              (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
                ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))) :
          (a : (↑(h.hom x x) : Type w)) →
            (h.objEquiv : (a : (↑h.obj : Type w)) → C) x ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) x)
        (𝟙 x) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
    (𝟙 ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
have rw : Eq.{v + 1} (α :=
  Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
    ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
  (((h.homEquiv :
          Equiv.{w + 1, v + 1} (↑(h.hom x x) : Type w)
            (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
              ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))) :
        (a : (↑(h.hom x x) : Type w)) →
          (h.objEquiv : (a : (↑h.obj : Type w)) → C) x ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) x)
      (h.smallCategoryOfSet.id x) :
    Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
  (𝟙 ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) :
    Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
Tactic: rw [SmallCategoryOfSet.id_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
Y : C
⊢ h.functor.essImage Y
have obtain : ∀ (X : (↑h.obj : Type w)), h.functor.essImage ((h.objEquiv : (a : (↑h.obj : Type w)) → C) X)
Tactic: obtain ⟨X, rfl⟩ := h.objEquiv.surjective Y
Cleared hypotheses: Y
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
⊢ Function.Bijective h.functor.mapArrow.obj
have left : Function.Injective h.functor.mapArrow.obj
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
left : Function.Injective h.functor.mapArrow.obj
⊢ Function.Bijective h.functor.mapArrow.obj
have right : Function.Surjective h.functor.mapArrow.obj
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.smallCategoryOfSet.obj : Type w)
f : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y
x' y' : (↑h.smallCategoryOfSet.obj : Type w)
g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x' ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y'
hfg :
  h.functor.mapArrow.obj
      { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    h.functor.mapArrow.obj { left := x', right := y', hom := g }
⊢ { left := x, right := y, hom := f :
      Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
        (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    { left := x', right := y', hom := g }
have left : ∀ (g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y')
  (hfg :
    h.functor.mapArrow.obj
        { left := x, right := y, hom := f :
          Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
            (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
      h.functor.mapArrow.obj { left := x, right := y', hom := g }),
  { left := x, right := y, hom := f :
      Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
        (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    { left := x, right := y', hom := g }
Tactic: obtain rfl : x = x' := by simpa using congr_arg Arrow.leftFunc.obj hfg
Cleared hypotheses: x', g, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.smallCategoryOfSet.obj : Type w)
f : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y
y' : (↑h.smallCategoryOfSet.obj : Type w)
g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y'
hfg :
  h.functor.mapArrow.obj
      { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    h.functor.mapArrow.obj { left := x, right := y', hom := g }
⊢ { left := x, right := y, hom := f :
      Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
        (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    { left := x, right := y', hom := g }
have left : ∀ (g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y)
  (hfg :
    h.functor.mapArrow.obj
        { left := x, right := y, hom := f :
          Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
            (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
      h.functor.mapArrow.obj { left := x, right := y, hom := g }),
  { left := x, right := y, hom := f :
      Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
        (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    { left := x, right := y, hom := g }
Tactic: obtain rfl : y = y' := by simpa using congr_arg Arrow.rightFunc.obj hfg
Cleared hypotheses: y', g, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.smallCategoryOfSet.obj : Type w)
f g : Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) x ⟶ Functor.obj (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) y
hfg :
  h.functor.mapArrow.obj
      { left := x, right := y, hom := f :
        Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
          (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    h.functor.mapArrow.obj { left := x, right := y, hom := g }
⊢ { left := x, right := y, hom := f :
      Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
        (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    { left := x, right := y, hom := g }
have left : ∀
  (hfg :
    h.functor.mapArrow.obj
        { left := x, right := y, hom := f :
          Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
            (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
      h.functor.mapArrow.obj { left := x, right := y, hom := f }),
  { left := x, right := y, hom := f :
      Comma (A := (↑h.smallCategoryOfSet.obj : Type w)) (𝟭 (↑h.smallCategoryOfSet.obj : Type w))
        (𝟭 (↑h.smallCategoryOfSet.obj : Type w)) } =
    { left := x, right := y, hom := f }
Tactic: obtain rfl : f = g := by simpa [Arrow.mk_eq_mk_iff] using hfg
Cleared hypotheses: g, hfg
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
X Y : C
f : Functor.obj.{v, v, u, u} (𝟭 C) X ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y
⊢ ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)), h.functor.mapArrow.obj a = { left := X, right := Y, hom := f }
have right : ∀ (x : (↑h.obj : Type w))
  (f :
    Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y),
  ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
    h.functor.mapArrow.obj a = { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := Y, hom := f }
Tactic: obtain ⟨x, rfl⟩ := h.objEquiv.surjective X
Cleared hypotheses: X, f
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
Y : C
x : (↑h.obj : Type w)
f : Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y
⊢ ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
    h.functor.mapArrow.obj a = { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := Y, hom := f }
have right : ∀ (y : (↑h.obj : Type w))
  (f :
    Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) ⟶
      Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) y)),
  ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
    h.functor.mapArrow.obj a =
      { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := (h.objEquiv : (a : (↑h.obj : Type w)) → C) y,
        hom := f }
Tactic: obtain ⟨y, rfl⟩ := h.objEquiv.surjective Y
Cleared hypotheses: Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x y : (↑h.obj : Type w)
f :
  Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) ⟶
    Functor.obj.{v, v, u, u} (𝟭 C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) y)
⊢ ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
    h.functor.mapArrow.obj a =
      { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := (h.objEquiv : (a : (↑h.obj : Type w)) → C) y,
        hom := f }
have right : ∀ (f : (↑(h.hom x y) : Type w)),
  ∃ (a : Arrow (↑h.smallCategoryOfSet.obj : Type w)),
    h.functor.mapArrow.obj a =
      { left := (h.objEquiv : (a : (↑h.obj : Type w)) → C) x, right := (h.objEquiv : (a : (↑h.obj : Type w)) → C) y,
        hom :=
          ((h.homEquiv :
                Equiv.{w + 1, v + 1} (↑(h.hom x y) : Type w)
                  (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
                    ((h.objEquiv : (a : (↑h.obj : Type w)) → C) y : C))) :
              (a : (↑(h.hom x y) : Type w)) →
                (h.objEquiv : (a : (↑h.obj : Type w)) → C) x ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) y)
            f }
Tactic: obtain ⟨f, rfl⟩ := h.homEquiv.surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
⊢ Nonempty (Arrow.{v, u} C ↪ Ω)
have rw : Cardinal.lift.{w, max u v} (Cardinal.mk (Arrow.{v, u} C)) ≤ Cardinal.lift.{max u v, w} (Cardinal.mk Ω)
Tactic: rw [← Cardinal.lift_mk_le']
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
⊢ ∃ (S : SmallCategoryCardinalLT κ), Nonempty (Equivalence.{w, v, w, u} (categoryFamily κ S) C)
have have : ∀ (ι : Arrow.{v, u} C ↪ Ω),
  ∃ (S : SmallCategoryCardinalLT κ), Nonempty (Equivalence.{w, v, w, u} (categoryFamily κ S) C)
Tactic: have ι : Arrow C ↪ Ω := Nonempty.some (by
    rw [← Cardinal.lift_mk_le']
    simpa [Ω] using hC.le)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
⊢ Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
have rw : Nonempty (C ↪ Ω)
Tactic: rw [Cardinal.lift_mk_le']
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
⊢ Nonempty (C ↪ Ω)
have refine : Function.Injective (β := Arrow.{v, u} C) fun (X : C) ↦ Arrow.mk (𝟙 X)
Tactic: refine ⟨Function.Embedding.trans { toFun X := Arrow.mk (𝟙 X), inj' := ?_ } ι⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (hypothesis)
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
⊢ ∃ (S : SmallCategoryCardinalLT κ), Nonempty (Equivalence.{w, v, w, u} (categoryFamily κ S) C)
have h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
Tactic: have h₁ : Cardinal.lift.{w} (Cardinal.mk C) ≤
      Cardinal.lift.{u} (Cardinal.mk Ω) := by
    rw [Cardinal.lift_mk_le']
    refine ⟨Function.Embedding.trans { toFun X := Arrow.mk (𝟙 X), inj' := ?_ } ι⟩
    intro X Y h
    exact congr_arg Arrow.leftFunc.obj h
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
X Y : C
⊢ Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
have rw : Nonempty (Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω)
Tactic: rw [Cardinal.lift_mk_le']
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (goal)
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
X Y : C
⊢ Nonempty (Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω)
have refine : Function.Injective (β := Arrow.{v, u} C) fun (f : X ⟶ Y) ↦ Arrow.mk f
Tactic: refine ⟨Function.Embedding.trans { toFun f := Arrow.mk f, inj' := ?_ } ι⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallRepresentatives (hypothesis)
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
⊢ ∃ (S : SmallCategoryCardinalLT κ), Nonempty (Equivalence.{w, v, w, u} (categoryFamily κ S) C)
have h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
Tactic: have h₂ (X Y : C) : Cardinal.lift.{w} (Cardinal.mk (X ⟶ Y)) ≤
      Cardinal.lift.{v} (Cardinal.mk Ω) := by
    rw [Cardinal.lift_mk_le']
    refine ⟨Function.Embedding.trans { toFun f := Arrow.mk f, inj' := ?_ } ι⟩
    intro f g h
    simpa [Arrow.mk_eq_mk_iff] using h