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
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 :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 (op i))) : (a : F.obj (op i)) → F.obj (op i)) (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)
        ⋯)
⊢ (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)
        ⋯)

Tactic:
rw [map_id, id_apply] at this

Premises used: CategoryTheory.id_apply, CategoryTheory.Functor.map_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
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)
        ⋯)
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 ⋯))) :
            (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 ⋯))) :
            (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)) ⋯) ⋙ F))
                x)
              (fun (x : { x : J // x ∈ Set.Iio j }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)) :
        F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
⊢ 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) ⋯)) ⋯))

Tactic:
ext ⟨⟨l, hl⟩⟩
-- 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
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)
        ⋯)
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 i hij').val :
      F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
    ((↑(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) ⋯)) ⋯) :
          (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) l ⋯)) :
      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) l ⋯)))

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
i : J
hi hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
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) ⋯)) 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) ⋯)) ⋯))
⊢ 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) ⋯)) ⋯)))
        ⋯)

Tactic:
congr
-- 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 hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
inr :
  ∀ (l : J) (hl : l ∈ Set.Iio i),
    Eq (α := F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
      (val (e (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J) ⋯))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op i)) → F.obj (op (↑(op ⟨l, hl⟩).1 : J)))
        (d.lift i hj
          (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
            Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
              (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F)) x)
            (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)))
⊢ Eq (α := (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J)))
    (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : F.obj (op i)) → F.obj (op (↑x.1 : J)))
      (d.lift i hj
        (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
          Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
            (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F)) x)
          (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯))

Tactic:
ext ⟨⟨l, hl⟩⟩
-- 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 hj : Order.IsSuccLimit i
e : (i_1 : J) → i_1 < i → d.Extension val₀ i_1
hij : i ≤ i
l : J
hl : l ∈ Set.Iio i
inr inr₁ :
  Eq (α := F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
    (val (e (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J) ⋯))
    ((↑(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) ⋯)) ⋯) :
        (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → (⋯.functor.op ⋙ F).obj j)
      (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)))
⊢ Eq (α := F.obj (op (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J)))
    (val (e (↑(op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l hl)).1 : J) ⋯))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : F.obj (op i)) → F.obj (op (↑(op ⟨l, hl⟩).1 : J)))
      (d.lift i hj
        (Subtype.mk (p := fun (x : (j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))) ↦
          Membership.mem (γ := Set ((j : { x : J // x ∈ Set.Iio i }ᵒᵖ) → F.obj (op (↑(unop j) : J))))
            (sections (Functor.op (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) ⋙ F)) x)
          (fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) ↦ val (e (↑x.1 : J) ⋯)) ⋯)))

Tactic:
rw [d.map_lift _ _ _ _ hl]

Premises used: CategoryTheory.Functor.WellOrderInductionData.map_lift
-- 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 : IsMin i
isMin : ∀ (hi : IsMin.{u} (α := J) ⊥), Nonempty.{v + 1} (d.Extension val₀ ⊥)
⊢ Nonempty.{v + 1} (d.Extension val₀ i)

Tactic:
obtain rfl : i = ⊥ := by simpa using hi

Premises used: 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
hi : IsMin.{u} (α := J) ⊥
⊢ Nonempty.{v + 1} (d.Extension val₀ ⊥)

Tactic:
⟨zero d val₀⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.WellOrderInductionData.Extension.zero
-- 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) ⊥
⊢ Nonempty.{v + 1} (d.Extension val₀ ⊥)

Tactic:
exact ⟨zero d 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 ⊥)
inst_3 : WellFoundedLT J
i : J
hi : ¬IsMax i
hi' : Nonempty.{v + 1} (d.Extension val₀ i)
⊢ Nonempty.{v + 1} (d.Extension val₀ (Order.succ i))

Tactic:
⟨hi'.some.succ hi⟩

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.succ, Nonempty.some, Nonempty.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' : Nonempty.{v + 1} (d.Extension val₀ i)
⊢ Nonempty.{v + 1} (d.Extension val₀ (Order.succ i))

Tactic:
exact ⟨hi'.some.succ 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 : Order.IsSuccLimit i
hi' : ∀ b < i, Nonempty.{v + 1} (d.Extension val₀ b)
⊢ Nonempty.{v + 1} (d.Extension val₀ i)

