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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij_1).op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
      (d.succ j hj 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)) ⋯) ⋙
                  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)) ⋯) ⋙
                  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)) ⋯) ⋙
              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)) ⋯) ⋙
                  F)
                x)
            x with
          | op ⟨k, hk⟩ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
                (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
              (d.succ j hj e.val))
        ⋯)
have this : Eq (α := (fun (X : Type v) ↦ X) (F.obj (op i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij').op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
            (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → (fun (X : Type v) ↦ X) (F.obj (op j)))
          (d.succ j hj e.val) :
        (fun (X : Type v) ↦ X) (F.obj (op j))) :
    (fun (X : Type v) ↦ X) (F.obj (op i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij').op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
      e.val :
    (fun (X : Type v) ↦ X) (F.obj (op i)))
Tactic: have := congr_arg (F.map (homOfLE hij').op) (d.map_succ j hj e.val)
-- 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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → F.obj (op i))
      (d.succ j hj 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)) ⋯) ⋙
                  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)) ⋯) ⋙
                  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)) ⋯) ⋙
              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)) ⋯) ⋙
                  F)
                x)
            x with
          | op ⟨k, hk⟩ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
                (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
              e.val)
        ⋯)
l : J
hl : l ∈ Set.Iio i
| ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) : (a : F.obj (op j)) → F.obj (op l)) e.val :
    F.obj (op l))
have rw : ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) : (a : F.obj (op j)) → F.obj (op l))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → (fun (X : Type v) ↦ X) (F.obj (op j)))
        (d.succ j hj e.val) :
      (fun (X : Type v) ↦ X) (F.obj (op j))) :
  F.obj (op l))
Tactic: rw [← d.map_succ j hj e.val]
-- 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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ Order.succ j
hij : i < Order.succ j
hij' : i ≤ j
this :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → F.obj (op i))
      (d.succ j hj 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)) ⋯) ⋙
                  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)) ⋯) ⋙
                  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)) ⋯) ⋙
              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)) ⋯) ⋙
                  F)
                x)
            x with
          | op ⟨k, hk⟩ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
                (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
              e.val)
        ⋯)
l : J
hl : l ∈ Set.Iio i
⊢ Eq (α := F.obj (op l))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) : (a : F.obj (op j)) → F.obj (op l)) e.val :
      F.obj (op l))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) : (a : F.obj (op (Order.succ j))) → F.obj (op l))
        (d.succ j hj e.val) :
      F.obj (op l))
have inl : Eq (α := F.obj (op l))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) : (a : F.obj (op j)) → F.obj (op l))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
            (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → (fun (X : Type v) ↦ X) (F.obj (op j)))
          (d.succ j hj e.val) :
        (fun (X : Type v) ↦ X) (F.obj (op j))) :
    F.obj (op l))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) : (a : F.obj (op (Order.succ j))) → F.obj (op l))
      (d.succ j hj e.val) :
    F.obj (op l))
