awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i < j
rw :
  (if h₁ : i < j then
      (ofCocone.objIso c i h₁).hom ≫
        c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i h₁) ≫ (ofCocone.objIsoPt c).inv ≫ 𝟙 (ofCocone.obj c j)
    else eqToHom ⋯) =
    (ofCocone.objIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv
rw₁ :
  (ofCocone.objIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv ≫ 𝟙 (ofCocone.obj c j) =
    (ofCocone.objIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv
rw₂ rw₃ :
  (ofCocone.objIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv =
    (ofCocone.objIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv
⊢ (if h₂ : j < j then Iso.hom (ofCocone.objIso c i ⋯) ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c j h₂).inv
    else
      if h₁ : i < j then
        (ofCocone.objIso c i h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i h₁) ≫
            (ofCocone.objIsoPt c).inv ≫ 𝟙 (ofCocone.obj c j)
      else eqToHom ⋯) =
    (ofCocone.objIso c i hi).hom ≫
      c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCocone.objIsoPt c).inv

Tactic:
rw [dif_neg (by simp), dif_pos hi, comp_id]

Premises used: dif_pos, CategoryTheory.Category.comp_id, dif_neg
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
dsimp :
  (if h₂ : i₂ < j then Iso.hom (ofCocone.objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c i₂ h₂).inv
    else
      if h₁ : i₁ < j then
        (ofCocone.objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (ofCocone.objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯) =
    Iso.hom (ofCocone.objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCocone.objIso c i₂ hi₂).inv
⊢ (ofCocone c).map (homOfLE hi) = Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv

Tactic:
dsimp [ofCocone, ofCoconeObjIso, ofCocone.map]

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCocone.map, CategoryTheory.SmallObject.SuccStruct.ofCocone, CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
rw rw₁ :
  Iso.hom (ofCocone.objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c i₂ hi₂).inv =
    Iso.hom (ofCocone.objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCocone.objIso c i₂ hi₂).inv
⊢ (if h₂ : i₂ < j then Iso.hom (ofCocone.objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c i₂ h₂).inv
    else
      if h₁ : i₁ < j then
        (ofCocone.objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (ofCocone.objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯) =
    Iso.hom (ofCocone.objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCocone.objIso c i₂ hi₂).inv

Tactic:
rw [dif_pos hi₂]

Premises used: dif_pos
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
rw :
  (Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫
      (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
rw₁ :
  Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫
      (F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv) ≫ (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
rw₂ :
  Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv ≫ (ofCoconeObjIso c i₂ hi₂).hom =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
rw₃ :
  Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫
      F.map (homOfLE hi) ≫ 𝟙 (F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ hi₂)) =
    Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
rw₄ rw₅ : Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi) = Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)
⊢ (ofCocone c).map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).hom = Iso.hom (ofCoconeObjIso c i₁ ⋯) ≫ F.map (homOfLE hi)

Tactic:
rw [ofCocone_map c i₁ i₂ hi hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.SmallObject.SuccStruct.ofCocone_map
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
X Y : (↑(Set.Iio j) : Type u)
f : X ⟶ Y
⊢ (restrictionLT (ofCocone c) ⋯).map f ≫
      Iso.hom
        ((fun (x : (↑(Set.Iio j) : Type u)) ↦
            (match (motive := (x : (↑(Set.Iio j) : Type u)) → (restrictionLT (ofCocone c) ⋯).obj x ≅ F.obj x) x with
              | ⟨i, hi⟩ => ofCoconeObjIso c i hi :
              (restrictionLT (ofCocone c) ⋯).obj x ≅ F.obj x))
          Y) =
    Iso.hom
        ((fun (x : (↑(Set.Iio j) : Type u)) ↦
            (match (motive := (x : (↑(Set.Iio j) : Type u)) → (restrictionLT (ofCocone c) ⋯).obj x ≅ F.obj x) x with
              | ⟨i, hi⟩ => ofCoconeObjIso c i hi :
              (restrictionLT (ofCocone c) ⋯).obj x ≅ F.obj x))
          X) ≫
      F.map f

Tactic:
apply ofCoconeObjIso_hom_naturality

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
hc : IsColimit c
x : (↑(Set.Iio j) : Type u)
i : J
hi : i ∈ Set.Iio j
dsimp :
  Eq (α :=
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
      (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
    (Iso.inv (ofCoconeObjIso c i ⋯) ≫ (ofCocone c).map (homOfLE ⋯))
⊢ Eq (α :=
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
      ((Cocone.precompose (restrictionLTOfCoconeIso c).inv).obj (coconeOfLE (ofCocone c) ⋯)).pt)
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).symm.hom)
    (((Cocone.precompose (restrictionLTOfCoconeIso c).inv).obj (coconeOfLE (ofCocone c) ⋯)).ι.app
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
hc : IsColimit c
x : (↑(Set.Iio j) : Type u)
i : J
hi : i ∈ Set.Iio j
rw :
  Eq (α :=
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
      (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
    (Iso.inv (ofCoconeObjIso c i ⋯) ≫
      (ofCoconeObjIso c i hi).hom ≫
        c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
rw₁ rw₂ :
  Eq (α :=
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
      (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
⊢ Eq (α :=
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ⟶
      (ofCocone c).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))
    (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv)
    (Iso.inv (ofCoconeObjIso c i ⋯) ≫ (ofCocone c).map (homOfLE ⋯))

Tactic:
rw [ofCocone_map_to_top _ _ hi, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.SmallObject.SuccStruct.ofCocone_map_to_top
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂ : i₂ < j
⊢ arrowMap (ofCocone c) i₁ i₂ h₁₂ ⋯ = Arrow.mk (F.map (homOfLE h₁₂))

Tactic:
Arrow.ext (ofCocone_obj_eq _ _ _) (ofCocone_obj_eq _ _ _) (ofCocone_map _ _ _ _ _)

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq, CategoryTheory.SmallObject.SuccStruct.ofCocone_map, CategoryTheory.Arrow.ext
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i < j
⊢ j ≤ j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i < j
rw :
  Arrow.mk
      ((ofCoconeObjIso c i hi).hom ≫
        c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv) =
    Arrow.mk (X := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))
⊢ arrowMap (ofCocone c) i j ⋯ ⋯ =
    Arrow.mk (X := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))

Tactic:
rw [arrowMap, ofCocone_map_to_top _ _ hi]

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCocone_map_to_top, CategoryTheory.SmallObject.SuccStruct.arrowMap
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i < j
⊢ Arrow.mk
      ((ofCoconeObjIso c i hi).hom ≫
        c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv) =
    Arrow.mk (X := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))

Tactic:
Arrow.ext (ofCocone_obj_eq _ _ _) (ofCocone_obj_eq_pt _) rfl

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq_pt, CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq, rfl, CategoryTheory.Arrow.ext
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
j : J
F : Functor.{u, v_1, u, u_1} (↑(Set.Iio j) : Type u) C
c : Cocone F
i : J
hi : i < j
⊢ Arrow.mk
      ((ofCoconeObjIso c i hi).hom ≫
        c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) ≫ (ofCoconeObjIsoPt c).inv) =
    Arrow.mk (X := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))
      (c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))

Tactic:
exact Arrow.ext (ofCocone_obj_eq _ _ _) (ofCocone_obj_eq_pt _) rfl

Premises used: CategoryTheory.Arrow.ext
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
x : J
h : x < ⊥
⊢ arrowSucc (Functor.obj (Functor.const (↑(Set.Iic ⊥) : Type u)) Φ.X₀) x h =
    Φ.toSuccArrow
      (Functor.obj.{u, v_1, u, u_1} (C := (↑(Set.Iic ⊥) : Type u))
        (Functor.obj (Functor.const (↑(Set.Iic ⊥) : Type u)) Φ.X₀)
        (Subtype.mk (p := fun (x : J) ↦ Membership.mem (γ := Set J) (Set.Iic ⊥) x) x ⋯))

Tactic:
simp at h
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
x : J
h₁ : Order.IsSuccLimit x
h₂ : x ≤ ⊥
⊢ IsMin x

Tactic:
simpa using h₂
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
rw : iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) ⊥ ⋯) = Φ.X₀
rw₁ rw₂ : Φ.X₀ = Φ.X₀
⊢ obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
      (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) ⊥ ⋯) =
    Φ.X₀

Tactic:
rw [extendToSucc_obj_eq _ _ _ _ bot_le, obj_bot]

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_eq, CategoryTheory.SmallObject.SuccStruct.Iteration.obj_bot, bot_le
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁ : i < Order.succ j
⊢ i ≤ j

Tactic:
rw [Order.lt_succ_iff_of_not_isMax hj] at hi₁

Premises used: Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁_1 : i < Order.succ j
hi₁ : i ≤ j
inl :
  ∀ (hi₁ : i < j),
    arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
        hi₁_1 =
      Φ.toSuccArrow
        (obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
          (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))
inr :
  ∀ (hj : ¬IsMax i) (iter : Φ.Iteration i) (hi₁ : i < Order.succ i) (hi₁_2 : i ≤ i),
    arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)))) i
        hi₁ =
      Φ.toSuccArrow
        (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
          (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))

