awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 neg : ∀ (hi : Order.succ j ≤ Order.succ j) (h₁ : ¬Order.succ j ≤ j),
  Eq.{v_1 + 1} (α :=
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry) ⟶
      obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) hi))
    (if h₁ : Order.succ j ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) sorry))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) sorry)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) sorry)) ≫
          Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁)))
    else
      if h₂ : Order.succ j ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) 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)) (Order.succ j) sorry)))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry)))
Tactic: obtain rfl : i = Order.succ j := le_antisymm hi (Order.succ_le_of_lt (not_le.1 h₁))
Cleared hypotheses: i, hi, 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
hi : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
⊢ Eq.{v_1 + 1} (α :=
    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)) (Order.succ j) hi))
    (if h₁ : Order.succ j ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) ⋯))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) ⋯)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) ⋯)) ≫
          Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁)))
    else
      if h₂ : Order.succ j ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) 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)) (Order.succ j) ⋯)))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯)))
have neg : Eq.{v_1 + 1} (α :=
  obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry) ⟶
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) hi))
  (if h₂ : Order.succ j ≤ j then
    Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) 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)) (Order.succ j) sorry)))
  (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry)))
Tactic: rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
      dif_neg 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
hi : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
neg :
  Eq.{v_1 + 1} (α :=
    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)) (Order.succ j) hi))
    (if h₂ : Order.succ j ≤ j then
      Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) 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)) (Order.succ j) ⋯)))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯)))
⊢ Eq.{v_1 + 1} (α :=
    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)) (Order.succ j) hi))
    (if h₁ : Order.succ j ≤ j then
      CategoryStruct.comp (Y := F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) ⋯))
        (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) ⋯)))
        (F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) ⋯)) ≫
          Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) h₁)))
    else
      if h₂ : Order.succ j ≤ j then
        Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) 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)) (Order.succ j) ⋯)))
    (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯)))
have neg₁ : Eq.{v_1 + 1} (α :=
  obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry) ⟶
    obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) hi))
  (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry)))
  (𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry)))
Tactic: rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj),
      dif_neg 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₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h
have pos : ∀ (h₁ : i₃ ≤ j), map hj F τ i₁ i₃ sorry h = map hj F τ i₁ i₂ h₁₂ sorry ≫ map hj F τ i₂ i₃ h₂₃ h
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₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
pos : ∀ (h₁ : i₃ ≤ j), map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h
have neg : ∀ (h₁ : ¬i₃ ≤ j), map hj F τ i₁ i₃ sorry h = map hj F τ i₁ i₂ h₁₂ sorry ≫ map hj F τ i₂ i₃ h₂₃ h
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₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : i₃ ≤ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h
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₃ h))
  (map hj F τ i₁ i₃ sorry 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₃ h))
  ((Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫
        F.map (homOfLE h₁₂) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ sorry))) ≫
      map hj F τ i₂ i₃ h₂₃ 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₃ h))
Tactic: rw [map_eq hj F τ i₁ i₂ _ (h₂₃.trans h₁), map_eq hj F τ i₂ i₃ _ h₁,
      map_eq hj F τ i₁ i₃ _ h₁, assoc, assoc, Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc,
      homOfLE_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₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : 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₃ h))
    (map hj F τ i₁ 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₃ h))
    ((Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
          F.map (homOfLE h₁₂) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ ⋯))) ≫
        map hj F τ i₂ i₃ h₂₃ 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₃ h))
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h
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₃ h))
  (map hj F τ i₁ i₃ sorry 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₃ h))
  (CategoryStruct.comp (Y := obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ sorry))
      (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫
        F.map (homOfLE h₁₂) ≫ Iso.inv (objIso F X (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 (homOfLE h₂₃) ≫ 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₃ h))
Tactic: rw [map_eq hj F τ i₁ i₂ _ (h₂₃.trans h₁), map_eq hj F τ i₂ i₃ _ h₁,
      map_eq hj F τ i₁ i₃ _ h₁, assoc, assoc, Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc,
      homOfLE_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₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : ¬i₃ ≤ j
⊢ map hj F τ i₁ i₃ ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ i₃ h₂₃ h
have neg : ∀ (h₂₃ : i₂ ≤ Order.succ j) (h : Order.succ j ≤ Order.succ j) (h₁ : ¬Order.succ j ≤ j),
  map hj F τ i₁ (Order.succ j) sorry h = map hj F τ i₁ i₂ h₁₂ sorry ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
Tactic: obtain rfl : i₃ = Order.succ j := le_antisymm h (Order.succ_le_of_lt (not_le.1 h₁))
Cleared hypotheses: i₃, h₂₃, h, 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
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
have neg : ∀ (h₂ : i₂ < Order.succ j),
  map hj F τ i₁ (Order.succ j) sorry h = map hj F τ i₁ i₂ h₁₂ sorry ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
Tactic: obtain h₂ | rfl := h₂₃.lt_or_eq
-- 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
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
neg :
  ∀ (h₂ : i₂ < Order.succ j),
    map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
have neg₁ : ∀ (h₁₂ : i₁ ≤ Order.succ j) (h₂₃ : Order.succ j ≤ Order.succ j),
  map hj F τ i₁ (Order.succ j) sorry h = map hj F τ i₁ (Order.succ j) h₁₂ sorry ≫ map hj F τ (Order.succ j) (Order.succ j) h₂₃ h
Tactic: obtain h₂ | rfl := h₂₃.lt_or_eq
Cleared hypotheses: i₂, h₁₂, h₂₃
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc (hypothesis)
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
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ < Order.succ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
have h₃ : i₂ ≤ j
Tactic: rw [Order.lt_succ_iff_of_not_isMax hj] at h₂
Cleared hypotheses: 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
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ i₂ h₁₂ ⋯ ≫ map hj F τ i₂ (Order.succ j) h₂₃ h
have neg : map hj F τ i₁ (Order.succ j) sorry h =
  (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫
      F.map (homOfLE h₁₂) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ h₂))) ≫
    map hj F τ i₂ (Order.succ j) h₂₃ h
