awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (hypothesis)
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 : ¬IsMax i
hi' : Subsingleton.{v + 1} (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
      e₁.val =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
        e₁.val)
⊢ e₁.val = e₂.val
have h₂ : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
      (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
    e₂.val =
  d.succ i sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
      e₂.val)
Tactic: have h₂ := e₂.map_succ i (Order.lt_succ_of_not_isMax hi)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (hypothesis)
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 : ¬IsMax i
hi' : Subsingleton.{v + 1} (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
      e₁.val =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
        e₁.val)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
      e₂.val =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
        e₂.val)
⊢ e₁.val = e₂.val
have h₃ : e₁.val =
  d.succ i sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op (Order.succ i))) → F.obj (op i))
      e₁.val)
Tactic: simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (hypothesis)
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 : ¬IsMax i
hi' : Subsingleton.{v + 1} (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
      e₁.val =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
        e₁.val)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
      e₂.val =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
        e₂.val)
h₃ :
  e₁.val =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op i))
        e₁.val)
⊢ e₁.val = e₂.val
have h₄ : e₂.val =
  d.succ i sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op (Order.succ i))) → F.obj (op i))
      e₂.val)
Tactic: simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- 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 : ¬IsMax i
hi' : Subsingleton.{v + 1} (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ :
  e₁.val =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op i))
        e₁.val)
h₂ :
  e₂.val =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op i))
        e₂.val)
⊢ e₁.val = e₂.val
have succ : d.succ i sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op (Order.succ i))) → F.obj (op i))
      e₁.val) =
  d.succ i sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op (Order.succ i))) → F.obj (op i))
      e₂.val)
Tactic: rw [h₁, h₂]
-- 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 : ¬IsMax i
hi' : Subsingleton.{v + 1} (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
h₁ :
  e₁.val =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op i))
        e₁.val)
h₂ :
  e₂.val =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op i))
        e₂.val)
⊢ d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op i))
        e₁.val) =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op i))
        e₂.val)
have succ : Eq (α := F.obj (op i))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op (Order.succ i))) → F.obj (op i))
      e₁.val :
    F.obj (op i))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op (Order.succ i))) → F.obj (op i))
      e₂.val :
    F.obj (op i))
Tactic: congr 1
-- 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 : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton.{v + 1} (d.Extension val₀ b)
⊢ Subsingleton.{v + 1} (d.Extension val₀ i)
have isSuccLimit : ∀ (e₁ e₂ : d.Extension val₀ i), e₁.val = e₂.val
Tactic: refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (hypothesis)
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 : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton.{v + 1} (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
⊢ e₁.val = e₂.val
have h₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
      (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
    e₁.val =
  d.lift i hi
    (Subtype.mk (p :=
      fun
        (x :
          (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) →
            obj
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio i) : (a : { x : J // x ∈ Set.Iio i }) → J)) sorry) ⋙
                F)
              j) ↦
      Membership.mem (γ :=
        Set
          ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) →
            obj
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio i) : (a : { x : J // x ∈ Set.Iio i }) → J)) sorry) ⋙
                F)
              j))
        (sections
          (Functor.op
              (Monotone.functor (f :=
                (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio i) : (a : { x : J // x ∈ Set.Iio i }) → J)) sorry) ⋙
            F))
        x)
      (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦
        match (motive :=
          (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) →
            obj
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio i) : (a : { x : J // x ∈ Set.Iio i }) → J)) sorry) ⋙
                F)
              x)
          x with
        | op ⟨k, hk⟩ =>
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
            e₁.val)
      sorry)
Tactic: have h₁ := e₁.map_limit i hi (by rfl)
-- 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 : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton.{v + 1} (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ :
  e₁.val =
    d.lift i hi
      (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 }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            e₁.val)
        ⋯)
h₂ :
  e₂.val =
    d.lift i hi
      (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 }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            e₂.val)
        ⋯)
⊢ e₁.val = e₂.val
have isSuccLimit : d.lift i hi
    (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 }ᵒᵖ) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
            (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
          e₁.val)
      sorry) =
  d.lift i hi
    (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 }ᵒᵖ) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
            (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
          e₂.val)
      sorry)
