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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
i : J
hi : i < Order.succ j
inl :
  ∀ (hij : i < j),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
        (d.succ j hj e.val) =
      d.succ i ⋯
        ((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 i)))
          (d.succ j hj e.val))
inr :
  ∀ (e : d.Extension val₀ i) (hj : ¬IsMax i) (hi : i < 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))))
        (d.succ i hj e.val) =
      d.succ i ⋯
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
            (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
          (d.succ i hj e.val))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
      (d.succ j hj e.val) =
    d.succ i ⋯
      ((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 i)))
        (d.succ j hj e.val))

Tactic:
obtain hij | rfl := ((Order.lt_succ_iff_of_not_isMax hj).mp hi).lt_or_eq

Premises used: LE.le.lt_or_eq, Iff.mp, Order.lt_succ_iff_of_not_isMax, 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 ⊥)
i : J
e : d.Extension val₀ i
hj : ¬IsMax i
hi : i < 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))))
      (d.succ i hj e.val) =
    d.succ i ⋯
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
        (d.succ i hj e.val))

Tactic:
simp only [homOfLE_refl, op_id, map_id, id_apply, homOfLE_leOfHom, d.map_succ]

Premises used: CategoryTheory.Functor.WellOrderInductionData.map_succ, 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 ⊥)
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
⊢ i ≤ j

Tactic:
have hij' : i ≤ j := (Order.lt_succ_iff_of_not_isMax hj).mp hij
-- 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 ⊥)
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
⊢ 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 ⋯))) :
              (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)
-- 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 ⊥)
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
rw :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE ⋯).op) : (a : F.obj (op j)) → F.obj (op l))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
            (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 ⋯).op) : (a : F.obj (op j)) → F.obj (op l)) e.val :
    F.obj (op l))

Tactic:
rw [← d.map_succ j hj e.val]

Premises used: CategoryTheory.Functor.WellOrderInductionData.map_succ, CategoryTheory.Functor.WellOrderInductionData.Extension.val
-- 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 ⊥)
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 (Quiver.Hom.op (homOfLE ⋯) ≫ (homOfLE ⋯).op)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ j)))) → F.obj (op l))
        (d.succ j hj 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))

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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
hi : Order.IsSuccLimit (Order.succ j)
hij : Order.succ j ≤ Order.succ j
inr : False
⊢ (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))
        ⋯)

Tactic:
exfalso
-- 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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
hi : Order.IsSuccLimit (Order.succ j)
hij : Order.succ j ≤ Order.succ j
⊢ False

Tactic:
hj hi.isMax

Premises used: Order.IsSuccLimit.isMax
-- 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 ⊥)
j : J
e : d.Extension val₀ j
hj : ¬IsMax j
hi : Order.IsSuccLimit (Order.succ j)
hij : Order.succ j ≤ Order.succ j
⊢ False

Tactic:
exact hj hi.isMax

Premises used: Order.IsSuccLimit.isMax
-- 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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
j_1 j' : { x : J // x ∈ Set.Iio j }ᵒᵖ
f : j_1 ⟶ j'
⊢ Eq (α := F.obj (op (↑(unop j') : J)))
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (F.map
              (Quiver.Hom.op (map (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) f.unop))) :
          (a : F.obj (op (↑(unop j_1) : J))) → F.obj (op (↑(unop j') : J)))
        (val (e (↑j_1.1 : J) ⋯)) :
      F.obj (op (↑(unop j') : J)))
    (val (e (↑j'.1 : J) ⋯) : F.obj (op (↑j'.1 : J)))

Tactic:
apply compatibility

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.compatibility
-- 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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ ⊥ < j

Tactic:
simpa [bot_lt_iff_ne_bot] using hj.not_isMin

Premises used: bot_lt_iff_ne_bot, Order.IsSuccLimit.not_isMin
-- 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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ (↑(Subtype.mk (p :=
            fun
              (x :
                (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                  obj
                    (Functor.op
                        (Monotone.functor (f :=
                          (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J))
                          ⋯) ⋙
                      F)
                    j_1) ↦
            Membership.mem (γ :=
              Set
                ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                  obj
                    (Functor.op
                        (Monotone.functor (f :=
                          (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J))
                          ⋯) ⋙
                      F)
                    j_1))
              (sections
                (Functor.op
                    (Monotone.functor (f :=
                      (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
                  F))
              x)
            (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦
              match (motive :=
                (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                  obj
                    (Functor.op
                        (Monotone.functor (f :=
                          (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J))
                          ⋯) ⋙
                      F)
                    x)
                x with
              | op ⟨i, hi⟩ => (e i hi).val)
            ⋯) :
        (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ F).obj j_1)
      (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) ⊥ ⋯)) =
    val₀

Tactic:
simpa using (e ⊥ (by simpa [bot_lt_iff_ne_bot] using hj.not_isMin)).map_zero

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.map_zero, Bot.bot
-- 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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
simp : ∃ (b : J), i < b
⊢ i < Order.succ i

Tactic:
simp only [Order.lt_succ_iff_not_isMax, not_isMax_iff]

Premises used: Order.lt_succ_iff_not_isMax, not_isMax_iff
-- 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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ ∃ (b : J), i < b

Tactic:
⟨_, hi⟩

Premises used: Exists.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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ ∃ (b : J), i < b

Tactic:
exact ⟨_, 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
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
i : J
hi : i < j
⊢ Eq (α := F.obj (op 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)))
        (val (e (Order.succ i) ⋯)) :
      (fun (X : Type v) ↦ X) (F.obj (op i)))
    ((↑(Subtype.mk (p :=
              fun
                (x :
                  (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                    obj
                      (Functor.op
                          (Monotone.functor (f :=
                            (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) :
                              (a : { x : J // x ∈ Set.Iio j }) → J))
                            ⋯) ⋙
                        F)
                      j_1) ↦
              Membership.mem (γ :=
                Set
                  ((j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                    obj
                      (Functor.op
                          (Monotone.functor (f :=
                            (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) :
                              (a : { x : J // x ∈ Set.Iio j }) → J))
                            ⋯) ⋙
                        F)
                      j_1))
                (sections
                  (Functor.op
                      (Monotone.functor (f :=
                        (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J))
                        ⋯) ⋙
                    F))
                x)
              (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦
                match (motive :=
                  (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) →
                    obj
                      (Functor.op
                          (Monotone.functor (f :=
                            (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) :
                              (a : { x : J // x ∈ Set.Iio j }) → J))
                            ⋯) ⋙
                        F)
                      x)
                  x with
                | op ⟨i, hi⟩ => (e i hi).val)
              ⋯) :
          (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ F).obj j_1)
        (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi)) :
      obj (C := { x : J // x ∈ Set.Iio j }ᵒᵖ)
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          F)
        (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi)))

Tactic:
apply compatibility

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.compatibility
-- 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
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
⊢ 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
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
⊢ (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 i hij').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 i hij').val)
        ⋯)

Tactic:
have := (e i hij').map_limit i hi (by rfl)