Tactic:
obtain hi₁ | rfl := hi₁.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi₁_1 : i < Order.succ j
hi₁_2 : i ≤ j
hi₁ : i < j
inl :
  arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))
inl₁ :
  arrowMap iter.F i (Order.succ i) ⋯ ⋯ =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))
inl₂ :
  arrowSucc iter.F i hi₁ =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))
inl₃ :
  Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))
inl₄ inl₅ :
  Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) =
    Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ j)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))

Tactic:
rw [arrowSucc_def, arrowMap_extendToSucc _ _ _ _ _ _ (Order.succ_le_of_lt hi₁),
        ← arrowSucc_def _ _ hi₁, iter.arrowSucc_eq i hi₁,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i hi₁.le]

Premises used: CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_eq, Order.succ_le_of_lt, CategoryTheory.SmallObject.SuccStruct.Iteration.F, LT.lt.le, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowSucc_eq, CategoryTheory.SmallObject.SuccStruct.arrowSucc_def, CategoryTheory.SmallObject.SuccStruct.toSucc, CategoryTheory.SmallObject.SuccStruct.arrowMap_extendToSucc
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
i : J
hj : ¬IsMax i
iter : Φ.Iteration i
hi₁_1 : i < Order.succ i
hi₁ : i ≤ i
inr :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))
      (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))) =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
