awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
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
x x_1 : J
f : x ⟶ x_1
dsimp :
  Eq (α := Φ.X₀ ⟶ Functor.obj (Φ.iterationFunctor J) x_1)
    (𝟙 Φ.X₀ ≫ Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))
    ((Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯)) ≫
      Functor.map (Φ.iterationFunctor J) f)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) Φ.X₀) x ⟶ Functor.obj (Φ.iterationFunctor J) x_1)
    (Functor.map (Functor.obj (Functor.const J) Φ.X₀) f ≫
      Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))
    ((Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯)) ≫
      Functor.map (Φ.iterationFunctor J) f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
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
x x_1 : J
f : x ⟶ x_1
rw :
  Eq (α := Φ.X₀ ⟶ Functor.obj (Φ.iterationFunctor J) x_1)
    (Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))
    (Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯ ≫ f))
⊢ Eq (α := Φ.X₀ ⟶ Functor.obj (Φ.iterationFunctor J) x_1)
    (𝟙 Φ.X₀ ≫ Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))
    ((Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯)) ≫
      Functor.map (Φ.iterationFunctor J) f)

Tactic:
rw [id_comp, assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
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
x x_1 : J
f : x ⟶ x_1
⊢ Eq (α := Φ.X₀ ⟶ Functor.obj (Φ.iterationFunctor J) x_1)
    (Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))
    (Iso.inv (Φ.iterationFunctorObjBotIso J) ≫ Functor.map (Φ.iterationFunctor J) (homOfLE ⋯ ≫ f))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
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 (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 ⋯))

Tactic:
have := (Φ.iter (Order.succ j)).prop_map_succ j (Order.lt_succ_of_not_isMax hj)
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
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 ⋯))
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 ⋯))
          (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 ⋯)) =
        Φ.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 ⋯))),
    Arrow.mk (X := Functor.obj (Φ.iterationFunctor J) j) (Y := Functor.obj (Φ.iterationFunctor J) (Order.succ j))
        (Functor.map (Φ.iterationFunctor J) (homOfLE ⋯)) =
      Φ.toSuccArrow (Functor.obj (Φ.iterationFunctor J) j)
⊢ Φ.prop (X := Functor.obj (Φ.iterationFunctor J) j) (Y := Functor.obj (Φ.iterationFunctor J) (Order.succ j))
    (Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))

Tactic:
rw [prop_iff] at this ⊢

Premises used: CategoryTheory.SmallObject.SuccStruct.prop_iff
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
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 :
  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 ⋯))
      (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 ⋯)) =
    Φ.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 ⋯))
⊢ Order.succ j ≤ Order.succ j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
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 :
  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 ⋯))
      (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 ⋯)) =
    Φ.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 ⋯))
⊢ Arrow.mk (X := Functor.obj (Φ.iterationFunctor J) j) (Y := Functor.obj (Φ.iterationFunctor J) (Order.succ j))
      (Functor.map (Φ.iterationFunctor J) (homOfLE ⋯)) =
    Φ.toSuccArrow (Functor.obj (Φ.iterationFunctor J) j)

Tactic:
simp only [Φ.iterationFunctor_obj j (Φ.iter (Order.succ j)) (Order.le_succ j),
      Φ.arrowMk_iterationFunctor_map _ _ (Order.le_succ j) (Φ.iter (Order.succ j)) (by simp),
      this]

Premises used: Order.succ, CategoryTheory.SmallObject.SuccStruct.arrowMk_iterationFunctor_map, CategoryTheory.SmallObject.SuccStruct.iter, Order.le_succ, CategoryTheory.SmallObject.SuccStruct.iterationFunctor_obj
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
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 ⋯))

Tactic:
(Φ.transfiniteCompositionOfShapeιIteration J).map_mem j hj

Premises used: CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map_mem
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
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
⊢ Eq (α := Functor.obj (Φ.iterationFunctor J) j ⟶ Functor.obj (Φ.iterationFunctor J) (Order.succ j))
    (Functor.map (Φ.iterationFunctor J) (homOfLE ⋯))
    (Φ.toSucc (Functor.obj (Φ.iterationFunctor J) j) ≫ Iso.inv (Φ.iterationFunctorObjSuccIso j hj))

Tactic:
(Φ.prop_iterationFunctor_map_succ j hj).fac

Premises used: Eq.mpr, CategoryTheory.eqToHom, CategoryTheory.SmallObject.SuccStruct.prop_iterationFunctor_map_succ, CategoryTheory.SmallObject.SuccStruct.prop.fac
-- 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
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'
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 ⋯))
                (Quiver.Hom.op
                  (map (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) 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 ⋯))) :
          (a : F.obj (op j)) → F.obj (op (↑j'.1 : J)))
        val :
      F.obj (op (↑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)))

Tactic:
rw [← comp_apply, ← map_comp]

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- 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
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 (FC := TypeCat.Fun)
            (F.map
              (CategoryStruct.comp (Y := op (↑j_1.1 : J)) (Quiver.Hom.op (homOfLE ⋯))
                (Quiver.Hom.op
                  (map (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio i)) ⋯) 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 ⋯))) :
          (a : F.obj (op j)) → F.obj (op (↑j'.1 : J)))
        val :
      F.obj (op (↑j'.1 : J)))

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
i : J
hij : i ≤ j
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 ⊥))
      e.val =
    val₀
⊢ (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₀

Tactic:
rw [← comp_apply, ← map_comp]

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- 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
i : J
hij : i ≤ j
⊢ (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 ⊥))
      e.val =
    val₀

Tactic:
e.map_zero

Premises used: CategoryTheory.Functor.WellOrderInductionData.Extension.map_zero, CategoryTheory.homOfLE
-- 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
i : J
hij : i ≤ j
⊢ (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 ⊥))
      e.val =
    val₀

Tactic:
exact e.map_zero

Premises used: 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
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
e_x :
  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))
⊢ 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))))

Tactic:
dsimp
-- 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
i : J
hij : i ≤ j
k : J
hk : Order.IsSuccLimit k
hki : k ≤ i
l : J
hl : l ∈ Set.Iio k
e_x :
  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 hij).op ≫ (homOfLE ⋯).op)) :
          (a : F.obj (op j)) → F.obj (op l))
        e.val :
      F.obj (op l))
⊢ 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))

Tactic:
rw [← comp_apply, ← map_comp]

Premises used: CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp
-- 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
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 hij).op ≫ (homOfLE ⋯).op)) :
          (a : F.obj (op j)) → F.obj (op l))
        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 ⊥)
inst_3 : WellFoundedLT J
i : J
hi : IsMin i
⊢ i = ⊥

Tactic:
simpa using 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 : IsMin i
isMin : ∀ (hi : IsMin.{u} (α := J) ⊥), Subsingleton.{v + 1} (d.Extension val₀ ⊥)
⊢ Subsingleton.{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) ⊥
⊢ Subsingleton.{v + 1} (d.Extension val₀ ⊥)

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
hi : IsMin.{u} (α := J) ⊥
isMin : ∀ (e₁ e₂ : d.Extension val₀ ⊥), e₁.val = e₂.val
⊢ Subsingleton.{v + 1} (d.Extension val₀ ⊥)

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
hi : IsMin.{u} (α := J) ⊥
e₁ e₂ : d.Extension val₀ ⊥
⊢ (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₀

Tactic:
have h₁ := e₁.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
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₀
⊢ (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₀

Tactic:
have h₂ := e₂.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
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 = 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