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₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
rw :
  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₂ ⋯))
      (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ ⋯)) ≫
        F.map (homOfLE ⋯) ≫ 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₁ ⋯)) ≫ F.map (homOfLE hi))
⊢ 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₂))
  (Iso.hom (extendToSucc.objIso F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i₁ sorry)) ≫
    CategoryStruct.comp (Y := extendToSucc.obj F X (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ 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]
-- 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₁ ⋯) ≫ F.map (homOfLE hi) ≫ Iso.inv (extendToSuccObjIso hj F τ i₂ hi₂)
have rw : Functor.map (extendToSucc hj F τ) (homOfLE hi) =
  Functor.map (extendToSucc hj F τ) (homOfLE hi) ≫
    Iso.hom (extendToSuccObjIso hj F τ i₂ hi₂) ≫ Iso.inv (extendToSuccObjIso hj F τ i₂ hi₂)
Tactic: rw [← extendToSuccObjIso_hom_naturality_assoc, Iso.hom_inv_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
rw :
  Functor.map (extendToSucc hj F τ) (homOfLE hi) =
    Functor.map (extendToSucc hj F τ) (homOfLE hi) ≫
      Iso.hom (extendToSuccObjIso hj F τ i₂ hi₂) ≫ Iso.inv (extendToSuccObjIso hj F τ i₂ hi₂)
⊢ Functor.map (extendToSucc hj F τ) (homOfLE hi) =
    Iso.hom (extendToSuccObjIso hj F τ i₁ ⋯) ≫ F.map (homOfLE hi) ≫ Iso.inv (extendToSuccObjIso hj F τ i₂ hi₂)
have rw₁ : Functor.map (extendToSucc hj F τ) (homOfLE hi) =
  Functor.map (extendToSucc hj F τ) (homOfLE hi) ≫
    𝟙
      (Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ sorry))
Tactic: rw [← extendToSuccObjIso_hom_naturality_assoc, Iso.hom_inv_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
rw :
  Functor.map (extendToSucc hj F τ) (homOfLE hi) =
    Functor.map (extendToSucc hj F τ) (homOfLE hi) ≫
      Iso.hom (extendToSuccObjIso hj F τ i₂ hi₂) ≫ Iso.inv (extendToSuccObjIso hj F τ i₂ hi₂)
rw₁ :
  Functor.map (extendToSucc hj F τ) (homOfLE hi) =
    Functor.map (extendToSucc hj F τ) (homOfLE hi) ≫
      𝟙
        (Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ ⋯))
⊢ Functor.map (extendToSucc hj F τ) (homOfLE hi) =
    Iso.hom (extendToSuccObjIso hj F τ i₁ ⋯) ≫ F.map (homOfLE hi) ≫ Iso.inv (extendToSuccObjIso hj F τ i₂ hi₂)
have rw₂ : Eq (α :=
  Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₁ sorry) ⟶
    Functor.obj (C := (↑(Set.Iic (Order.succ j)) : Type u)) (extendToSucc hj F τ)
      (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic (Order.succ j)) i₂ sorry))
  (Functor.map (extendToSucc hj F τ) (homOfLE hi)) (Functor.map (extendToSucc hj F τ) (homOfLE hi))
