awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
j : J
hj : ¬IsMax j
⊢ Φ.prop (X := Functor.obj (Φ.iterationFunctor J) j) (Y := Functor.obj (Φ.iterationFunctor J) (Order.succ j))
    (Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))
have this : Φ.prop (X :=
  Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type w)) (Iteration.F (Φ.iter (Order.succ j)))
    (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j sorry))
  (Y :=
  Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type w)) (Iteration.F (Φ.iter (Order.succ j)))
    (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))
  (Functor.map (Iteration.F (Φ.iter (Order.succ j))) (homOfLE sorry))
Tactic: have := (Φ.iter (Order.succ j)).prop_map_succ j (Order.lt_succ_of_not_isMax hj)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteIteration (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{w, v, u} J C
j : J
hj : ¬IsMax j
this :
  Φ.prop (X :=
    Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type w)) (Iteration.F (Φ.iter (Order.succ j)))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯))
    (Y :=
    Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type w)) (Iteration.F (Φ.iter (Order.succ j)))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
    (Functor.map (Iteration.F (Φ.iter (Order.succ j))) (homOfLE ⋯))
⊢ Φ.prop (X := Functor.obj (Φ.iterationFunctor J) j) (Y := Functor.obj (Φ.iterationFunctor J) (Order.succ j))
    (Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))
have rw : ∀
  (this :
    Arrow.mk (X :=
        Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type w)) (Iteration.F (Φ.iter (Order.succ j)))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j sorry))
        (Y :=
        Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type w)) (Iteration.F (Φ.iter (Order.succ j)))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))
        (Functor.map (Iteration.F (Φ.iter (Order.succ j))) (homOfLE sorry)) =
      Φ.toSuccArrow
        (Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type w)) (Iteration.F (Φ.iter (Order.succ j)))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j sorry))),
  Arrow.mk (X := Functor.obj (Φ.iterationFunctor J) j) (Y := Functor.obj (Φ.iterationFunctor J) (Order.succ j))
      (Functor.map (Φ.iterationFunctor J) (homOfLE sorry)) =
    Φ.toSuccArrow (Functor.obj (Φ.iterationFunctor J) j)
Tactic: rw [prop_iff] at this ⊢
Cleared hypotheses: this
-- 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
val : F.obj (op j)
map_zero :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op ⊥)))
      val =
    val₀
map_succ :
  ∀ (i : J) (hi : i < j),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
        val =
      d.succ i ⋯
        ((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 i)))
          val)
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
j_1 j' : { x : J // x ∈ Set.Iio i }ᵒᵖ
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 i)) ⋯) f.unop))) :
            TypeCat.Fun (F.obj (op (↑(unop j_1) : J))) (F.obj (op (↑(unop j') : J)))) :
          (a : F.obj (op (↑(unop j_1) : J))) → F.obj (op (↑(unop j') : J)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : F.obj (op j)) → F.obj (op (↑j_1.1 : J)))
            val :
          F.obj (op (↑j_1.1 : J))) :
      F.obj (op (↑(unop j') : J)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : F.obj (op j)) → F.obj (op (↑j'.1 : J)))
        val :
      F.obj (op (↑j'.1 : J)))
have rw : Eq (α := F.obj (op (↑(unop j') : J)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (CategoryStruct.comp (Y := op (↑j_1.1 : J)) (Quiver.Hom.op (homOfLE sorry))
              (Quiver.Hom.op
                (map (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) sorry) f.unop)))) :
        (a : F.obj (op j)) → F.obj (op (↑(unop j') : J)))
      val :
    F.obj (op (↑(unop j') : J)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : F.obj (op j)) → F.obj (op (↑j'.1 : J)))
      val :
    F.obj (op (↑j'.1 : J)))
Tactic: rw [← comp_apply, ← map_comp]
-- 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
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 ⊥)))
      ((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))) =
    val₀
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((homOfLE hij).op ≫ Quiver.Hom.op (homOfLE sorry))) :
      (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op ⊥))
    e.val =
  val₀
Tactic: rw [← comp_apply, ← map_comp]
-- 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
i : J
hij : i ≤ j
k : J
hk : k < 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 (Order.succ k))))
      ((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))) =
    d.succ k ⋯
      ((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)))
        ((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))))
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op ≫ F.map (Quiver.Hom.op (homOfLE sorry))) :
      (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
    e.val =
  d.succ k sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
      ((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: rw [← comp_apply, ← map_comp, ← comp_apply, ← map_comp, ← op_comp, ← op_comp,
      homOfLE_comp, homOfLE_comp, e.map_succ k (lt_of_lt_of_le hk hij)]
-- 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
i : J
hij : i ≤ j
k : J
hk : k < i
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op ≫ F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((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)))
        ((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))))
