awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
k₁ k₂ : J
h : k₁ ≤ k₂
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
hj : j₁ ≤ j₂
⊢ arrowMap iter₁.F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
have rw : arrowMap (iter₂.trunc hj).F k₁ k₂ h h₁ = arrowMap iter₂.F k₁ k₂ h h₂
Tactic: rw [Subsingleton.elim iter₁ (iter₂.trunc hj)]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
⊢ iter₁.F.map (homOfLE h) = eqToHom ⋯ ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯
have this : ∃ (hX :
  iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₁ sorry) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₁ sorry))
  (hY :
  iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₂ h₁) =
    iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₂ h₂)),
  iter₁.F.map (homOfLE h) = eqToHom hX ≫ iter₂.F.map (homOfLE h) ≫ eqToHom sorry
Tactic: have := (Arrow.mk_eq_mk_iff _ _).1 (congr_arrowMap iter₁ iter₂ h h₁ h₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
Φ : SuccStruct.{v, u} C
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : HasIterationOfShape.{w, v, u} J C
inst_5 : WellFoundedLT J
j₁ j₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h : k₁ ≤ k₂
h₁ : k₂ ≤ j₁
h₂ : k₂ ≤ j₂
this :
  ∃ (hX :
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₁ ⋯) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₁ ⋯))
    (hY :
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₂ h₁) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₂ h₂)),
    iter₁.F.map (homOfLE h) = eqToHom hX ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯
⊢ iter₁.F.map (homOfLE h) = eqToHom ⋯ ≫ iter₂.F.map (homOfLE h) ≫ eqToHom ⋯
have tauto : ∀
  (w :
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₁ sorry) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₁ sorry))
  (w_1 :
    iter₁.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₁) k₂ h₁) =
      iter₂.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j₂) k₂ h₂)),
  iter₁.F.map (homOfLE h) = eqToHom w ≫ iter₂.F.map (homOfLE h) ≫ eqToHom sorry →
    iter₁.F.map (homOfLE h) = eqToHom sorry ≫ iter₂.F.map (homOfLE h) ≫ eqToHom sorry
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ Order.succ j
h₁ : ¬i₂ ≤ j
h₂ : i₁ ≤ j
⊢ obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯) =
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ hi₂)
have e_i : Order.succ j = i₂
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ Order.succ j
h₁ : ¬i₂ ≤ j
h₂ : ¬i₁ ≤ j
⊢ obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) =
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ hi₂)
have e_i : i₁ = i₂
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ Order.succ j
h₁ : ¬i₂ ≤ j
h₂ : ¬i₁ ≤ j
⊢ i₁ = i₂
have e_i : i₁ = Order.succ j
Tactic: rw [le_antisymm hi₂ (Order.succ_le_of_lt (not_le.1 h₁)),
          le_antisymm (hi.trans hi₂) (Order.succ_le_of_lt (not_le.1 h₂))]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ Order.succ j
h₁ : ¬i₂ ≤ j
h₂ : ¬i₁ ≤ j
e_i : i₁ = Order.succ j
⊢ i₁ = i₂
have e_i₁ : Order.succ j = Order.succ j
Tactic: rw [le_antisymm hi₂ (Order.succ_le_of_lt (not_le.1 h₁)),
          le_antisymm (hi.trans hi₂) (Order.succ_le_of_lt (not_le.1 h₂))]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
⊢ Eq (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
    (map hj F τ j (Order.succ j) ⋯ ⋯ :
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯) ⟶
        obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
    (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)) ≫ τ ≫ Iso.inv (objSuccIso hj F X) :
      obj F X
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j))
            (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) : J) ⋯) ⟶
        obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
have dsimp : Eq (α :=
  obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j sorry) ⟶
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))
  (if h₁ : Order.succ j ≤ j then
    CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry))
      (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry)))
      (CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁))
        (F.map (homOfLE sorry)) (Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁))))
  else
    if h₂ : j ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂)) ≫
          τ ≫
            Iso.inv (objSuccIso hj F X) ≫
              𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry)))
    else eqToHom sorry)
  (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry)) ≫ τ ≫ Iso.inv (objSuccIso hj F X))
Tactic: dsimp [map]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
⊢ Eq (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
    (if h₁ : Order.succ j ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))
        (CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁))
          (F.map (homOfLE ⋯)) (Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁))))
    else
      if h₂ : j ≤ j then
        CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂))
          (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂)))
          (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂)) ≫
            τ ≫
              Iso.inv (objSuccIso hj F X) ≫
                𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯)))
      else eqToHom ⋯)
    (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)) ≫ τ ≫ Iso.inv (objSuccIso hj F X))