Tactic: rw [map_eq hj F τ i₁ i₂ _ 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
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ Order.succ j
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₂ : i₂ ≤ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h =
    (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
        F.map (homOfLE h₁₂) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ h₂))) ≫
      map hj F τ i₂ (Order.succ j) h₂₃ h
have neg : 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)) (Order.succ j) h))
  (if h₁ : Order.succ j ≤ j then
    Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫
      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₂ : 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) ≫
              𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))
    else eqToHom sorry)
  (CategoryStruct.comp (Y := obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ sorry))
    (Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫
      F.map (homOfLE h₁₂) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ h₂)))
    (if h₁ : Order.succ j ≤ j then
      Iso.hom (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ sorry)) ≫
        F.map (homOfLE h₂₃) ≫ Iso.inv (objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ j) 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) ≫
                𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))
      else eqToHom 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
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₁₂ : i₁ ≤ Order.succ j
h₂₃ : Order.succ j ≤ Order.succ j
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ (Order.succ j) h₁₂ ⋯ ≫ map hj F τ (Order.succ j) (Order.succ j) h₂₃ h
have neg : map hj F τ i₁ (Order.succ j) sorry h =
  map hj F τ i₁ (Order.succ j) h₁₂ sorry ≫
    𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) sorry))
Tactic: rw [map_id, comp_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
h : Order.succ j ≤ Order.succ j
h₁ : ¬Order.succ j ≤ j
h₁₂ : i₁ ≤ Order.succ j
h₂₃ : Order.succ j ≤ Order.succ j
neg :
  map hj F τ i₁ (Order.succ j) ⋯ h =
    map hj F τ i₁ (Order.succ j) h₁₂ ⋯ ≫
      𝟙 (obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) (Order.succ j) ⋯))
⊢ map hj F τ i₁ (Order.succ j) ⋯ h = map hj F τ i₁ (Order.succ j) h₁₂ ⋯ ≫ map hj F τ (Order.succ j) (Order.succ j) h₂₃ h
have neg₁ : map hj F τ i₁ (Order.succ j) sorry h = map hj F τ i₁ (Order.succ j) h₁₂ sorry
Tactic: rw [map_id, comp_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₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ Functor.map (extendToSucc hj F τ) (homOfLE hi) ≫ Iso.hom (extendToSuccObjIso hj F τ i₂ hi₂) =
    Iso.hom (extendToSuccObjIso hj F τ i₁ ⋯) ≫ F.map (homOfLE hi)
have dsimp : Eq (α :=
  extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ sorry) ⟶
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
  (CategoryStruct.comp (Y := extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ sorry))
      (extendToSucc.map hj F τ i₁ i₂ sorry sorry)
      (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))) :
    extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ sorry) ⟶
      F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
  (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫ F.map (homOfLE hi) :
    extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ sorry) ⟶
      F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
Tactic: dsimp [extendToSucc, extendToSuccObjIso]
-- 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₂ ≤ j
⊢ Eq (α :=
    extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
      F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
    (CategoryStruct.comp (Y := extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
        (extendToSucc.map hj F τ i₁ i₂ ⋯ ⋯)
        (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))) :
      extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
        F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
    (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫ F.map (homOfLE hi) :
      extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ ⋯) ⟶
        F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
have rw : Eq (α :=
  extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ sorry) ⟶
    F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))
  (CategoryStruct.comp (Y := extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ sorry))
    (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫
      F.map (homOfLE sorry) ≫ Iso.inv (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂)))
    (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₂ hi₂))))
  (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫ F.map (homOfLE hi))
Tactic: rw [extendToSucc.map_eq _ _ _ _ _ _ hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]