⊢ (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 (Order.succ k))))
      ((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))) =
    d.succ k ⋯
      ((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)))
        ((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))))
have rw₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((homOfLE hij).op ≫ Quiver.Hom.op (homOfLE sorry))) :
      (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
    e.val =
  d.succ k sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op i))) → (fun (X : Type v) ↦ X) (F.obj (op k)))
      ((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: rw [← comp_apply, ← map_comp, ← comp_apply, ← map_comp, ← op_comp, ← op_comp,
      homOfLE_comp, homOfLE_comp, e.map_succ k (lt_of_lt_of_le hk hij)]
-- 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
i : J
hij : i ≤ j
k : J
hk : k < i
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op ≫ F.map (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((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)))
        ((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))))
rw₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((homOfLE hij).op ≫ Quiver.Hom.op (homOfLE ⋯))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
      e.val =
    d.succ k ⋯
      ((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)))
        ((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))))
⊢ (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 (Order.succ k))))
      ((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))) =
    d.succ k ⋯
      ((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)))
        ((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))))
have rw₂ : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((homOfLE hij).op ≫ Quiver.Hom.op (homOfLE sorry))) :
      (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op (Order.succ k)))
    e.val =
  d.succ k sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op ≫ F.map (homOfLE sorry).op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op j))) → F.obj (op k))
      e.val)
Tactic: rw [← comp_apply, ← map_comp, ← comp_apply, ← map_comp, ← op_comp, ← op_comp,
      homOfLE_comp, homOfLE_comp, e.map_succ k (lt_of_lt_of_le hk hij)]
-- 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
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
l : J
hl : l ∈ Set.Iio k
⊢ Eq.{v + 1} (α :=
    obj
      (Functor.op
          (Monotone.functor (f :=
            (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) ⋯) ⋙
        F)
      (op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio k) l hl)))
    (match (motive :=
      (x : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
        obj
          (Functor.op
              (Monotone.functor (f :=
                (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) ⋯) ⋙
            F)
          x)
      op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio k) l hl) with
    | op ⟨k_1, 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_1)))
        e.val)
    (match (motive :=
      (x : { x : J // x ∈ Set.Iio k }ᵒᵖ) →
        obj
          (Functor.op
              (Monotone.functor (f :=
                (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio k) : (a : { x : J // x ∈ Set.Iio k }) → J)) ⋯) ⋙
            F)
          x)
      op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio k) l hl) with
    | op ⟨k_1, 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_1)))
        ((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))))
have e_x : Eq (α := F.obj (op l))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) : (a : F.obj (op j)) → F.obj (op l)) e.val :
    F.obj (op l))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) : (a : F.obj (op i)) → F.obj (op l))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op) : (a : F.obj (op j)) → F.obj (op i)) e.val :
        F.obj (op i)) :
    F.obj (op l))
Tactic: dsimp
-- 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
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
l : J
hl : l ∈ Set.Iio k
⊢ 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 i)) → F.obj (op l))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE hij).op) : (a : F.obj (op j)) → F.obj (op i)) e.val :
          F.obj (op i)) :
      F.obj (op l))
