awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ ⦃X Y : (↑(Set.Iio i) : Type u)⦄ (f : X ⟶ Y),
    (restrictionLT iter.F hij').mapArrow.obj (Arrow.mk f) =
      (restrictionLT
              (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
              hij).mapArrow.obj
        (Arrow.mk 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

Tactic:
apply Arrow.functor_ext

Premises used: CategoryTheory.Arrow.functor_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
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
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂
e_F :
  Arrow.mk (iter.F.map (homOfLE ⋯)) =
    Arrow.mk (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)) k₁ ⋯))
      (map (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (homOfLE ⋯))
⊢ (restrictionLT iter.F hij').mapArrow.obj (Arrow.mk f) =
    (restrictionLT (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
            hij).mapArrow.obj
      (Arrow.mk f)

Tactic:
dsimp
-- 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
k₁ : J
h₁ : k₁ ∈ Set.Iio i
k₂ : J
h₂ : k₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂
e_F :
  arrowMap iter.F (↑(⋯.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁)) : J)
      (↑(⋯.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂)) : J) ⋯ ⋯ =
    arrowMap iter.F (↑(⋯.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₁ h₁)) : J)
      (↑(⋯.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂)) : J) ⋯ ⋯
e_F₁ : (↑(⋯.functor.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k₂ h₂)) : J) ≤ j
⊢ Arrow.mk (iter.F.map (homOfLE ⋯)) =
    Arrow.mk (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)) k₁ ⋯))
      (map (extendToSucc hj iter.F (Φ.toSucc (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))))
        (homOfLE ⋯))

Tactic:
rw [← arrowMap, ← arrowMap, arrowMap_extendToSucc]

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowMap, 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : (↑(Set.Iio j) : Type u)
⊢ (↑i : J) ∈ Set.Iic (↑i : J)

Tactic:
simp
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : (↑(Set.Iio j) : Type u)
f : i₁ ⟶ i₂
⊢ (↑i₁ : J) ≤ (↑i₁ : J)

Tactic:
simp
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : (↑(Set.Iio j) : Type u)
f : i₁ ⟶ i₂
⊢ (↑i₂ : J) ≤ (↑i₂ : J)

Tactic:
simp
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
dsimp :
  (ofCocone (colimit.cocone (inductiveSystem iter))).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯) =
    iter'.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k) i hk)
⊢ (functor hj iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯) =
    iter'.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k) i hk)

Tactic:
dsimp only [functor]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
rw :
  (inductiveSystem iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) =
    iter'.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k) i hk)
⊢ (ofCocone (colimit.cocone (inductiveSystem iter))).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯) =
    iter'.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k) i hk)

Tactic:
rw [ofCocone_obj_eq _ _ hi]

Premises used: CategoryTheory.SmallObject.SuccStruct.ofCocone_obj_eq
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
k : J
iter' : Φ.Iteration k
hk : i ≤ k
⊢ (inductiveSystem iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi) =
    iter'.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic k) i hk)

Tactic:
apply congr_obj

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.congr_obj
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂ : i₂ < j
⊢ i₁ ≤ i₁

Tactic:
simp
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂ : i₂ < j
⊢ i₂ ≤ i₂

Tactic:
simp
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i₁ i₂ : J
h₁₂ : i₁ ≤ i₂
h₂ : i₂ < j
⊢ arrowMap (functor hj iter) i₁ i₂ h₁₂ ⋯ =
    Arrow.mk (X := (iter i₁ ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i₁) i₁ ⋯)) (Y :=
      (iter i₂ h₂).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i₂) i₂ ⋯))
      ((iter i₁ ⋯).mapObj (iter i₂ h₂) h₁₂ ⋯ ⋯ h₁₂)

Tactic:
arrowMap_ofCocone _ _ _ _ h₂

Premises used: Set.Mem, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor, CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj, CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
this : HasColimitsOfShape.{u, u, v_1, u_1} (↑(Set.Iio j) : Type u) C := ⋯
⊢ j ≤ j