have rw : Eq (α :=
  obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j sorry) ⟶
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))
  (if h₂ : j ≤ j then
    CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂))
      (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂)))
      (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂)) ≫
        τ ≫
          Iso.inv (objSuccIso hj F X) ≫
            𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry)))
  else eqToHom sorry)
  (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry)) ≫ τ ≫ Iso.inv (objSuccIso hj F X))
Tactic: rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
    dif_pos (by rfl), Functor.map_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
rw :
  Eq (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
    (if h₂ : j ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂)) ≫
          τ ≫
            Iso.inv (objSuccIso hj F X) ≫
              𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯)))
    else eqToHom ⋯)
    (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)) ≫ τ ≫ Iso.inv (objSuccIso hj F X))
⊢ Eq (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
    (if h₁ : Order.succ j ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)))
        (CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁))
          (F.map (homOfLE ⋯)) (Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁))))
    else
      if h₂ : j ≤ j then
        CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂))
          (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂)))
          (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j h₂)) ≫
            τ ≫
              Iso.inv (objSuccIso hj F X) ≫
                𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯)))
      else eqToHom ⋯)
    (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯)) ≫ τ ≫ Iso.inv (objSuccIso hj F X))
have rw₁ : Eq (α :=
  obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) j sorry) ⟶
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))
  (CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry))
    (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry)))
    (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry)) ≫
      τ ≫
        Iso.inv (objSuccIso hj F X) ≫
          𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))))
  (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j sorry)) ≫ τ ≫ Iso.inv (objSuccIso hj F X))
Tactic: rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
    dif_pos (by rfl), Functor.map_id, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i : J
hi : i ≤ Order.succ j
⊢ Eq (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
    (map hj F τ i i ⋯ hi :
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
        obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)) :
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
        obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))
have dsimp : Eq.{v_1 + 1} (α :=
  obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry) ⟶
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
  (if h₁ : i ≤ j then
    CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
      (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)))
      (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)) ≫
        Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁)))
  else
    if h₂ : i ≤ j then
      Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₂)) ≫
        F.map (homOfLE h₂) ≫ τ ≫ Iso.inv (objSuccIso hj F X) ≫ eqToHom sorry
    else 𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry)))
  (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry)))
Tactic: dsimp [map]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i : J
hi : i ≤ Order.succ j
⊢ Eq.{v_1 + 1} (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
    (if h₁ : i ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) ≫
          Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁)))
    else
      if h₂ : i ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₂)) ≫
          F.map (homOfLE h₂) ≫ τ ≫ Iso.inv (objSuccIso hj F X) ≫ eqToHom ⋯
      else 𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)))
have pos : ∀ (h₁ : i ≤ j),
  Eq.{v_1 + 1} (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
    (if h₁ : i ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)) ≫
          Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁)))
    else
      if h₂ : i ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₂)) ≫
          F.map (homOfLE h₂) ≫ τ ≫ Iso.inv (objSuccIso hj F X) ≫ eqToHom sorry
      else 𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry)))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry)))
Tactic: by_cases h₁ : i ≤ j
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i : J
hi : i ≤ Order.succ j
h₁ : i ≤ j
⊢ Eq.{v_1 + 1} (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
    (if h₁ : i ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) ≫
          Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁)))
    else
      if h₂ : i ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₂)) ≫
          F.map (homOfLE h₂) ≫ τ ≫ Iso.inv (objSuccIso hj F X) ≫ eqToHom ⋯
      else 𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)))
have pos : Eq (α :=
  obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry) ⟶
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
  (CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
      (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)))
      (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)) ≫
        Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁))) :
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
  (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry)) :
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry))
Tactic: rw [dif_pos h₁, CategoryTheory.Functor.map_id, id_comp, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : Type u
inst_1 : LinearOrder J
inst_2 : SuccOrder J
j : J
hj : ¬IsMax j
F : Functor.{u, v_1, u, u_1} (↑(Set.Iic j) : Type u) C
X : C
τ : F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) j ⋯) ⟶ X
i : J
hi : i ≤ Order.succ j
h₁ : i ≤ j
pos :
  Eq (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
    (CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) ≫
          Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁))) :
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
        obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)) :
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
        obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯))
⊢ Eq.{v_1 + 1} (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i hi))
    (if h₁ : i ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) ≫
          Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁)))
    else
      if h₂ : i ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₂)) ≫
          F.map (homOfLE h₂) ≫ τ ≫ Iso.inv (objSuccIso hj F X) ≫ eqToHom ⋯
      else 𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i ⋯)))
have pos₁ : Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)) ≫
    𝟙 (F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)) ≫
      Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i h₁)) =
  𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i sorry))
Tactic: rw [dif_pos h₁, CategoryTheory.Functor.map_id, id_comp, Iso.hom_inv_id]