have e_x : Eq (α := F.obj (op l))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (homOfLE sorry).op) : (a : F.obj (op j)) → F.obj (op l)) e.val :
    F.obj (op l))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((homOfLE hij).op ≫ (homOfLE sorry).op)) :
        (a : F.obj (op j)) → F.obj (op l))
      e.val :
    F.obj (op l))
Tactic: rw [← comp_apply, ← map_comp]
-- 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 : IsMin i
⊢ Subsingleton.{v + 1} (d.Extension val₀ i)
have isMin : ∀ (hi : IsMin.{u} (α := J) ⊥), Subsingleton.{v + 1} (d.Extension val₀ ⊥)
Tactic: obtain rfl : i = ⊥ := by simpa using hi
Cleared hypotheses: i, 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
hi : IsMin.{u} (α := J) ⊥
⊢ Subsingleton.{v + 1} (d.Extension val₀ ⊥)
have isMin : ∀ (e₁ e₂ : d.Extension val₀ ⊥), e₁.val = e₂.val
Tactic: refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (hypothesis)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
hi : IsMin.{u} (α := J) ⊥
e₁ e₂ : d.Extension val₀ ⊥
⊢ e₁.val = e₂.val
have h₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
      (a : (fun (X : Type v) ↦ X) (F.obj (op ⊥))) → (fun (X : Type v) ↦ X) (F.obj (op ⊥)))
    e₁.val =
  val₀
Tactic: have h₁ := e₁.map_zero
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (hypothesis)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
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₀
⊢ e₁.val = e₂.val
have h₂ : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
      (a : (fun (X : Type v) ↦ X) (F.obj (op ⊥))) → (fun (X : Type v) ↦ X) (F.obj (op ⊥)))
    e₂.val =
  val₀
Tactic: have h₂ := e₂.map_zero
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (hypothesis)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
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₀
⊢ e₁.val = e₂.val
have h₃ : e₁.val = val₀
Tactic: simp only [homOfLE_refl, op_id, map_id, id_apply] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (hypothesis)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
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 = e₂.val
have h₄ : e₂.val = val₀
Tactic: simp only [homOfLE_refl, op_id, map_id, id_apply] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (goal)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
hi : IsMin.{u} (α := J) ⊥
e₁ e₂ : d.Extension val₀ ⊥
h₁ : e₁.val = val₀
h₂ : e₂.val = val₀
⊢ e₁.val = e₂.val
have isMin : val₀ = e₂.val
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (goal)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
hi : IsMin.{u} (α := J) ⊥
e₁ e₂ : d.Extension val₀ ⊥
h₁ : e₁.val = val₀
h₂ : e₂.val = val₀
isMin : val₀ = e₂.val
⊢ e₁.val = e₂.val
have isMin₁ : val₀ = val₀
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (goal)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
i : J
hi : ¬IsMax i
hi' : Subsingleton.{v + 1} (d.Extension val₀ i)
⊢ Subsingleton.{v + 1} (d.Extension val₀ (Order.succ i))
have succ : ∀ (e₁ e₂ : d.Extension val₀ (Order.succ i)), e₁.val = e₂.val
Tactic: refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.WellOrderInductionData (hypothesis)
Goal:
J : Type u
inst : LinearOrder J
inst_1 : SuccOrder J
F : Functor.{u, v, u, v + 1} Jᵒᵖ (Type v)
d : F.WellOrderInductionData
inst_2 : OrderBot J
val₀ : F.obj (op ⊥)
inst_3 : WellFoundedLT J
i : J
hi : ¬IsMax i
hi' : Subsingleton.{v + 1} (d.Extension val₀ i)
e₁ e₂ : d.Extension val₀ (Order.succ i)
⊢ e₁.val = e₂.val
have h₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
      (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i))))
    e₁.val =
  d.succ i sorry
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (Order.succ i)))) → (fun (X : Type v) ↦ X) (F.obj (op i)))
      e₁.val)
Tactic: have h₁ := e₁.map_succ i (Order.lt_succ_of_not_isMax hi)