Tactic: rw [h₁, h₂]
-- 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 : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton.{v + 1} (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ :
  e₁.val =
    d.lift i hi
      (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 }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            e₁.val)
        ⋯)
h₂ :
  e₂.val =
    d.lift i hi
      (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 }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            e₂.val)
        ⋯)
⊢ d.lift i hi
      (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 }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            e₁.val)
        ⋯) =
    d.lift i hi
      (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 }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            e₂.val)
        ⋯)
have isSuccLimit : Eq (α := (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J)))
  (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
      e₁.val)
  fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
      (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
    e₂.val
Tactic: congr
-- 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 : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton.{v + 1} (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ :
  e₁.val =
    d.lift i hi
      (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 }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            e₁.val)
        ⋯)
h₂ :
  e₂.val =
    d.lift i hi
      (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 }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            e₂.val)
        ⋯)
⊢ Eq (α := (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : 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)))
        e₁.val)
    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)))
      e₂.val
have isSuccLimit : ∀ (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)))
    ((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)))
        e₁.val :
      F.obj (op (↑(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 sorry))) :
          (a : F.obj (op i)) → F.obj (op (↑(op ⟨l, hl⟩).1 : J)))
        e₂.val :
      F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
Tactic: ext ⟨⟨l, hl⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (hypothesis)
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 : Order.IsSuccLimit i
hi' : ∀ b < i, Subsingleton.{v + 1} (d.Extension val₀ b)
e₁ e₂ : d.Extension val₀ i
h₁ :
  e₁.val =
    d.lift i hi
      (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 }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            e₁.val)
        ⋯)
h₂ :
  e₂.val =
    d.lift i hi
      (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 }ᵒᵖ) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
            e₂.val)
        ⋯)
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)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op i)) → F.obj (op (↑(op ⟨l, hl⟩).1 : J)))
        e₁.val :
      F.obj (op (↑(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)))
        e₂.val :
      F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
have this : Subsingleton.{v + 1} (d.Extension val₀ l)
Tactic: have := hi' 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
j : J
⊢ Subsingleton.{v + 1} (d.Extension val₀ j)
have isMin : ∀ (i : J) (hi : IsMin i), Subsingleton.{v + 1} (d.Extension val₀ i)
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin i hi =>
    obtain rfl : i = ⊥ := by simpa using hi
    refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
    have h₁ := e₁.map_zero
    have h₂ := e₂.map_zero
    simp only [homOfLE_refl, op_id, map_id, id_apply] at h₁ h₂
    rw [h₁, h₂]
  | succ i hi hi' =>
    refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
    have h₁ := e₁.map_succ i (Order.lt_succ_of_not_isMax hi)
    have h₂ := e₂.map_succ i (Order.lt_succ_of_not_isMax hi)
    simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom] at h₁ h₂
    rw [h₁, h₂]
    congr 1
    exact congrArg val (Subsingleton.elim (e₁.ofLE (Order.le_succ i)) (e₂.ofLE (Order.le_succ i)))
  | isSuccLimit i hi hi' =>
    refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
    have h₁ := e₁.map_limit i hi (by rfl)
    have h₂ := e₂.map_limit i hi (by rfl)
    simp only [homOfLE_refl, op_id, map_id, id_apply, OrderHom.Subtype.val_coe, comp_obj, op_obj,
      Monotone.functor_obj, homOfLE_leOfHom] at h₁ h₂
    rw [h₁, h₂]
    congr
    ext ⟨⟨l, hl⟩⟩
    have := hi' l hl
    exact congr_arg val (Subsingleton.elim (e₁.ofLE hl.le) (e₂.ofLE hl.le))
Cleared hypotheses: j