Tactic: conv_lhs => rw [← d.map_succ j hj e.val]
-- 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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
hi : Order.IsSuccLimit (Order.succ j)
hij : Order.succ j ≤ Order.succ j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j))))
      (d.succ j hj e.val) =
    d.lift (Order.succ j) hi
      (Subtype.mk (p :=
        fun
          (x :
            (j_1 : { x : J // x ∈ Set.Iio (Order.succ j) }ᵒᵖ) →
              obj
                (Functor.op
                    (Monotone.functor (f :=
                      (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio (Order.succ j)) :
                        (a : { x : J // x ∈ Set.Iio (Order.succ j) }) → J))
                      ⋯) ⋙
                  F)
                j_1) ↦
        Membership.mem (γ :=
          Set
            ((j_1 : { x : J // x ∈ Set.Iio (Order.succ j) }ᵒᵖ) →
              obj
                (Functor.op
                    (Monotone.functor (f :=
                      (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio (Order.succ j)) :
                        (a : { x : J // x ∈ Set.Iio (Order.succ j) }) → J))
                      ⋯) ⋙
                  F)
                j_1))
          (sections
            (Functor.op
                (Monotone.functor (f :=
                  (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio (Order.succ j)) :
                    (a : { x : J // x ∈ Set.Iio (Order.succ j) }) → J))
                  ⋯) ⋙
              F))
          x)
        (fun (x : { x : J // x ∈ Set.Iio (Order.succ j) }ᵒᵖ) ↦
          match (motive :=
            (x : { x : J // x ∈ Set.Iio (Order.succ j) }ᵒᵖ) →
              obj
                (Functor.op
                    (Monotone.functor (f :=
                      (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio (Order.succ j)) :
                        (a : { x : J // x ∈ Set.Iio (Order.succ j) }) → J))
                      ⋯) ⋙
                  F)
                x)
            x with
          | op ⟨k, hk⟩ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
                (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
              (d.succ j hj e.val))
        ⋯)
have inr : False
Tactic: exfalso
-- 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
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ i < Order.succ i
have simp : ∃ (b : J), i < b
Tactic: simp only [Order.lt_succ_iff_not_isMax, not_isMax_iff]
-- 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
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ Eq (α := F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op j)) → F.obj (op (Order.succ i)))
        (d.lift j hj
          (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
            Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)) :
      F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 (op (Order.succ i)))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op (Order.succ i)))
        (val (e (Order.succ i) ⋯)) :
      F.obj (op (Order.succ i)))
have h : Eq (α := F.obj (op (Order.succ i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op j)) → F.obj (op (Order.succ i)))
      (d.lift j hj
        (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
          Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
            (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) sorry) ⋙ F)) x)
          (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) sorry)) sorry)) :
    F.obj (op (Order.succ i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj (op (Order.succ i)))) :
        (a : F.obj (op (Order.succ i))) → F.obj (op (Order.succ i)))
      (val (e (Order.succ i) sorry)) :
    F.obj (op (Order.succ i)))
Tactic: rw [map_id, id_apply, d.map_lift _ _ _ _ ((Order.IsSuccLimit.succ_lt_iff hj).mpr 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
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
h :
  Eq (α := F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op j)) → F.obj (op (Order.succ i)))
        (d.lift j hj
          (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
            Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)) :
      F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj (op (Order.succ i)))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op (Order.succ i)))
        (val (e (Order.succ i) ⋯)) :
      F.obj (op (Order.succ i)))
⊢ Eq (α := F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op j)) → F.obj (op (Order.succ i)))
        (d.lift j hj
          (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
            Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)) :
      F.obj (op (Order.succ i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 (op (Order.succ i)))) :
          (a : F.obj (op (Order.succ i))) → F.obj (op (Order.succ i)))
        (val (e (Order.succ i) ⋯)) :
      F.obj (op (Order.succ i)))
have h₁ : Eq (α := F.obj (op (Order.succ i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op j)) → F.obj (op (Order.succ i)))
      (d.lift j hj
        (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
          Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
            (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) sorry) ⋙ F)) x)
          (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) sorry)) sorry)) :
    F.obj (op (Order.succ i)))
  (val (e (Order.succ i) sorry) : F.obj (op (Order.succ i)))
Tactic: rw [map_id, id_apply, d.map_lift _ _ _ _ ((Order.IsSuccLimit.succ_lt_iff hj).mpr 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
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
hij' : i < j
this :
  (e i hij').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 i hij').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 i hij').val)
    fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : F.obj (op j)) → F.obj (op (↑x.1 : J)))
      (d.lift j hj
        (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
          Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
            (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) ⋙ F)) x)
          (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯))
have inl : ∀ (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 i hij').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 j)) → F.obj (op (↑(op ⟨l, hl⟩).1 : J)))
        (d.lift j hj
          (Subtype.mk (p := fun (x : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))) ↦
            Membership.mem (γ := Set ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → F.obj (op (↑(unop j_1) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) sorry) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) sorry)) sorry)) :
      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 (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
⊢ 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) ⋯)) ⋯) =
    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)))
            (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 (α := (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) sorry)) 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)))
    (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: congr