Tactic:
simp
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ arrowMap (functor hj iter) i j ⋯ ⋯ =
    Arrow.mk (X := (inductiveSystem iter).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi)) (Y :=
      colimit (inductiveSystem iter))
      (colimit.ι (inductiveSystem iter) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hi))

Tactic:
arrowMap_ofCocone_to_top _ _ _

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.functor, CategoryTheory.Limits.colimit, CategoryTheory.SmallObject.SuccStruct.arrowMap_ofCocone_to_top, CategoryTheory.Limits.colimit.ι
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
⊢ LE.le.{u} (α := J) ⊥ ⊥

Tactic:
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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : i < j
⊢ i ≤ i

Tactic:
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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
k : J
hk : k < i
inl : ∀ (hij_1 : i < j), arrowMap (functor hj iter) k i ⋯ hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk
inr :
  ∀ (hj : Order.IsSuccLimit i) (iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1) (hij : i ≤ i),
    arrowMap (functor hj iter) k i ⋯ hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk
⊢ arrowMap (functor hj iter) k i ⋯ hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk

Tactic:
obtain hij | rfl := hij.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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
inl : arrowι (restrictionLT (iter i hij).F ⋯) hi k hk = arrowι (restrictionLT (functor hj iter) hij_1) hi k hk
⊢ arrowMap (functor hj iter) k i ⋯ hij_1 = arrowι (restrictionLT (functor hj iter) hij_1) hi k hk

Tactic:
rw [arrowMap_functor _ _ _ _ _ hij, arrow_mk_mapObj,
        arrowMap_limit _ _ hi _ _ hk]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor, CategoryTheory.SmallObject.SuccStruct.Iteration.arrowMap_limit, CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
inl : restrictionLT (iter i hij).F ⋯ = restrictionLT (functor hj iter) hij_1
⊢ arrowι (restrictionLT (iter i hij).F ⋯) hi k hk = arrowι (restrictionLT (functor hj iter) hij_1) hi k hk

Tactic:
congr 1
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
inl :
  ∀ ⦃X Y : (↑(Set.Iio i) : Type u)⦄ (f : X ⟶ Y),
    (restrictionLT (iter i hij).F ⋯).mapArrow.obj (Arrow.mk f) =
      (restrictionLT (functor hj iter) hij_1).mapArrow.obj (Arrow.mk f)
⊢ restrictionLT (iter i hij).F ⋯ = restrictionLT (functor hj iter) hij_1

Tactic:
apply Arrow.functor_ext

Premises used: CategoryTheory.Arrow.functor_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
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₁ hl₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₂ hl₂
inl :
  Arrow.mk (X := (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ ⋯)) (Y :=
      (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ ⋯))
      ((iter i hij).F.map (homOfLE ⋯) :
        (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ ⋯) ⟶
          (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ ⋯)) =
    Arrow.mk ((functor hj iter).map (homOfLE ⋯))
⊢ (restrictionLT (iter i hij).F ⋯).mapArrow.obj (Arrow.mk f) =
    (restrictionLT (functor hj iter) hij_1).mapArrow.obj (Arrow.mk f)

Tactic:
dsimp
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₁ hl₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₂ hl₂
inl :
  ∀ (pf : l₁ ∈ Set.Iic i) (pf_1 : l₂ ∈ Set.Iic i)
    (pf_2 : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_1)
    (pf_3 : l₁ ∈ Set.Iic j) (pf_4 : l₂ ∈ Set.Iic j)
    (pf_5 :
      Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) l₁ pf_3 ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) l₂ pf_4),
    Arrow.mk ((iter i hij).F.map (homOfLE pf_2)) = Arrow.mk ((functor hj iter).map (homOfLE pf_5))
⊢ Arrow.mk (X := (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ ⋯)) (Y :=
      (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ ⋯))
      ((iter i hij).F.map (homOfLE ⋯) :
        (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ ⋯) ⟶
          (iter i hij).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ ⋯)) =
    Arrow.mk ((functor hj iter).map (homOfLE ⋯))