Tactic: rw [← extendToSuccObjIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
h₂ : ¬i₂ < j
h₂' : i₂ = j
h₁ : i₁ < j
⊢ obj c j = obj c i₂
have subst : ∀ {F : Functor.{u, v_1, u, u_1} (↑(Set.Iio i₂) : Type u) C} (c : Cocone F) (hi₂ : i₂ ≤ i₂) (h₂ : ¬i₂ < i₂)
  (h₁ : i₁ < i₂), obj c i₂ = obj c i₂
Tactic: subst h₂'
Cleared hypotheses: j, F, c, hi₂, h₂, h₂', h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
h₂ : ¬i₂ < j
h₂' : i₂ = j
h₁ : ¬i₁ < j
h₁' : i₁ = j
⊢ obj c i₁ = obj c i₂
have subst : ∀ (hi : i₂ ≤ i₂) {F : Functor.{u, v_1, u, u_1} (↑(Set.Iio i₂) : Type u) C} (c : Cocone F) (hi₂ : i₂ ≤ i₂)
  (h₂ h₁ : ¬i₂ < i₂), obj c i₂ = obj c i₂
Tactic: subst h₁' h₂'
Cleared hypotheses: j, F, c, i₁, hi, hi₂, h₂, h₂', h₁, h₁'
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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
⊢ map c i i ⋯ hi = 𝟙 (obj c i)
have dsimp : Eq.{v_1 + 1} (α := obj c i ⟶ obj c i)
  (if h₂ : i < j then
    Iso.hom (objIso c i sorry) ≫ F.map (𝟙 (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i sorry)) ≫ (objIso c i h₂).inv
  else
    if h₁ : i < j then
      (objIso c i h₁).hom ≫ c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
    else 𝟙 (obj c i))
  (𝟙 (obj c i))
Tactic: dsimp [map]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃
have inl : ∀ (hi₁₂ : i₁ < i₂), map c i₁ i₃ sorry hi₃ = map c i₁ i₂ hi sorry ≫ map c i₂ i₃ hi' hi₃
Tactic: obtain hi₁₂ | rfl := hi.lt_or_eq
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
inl : ∀ (hi₁₂ : i₁ < i₂), map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃
have inr : ∀ (hi : i₁ ≤ i₁) (hi' : i₁ ≤ i₃), map c i₁ i₃ sorry hi₃ = map c i₁ i₁ hi sorry ≫ map c i₁ i₃ hi' hi₃
Tactic: obtain hi₁₂ | rfl := hi.lt_or_eq
Cleared hypotheses: i₂, hi, hi'
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃
have inl : ∀ (hi₂₃ : i₂ < i₃), map c i₁ i₃ sorry hi₃ = map c i₁ i₂ hi sorry ≫ map c i₂ i₃ hi' hi₃
Tactic: obtain hi₂₃ | rfl := hi'.lt_or_eq
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
inl : ∀ (hi₂₃ : i₂ < i₃), map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃
have inl₁ : ∀ (hi' : i₂ ≤ i₂) (hi₃ : i₂ ≤ j), map c i₁ i₂ sorry hi₃ = map c i₁ i₂ hi sorry ≫ map c i₂ i₂ hi' hi₃
Tactic: obtain hi₂₃ | rfl := hi'.lt_or_eq
Cleared hypotheses: i₃, hi', hi₃
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
⊢ map c i₁ i₃ ⋯ hi₃ = map c i₁ i₂ hi ⋯ ≫ map c i₂ i₃ hi' hi₃
have inl : Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
  (if h₂ : i₃ < j then Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE sorry) ≫ (objIso c i₃ h₂).inv
  else
    if h₁ : i₁ < j then
      (objIso c i₁ h₁).hom ≫
        c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
    else eqToHom sorry)
  (CategoryStruct.comp (Y := obj c i₂)
    (if h₂ : i₂ < j then Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
    else
      if h₁ : i₁ < j then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
      else eqToHom sorry)
    (if h₂ : i₃ < j then Iso.hom (objIso c i₂ sorry) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₂ < j then
        (objIso c i₂ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
      else eqToHom sorry))
Tactic: dsimp [map]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
⊢ Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₂ : i₃ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₁ < j then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < j then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < j then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < j then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯))
have inl : ∀ (hi₃' : i₃ < j),
  Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₂ : i₃ < j then Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE sorry) ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₁ < j then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
      else eqToHom sorry)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < j then Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < j then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
        else eqToHom sorry)
      (if h₂ : i₃ < j then Iso.hom (objIso c i₂ sorry) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < j then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
        else eqToHom sorry))
Tactic: obtain hi₃' | rfl := hi₃.lt_or_eq
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
⊢ Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₂ : i₃ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₁ < j then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < j then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < j then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < j then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯))
have inl : Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE sorry) ≫ (objIso c i₃ hi₃').inv =
  CategoryStruct.comp (Y := obj c i₂)
    (if h₂ : i₂ < j then Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
    else
      if h₁ : i₁ < j then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
      else eqToHom sorry)
    (if h₂ : i₃ < j then Iso.hom (objIso c i₂ sorry) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₂ < j then
        (objIso c i₂ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
      else eqToHom sorry)
Tactic: rw [dif_pos hi₃', dif_pos (hi₂₃.trans hi₃'), dif_pos hi₃', assoc, assoc,
          Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
inl :
  Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < j then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < j then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < j then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
⊢ Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₂ : i₃ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₁ < j then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < j then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < j then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < j then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯))
have inl₁ : Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE sorry) ≫ (objIso c i₃ hi₃').inv =
  (Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE hi) ≫ Iso.inv (objIso c i₂ sorry)) ≫
    if h₂ : i₃ < j then Iso.hom (objIso c i₂ sorry) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₂ < j then
        (objIso c i₂ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom sorry
      else eqToHom sorry
Tactic: rw [dif_pos hi₃', dif_pos (hi₂₃.trans hi₃'), dif_pos hi₃', assoc, assoc,
          Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone (goal)
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₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
inl :
  Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < j then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < j then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < j then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
inl₁ :
  Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    (Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ Iso.inv (objIso c i₂ ⋯)) ≫
      if h₂ : i₃ < j then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < j then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯
⊢ Eq.{v_1 + 1} (α := obj c i₁ ⟶ obj c i₃)
    (if h₂ : i₃ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ h₂).inv
    else
      if h₁ : i₁ < j then
        (objIso c i₁ h₁).hom ≫
          c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯)
    (CategoryStruct.comp (Y := obj c i₂)
      (if h₂ : i₂ < j then Iso.hom (objIso c i₁ ⋯) ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
      else
        if h₁ : i₁ < j then
          (objIso c i₁ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₁ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯)
      (if h₂ : i₃ < j then Iso.hom (objIso c i₂ ⋯) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ h₂).inv
      else
        if h₁ : i₂ < j then
          (objIso c i₂ h₁).hom ≫
            c.ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i₂ h₁) ≫ (objIsoPt c).inv ≫ eqToHom ⋯
        else eqToHom ⋯))
have inl₂ : Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE sorry) ≫ (objIso c i₃ hi₃').inv =
  (Iso.hom (objIso c i₁ sorry) ≫ F.map (homOfLE hi) ≫ Iso.inv (objIso c i₂ sorry)) ≫
    Iso.hom (objIso c i₂ sorry) ≫ F.map (homOfLE hi') ≫ (objIso c i₃ hi₃').inv
Tactic: rw [dif_pos hi₃', dif_pos (hi₂₃.trans hi₃'), dif_pos hi₃', assoc, assoc,
          Iso.inv_hom_id_assoc, ← Functor.map_comp_assoc, homOfLE_comp]