Tactic:
⟨limit i hi (fun l hl ↦ (hi' l hl).some)⟩

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.limit, Nonempty.some, Nonempty.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, Nonempty.{v + 1} (d.Extension val₀ b)
⊢ Nonempty.{v + 1} (d.Extension val₀ i)

Tactic:
exact ⟨limit i hi (fun l hl ↦ (hi' l hl).some)⟩
-- 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
isMin : ∀ (i : J) (hi : IsMin i), Nonempty.{v + 1} (d.Extension val₀ i)
succ :
  ∀ (i : J) (hi : ¬IsMax i) (hi' : Nonempty.{v + 1} (d.Extension val₀ i)),
    Nonempty.{v + 1} (d.Extension val₀ (Order.succ i))
isSuccLimit :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hi' : ∀ b < i, Nonempty.{v + 1} (d.Extension val₀ b)),
    Nonempty.{v + 1} (d.Extension val₀ i)
⊢ Nonempty.{v + 1} (d.Extension val₀ j)

Tactic:
induction j using SuccOrder.limitRecOn with
  | isMin i hi =>
    obtain rfl : i = ⊥ := by simpa using hi
    exact ⟨zero d val₀⟩
  | succ i hi hi' => exact ⟨hi'.some.succ hi⟩
  | isSuccLimit i hi hi' => exact ⟨limit i hi (fun l hl ↦ (hi' l hl).some)⟩

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.succ, 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
inst_3 : WellFoundedLT J
val₀ : F.obj (op ⊥)
j j' : Jᵒᵖ
f : j ⟶ j'
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj j)) → (fun (X : Type v) ↦ X) (F.obj j'))
        ((fun (j : Jᵒᵖ) ↦ (Extension.val (d := d) (val₀ := val₀) default : F.obj (op (unop j)))) j) :
      (fun (X : Type v) ↦ X) (F.obj j'))
    ((fun (j : Jᵒᵖ) ↦ (Extension.val (d := d) (val₀ := val₀) default : F.obj (op (unop j)))) j' : F.obj (op (unop j')))

Tactic:
apply Extension.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
inst_3 : WellFoundedLT J
val₀ : F.obj (op ⊥)
⊢ (↑(d.sectionsMk val₀) : (j : Jᵒᵖ) → F.obj j) (op ⊥) = val₀

Tactic:
simpa using (default : d.Extension val₀ ⊥).map_zero

Premises used: Inhabited.default, CategoryTheory.Functor.WellOrderInductionData.Extension.map_zero
-- 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
inst_3 : WellFoundedLT J
⊢ Function.Surjective (α := (↑F.sections : Type (max u v))) (β := F.obj (op ⊥))
    ((fun (s : (j : Jᵒᵖ) → F.obj j) ↦ s (op ⊥)) ∘ Subtype.val (p := fun (x : (j : Jᵒᵖ) → F.obj j) ↦ x ∈ F.sections))

Tactic:
fun val₀ ↦ ⟨d.sectionsMk val₀, d.sectionsMk_val_op_bot val₀⟩

Premises used: CategoryTheory.Functor.WellOrderInductionData.sectionsMk_val_op_bot, Exists.intro, Function.Surjective, CategoryTheory.Functor.WellOrderInductionData.sectionsMk
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x : (↑h.smallCategoryOfSet.obj : Type w)
rw :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
    (((h.homEquiv :
            Equiv.{w + 1, v + 1} (↑(h.hom x x) : Type w)
              (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
                ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))) :
          (a : (↑(h.hom x x) : Type w)) →
            (h.objEquiv : (a : (↑h.obj : Type w)) → C) x ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) x)
        (h.smallCategoryOfSet.id x) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
    (𝟙 ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
    (((h.homEquiv :
            Equiv.{w + 1, v + 1} (↑(h.hom x x) : Type w)
              (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
                ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))) :
          (a : (↑(h.hom x x) : Type w)) →
            (h.objEquiv : (a : (↑h.obj : Type w)) → C) x ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) x)
        (𝟙 x) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
    (𝟙 ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))

Tactic:
rw [SmallCategoryOfSet.id_def]

Premises used: CategoryTheory.SmallCategoryOfSet.id_def
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
Ω : Type w
C : Type u
inst : Category.{v, u} C
h : CoreSmallCategoryOfSet.{w, v, u} Ω C
x : (↑h.smallCategoryOfSet.obj : Type w)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
      ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
    (((h.homEquiv :
            Equiv.{w + 1, v + 1} (↑(h.hom x x) : Type w)
              (Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
                ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))) :
          (a : (↑(h.hom x x) : Type w)) →
            (h.objEquiv : (a : (↑h.obj : Type w)) → C) x ⟶ (h.objEquiv : (a : (↑h.obj : Type w)) → C) x)
        (h.smallCategoryOfSet.id x) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))
    (𝟙 ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x) :
      Quiver.Hom.{v, u} (V := C) ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C)
        ((h.objEquiv : (a : (↑h.obj : Type w)) → C) x : C))

Tactic:
simp