Tactic:
generalize_proofs
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₁ hl₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₂ hl₂
pf : l₁ ∈ Set.Iic i
pf_1 : l₂ ∈ Set.Iic i
pf_2 : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_1
pf_3 : l₁ ∈ Set.Iic j
pf_4 : l₂ ∈ Set.Iic j
pf_5 : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) l₁ pf_3 ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) l₂ pf_4
inl :
  arrowMap (iter i hij).F (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf) : J)
      (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_1) : J) pf_2 pf_1 =
    arrowMap (iter l₂ ⋯).F l₁ l₂ pf_5 ⋯
⊢ Arrow.mk ((iter i hij).F.map (homOfLE pf_2)) = Arrow.mk ((functor hj iter).map (homOfLE pf_5))

Tactic:
rw [← arrowMap, ← arrowMap, arrowMap_functor hj iter l₁ l₂ _ (hl₂.trans hij),
        arrow_mk_mapObj]

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor, LT.lt.trans, CategoryTheory.SmallObject.SuccStruct.arrowMap, CategoryTheory.SmallObject.SuccStruct.Iteration.arrow_mk_mapObj
-- 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 : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij_1 : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₁ hl₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₂ hl₂
pf : l₁ ∈ Set.Iic i
pf_1 : l₂ ∈ Set.Iic i
pf_2 : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_1
pf_3 : l₁ ∈ Set.Iic j
pf_4 : l₂ ∈ Set.Iic j
pf_5 : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) l₁ pf_3 ≤ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) l₂ pf_4
⊢ arrowMap (iter i hij).F (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₁ pf) : J)
      (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic i) l₂ pf_1) : J) pf_2 pf_1 =
    arrowMap (iter l₂ ⋯).F l₁ l₂ pf_5 ⋯

Tactic:
apply congr_arrowMap

Premises used: CategoryTheory.SmallObject.SuccStruct.Iteration.congr_arrowMap
-- 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
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
inr : arrowι (inductiveSystem iter) hi k hk = arrowι (restrictionLT (functor hj iter) hij) hi k hk
⊢ arrowMap (functor hj iter) k i ⋯ hij = arrowι (restrictionLT (functor hj iter) hij) hi k hk

Tactic:
rw [arrowMap_functor_to_top _ _ _ hk, ← arrowι_def _ hi]

Premises used: CategoryTheory.SmallObject.SuccStruct.arrowι_def, CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.arrowMap_functor_to_top
-- 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
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
inr : inductiveSystem iter = restrictionLT (functor hj iter) hij
⊢ arrowι (inductiveSystem iter) hi k hk = arrowι (restrictionLT (functor hj iter) hij) hi k hk

Tactic:
congr 1
-- 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
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
inr :
  ∀ ⦃X Y : (↑(Set.Iio i) : Type u)⦄ (f : X ⟶ Y),
    (inductiveSystem iter).mapArrow.obj (Arrow.mk f) = (restrictionLT (functor hj iter) hij).mapArrow.obj (Arrow.mk f)
⊢ inductiveSystem iter = restrictionLT (functor hj iter) hij

Tactic:
apply Arrow.functor_ext

Premises used: CategoryTheory.Arrow.functor_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
i : J
hi : Order.IsSuccLimit i
k : J
hk : k < i
hj : Order.IsSuccLimit i
iter : (i_1 : J) → i_1 < i → Φ.Iteration i_1
hij : i ≤ i
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₁ hl₁ ⟶ Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) l₂ hl₂
inr :
  Arrow.mk (X := (iter l₁ ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic l₁) l₁ ⋯)) (Y :=
      (iter l₂ ⋯).F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic l₂) l₂ ⋯))
      ((iter l₁ ⋯).mapObj (iter l₂ ⋯) ⋯ ⋯ ⋯ ⋯) =
    Arrow.mk ((functor hj iter).map (homOfLE ⋯))
⊢ (inductiveSystem iter).mapArrow.obj (Arrow.mk f) = (restrictionLT (functor hj iter) hij).mapArrow.obj (Arrow.mk f)

Tactic:
dsimp