inr₁ :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))
      (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))) =
    Arrow.mk (X :=
      obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))
      (Φ.toSucc
        (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
          (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯)))
inr₂ :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))
      (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))) =
    Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))
      (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)))
inr₃ : i ≤ i
inr₄ :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))
      (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))) =
    Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))
      (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)))
inr₅ : i ≤ i
⊢ arrowSucc (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯)))) i
      hi₁_1 =
    Φ.toSuccArrow
      (obj (C := (↑(Set.Iic (Order.succ i)) : Type u))
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) i ⋯))))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ i)) i ⋯))

Tactic:
rw [arrowSucc_extendToSucc, toSuccArrow,
        extendToSucc_obj_eq hj iter.F (Φ.toSucc _) i]

Premises used: CategoryTheory.SmallObject.SuccStruct.toSuccArrow, CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_eq, CategoryTheory.SmallObject.SuccStruct.Iteration.F, CategoryTheory.SmallObject.SuccStruct.arrowSucc_extendToSucc, CategoryTheory.SmallObject.SuccStruct.toSucc
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
⊢ i ≤ j

Tactic:
have hij' := (Order.IsSuccLimit.le_succ_iff hi).1 hij
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
rw :
  arrowι (restrictionLT iter.F hij') hi k hk =
    arrowι
      (restrictionLT
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) hij)
      hi k hk
⊢ arrowMap (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) k i ⋯
      hij =
    arrowι
      (restrictionLT
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) hij)
      hi k hk

Tactic:
rw [arrowMap_extendToSucc _ _ _ _ _ _ hij', arrowMap_limit _ _ hi _ _ hk]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.arrowMap_limit, CategoryTheory.SmallObject.SuccStruct.arrowMap_extendToSucc
-- Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Φ : SuccStruct.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
inst_5 : HasIterationOfShape.{u, v_1, u_1} J C
j : J
hj : ¬IsMax j
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ Order.succ j
k : J
hk : k < i
hij' : i ≤ j
e_F :
  restrictionLT iter.F hij' =
    restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
      hij
⊢ arrowι (restrictionLT iter.F hij') hi k hk =
    arrowι
      (restrictionLT
        (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))) hij)
      hi k hk

Tactic:
congr 1