awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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
hi : IsMin.{u} (α := J) ⊥
e₁ e₂ : d.Extension val₀ ⊥
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op ⊥))) → (fun (X : Type v) ↦ X) (F.obj (op ⊥)))
      e₁.val =
    val₀
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op ⊥))) → (fun (X : Type v) ↦ X) (F.obj (op ⊥)))
      e₂.val =
    val₀
h₃ : e₁.val = val₀
⊢ e₂.val = val₀

Tactic:
simp only [homOfLE_refl, op_id, map_id, id_apply] at h₁ h₂

Premises used: CategoryTheory.homOfLE_refl, CategoryTheory.id_apply, CategoryTheory.Functor.map_id, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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
hi : IsMin.{u} (α := J) ⊥
e₁ e₂ : d.Extension val₀ ⊥
h₁ : e₁.val = val₀
h₂ : e₂.val = val₀
isMin : val₀ = e₂.val
isMin₁ isMin₂ : val₀ = val₀
⊢ e₁.val = e₂.val

Tactic:
rw [h₁, h₂]
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)
⊢ Subsingleton.{v + 1} (d.Extension val₀ (Order.succ i))

Tactic:
Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.val_injective, Subsingleton.intro
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)
succ : ∀ (e₁ e₂ : d.Extension val₀ (Order.succ i)), e₁.val = e₂.val
⊢ Subsingleton.{v + 1} (d.Extension val₀ (Order.succ i))

Tactic:
refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.val_injective, Subsingleton.intro
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)
⊢ (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)

Tactic:
have h₁ := e₁.map_succ i (Order.lt_succ_of_not_isMax hi)
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)
⊢ (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)

Tactic:
have h₂ := e₂.map_succ i (Order.lt_succ_of_not_isMax hi)
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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 =
    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)

Tactic:
simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom] at h₁ h₂

Premises used: CategoryTheory.homOfLE_refl, CategoryTheory.homOfLE_leOfHom, CategoryTheory.id_apply, CategoryTheory.Functor.map_id, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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 =
    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)

Tactic:
simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom] at h₁ h₂

Premises used: CategoryTheory.homOfLE_refl, CategoryTheory.homOfLE_leOfHom, CategoryTheory.id_apply, CategoryTheory.Functor.map_id, CategoryTheory.op_id
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)
succ :
  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)
⊢ e₁.val = e₂.val

Tactic:
rw [h₁, h₂]
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)
succ :
  Eq (α := F.obj (op 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 :
      F.obj (op 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 :
      F.obj (op i))
⊢ 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)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)
⊢ Eq (α := F.obj (op 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 :
      F.obj (op 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 :
      F.obj (op i))

Tactic:
congrArg val (Subsingleton.elim (e₁.ofLE (Order.le_succ i)) (e₂.ofLE (Order.le_succ i)))

Premises used: congrArg, CategoryTheory.Functor.WellOrderInductionData.Extension.val, CategoryTheory.Functor.WellOrderInductionData.Extension.ofLE, Order.le_succ, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)
⊢ Eq (α := F.obj (op 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 :
      F.obj (op 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 :
      F.obj (op i))

Tactic:
exact congrArg val (Subsingleton.elim (e₁.ofLE (Order.le_succ i)) (e₂.ofLE (Order.le_succ i)))

Premises used: congrArg, CategoryTheory.Functor.WellOrderInductionData.Extension.val, CategoryTheory.Functor.WellOrderInductionData.Extension.ofLE, Order.le_succ, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)

Tactic:
Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.val_injective, Subsingleton.intro
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)
isSuccLimit : ∀ (e₁ e₂ : d.Extension val₀ i), e₁.val = e₂.val
⊢ Subsingleton.{v + 1} (d.Extension val₀ i)

Tactic:
refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.val_injective, Subsingleton.intro
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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
⊢ i ≤ i

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (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)) ⋯) ⋙
                  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 i))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
              e₁.val)
        ⋯)

Tactic:
have h₁ := e₁.map_limit i hi (by rfl)
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (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)) ⋯) ⋙
                  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 i))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
              e₁.val)
        ⋯)
⊢ i ≤ i

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
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)
        ⋯)
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)) ⋯) ⋙ 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)
        ⋯)
⊢ e₁.val = e₂.val

Tactic:
rw [h₁, h₂]