awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (X := obj I κ f) (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
⊢ (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts f
have this : HasLiftingProperty (X := obj I κ f) f (πObj I κ f)
Tactic: have := hf _ (rlp_πObj I κ f)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (X := obj I κ f) (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
this : HasLiftingProperty (X := obj I κ f) f (πObj I κ f)
⊢ (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts f
have refine : RetractArrow (W := obj I κ f) f (ιObj I κ f)
Tactic: refine ⟨_, _, _, ?_, transfiniteCompositionsOfShape_ιObj I κ f⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
inst_1 : I.IsCardinalForSmallObjectArgument Cardinal.aleph0
e : ℕ ≃o Cardinal.aleph0.ord.ToType := OrderIso.trans (OrderIso.symm ULift.orderIso.{w, 0}) (OrderIso.ofRelIsoLT ⋯.some)
⊢ I.rlp.llp = ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape ℕ).retracts
have rw : (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts Cardinal.aleph0.ord.ToType).retracts =
  ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape ℕ).retracts
Tactic: rw [SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument' _ Cardinal.aleph0,
    MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso _ e]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
inst_1 : I.IsCardinalForSmallObjectArgument Cardinal.aleph0
e : ℕ ≃o Cardinal.aleph0.ord.ToType := OrderIso.trans (OrderIso.symm ULift.orderIso.{w, 0}) (OrderIso.ofRelIsoLT ⋯.some)
rw :
  (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts Cardinal.aleph0.ord.ToType).retracts =
    ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape ℕ).retracts
⊢ I.rlp.llp = ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape ℕ).retracts
have rw₁ : (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts Cardinal.aleph0.ord.ToType).retracts =
  (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts Cardinal.aleph0.ord.ToType).retracts
Tactic: rw [SmallObject.llp_rlp_of_isCardinalForSmallObjectArgument' _ Cardinal.aleph0,
    MorphismProperty.transfiniteCompositionsOfShape_eq_of_orderIso _ e]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp = (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts
have refine : I.rlp.llp ≤ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts
Tactic: refine le_antisymm ?_
    (retracts_transfiniteComposition_pushouts_coproducts_le_llp_rlp I)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp ≤ (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts
have rw : (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts ≤
  (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts
Tactic: rw [llp_rlp_of_isCardinalForSmallObjectArgument' I κ]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : OrderBot κ.ord.ToType
inst_3 : I.IsCardinalForSmallObjectArgument κ
⊢ (transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType).retracts ≤
    (transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts).retracts
have a : transfiniteCompositionsOfShape.{w, v, u} (coproducts.{w, v, u} I).pushouts κ.ord.ToType ≤
  transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} I).pushouts
Tactic: apply retracts_monotone
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Φ.prop f ↔ Arrow.mk f = Φ.toSuccArrow X
have mp : Φ.prop f → Arrow.mk f = Φ.toSuccArrow X
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
mp : Φ.prop f → Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.prop f ↔ Arrow.mk f = Φ.toSuccArrow X
have mpr : Arrow.mk f = Φ.toSuccArrow X → Φ.prop f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.prop f
have mpr : Φ.toSuccArrow X ∈ Φ.prop.toSet
Tactic: rw [← Φ.prop.arrow_mk_mem_toSet_iff, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
⊢ Φ.succ X = Y
have mk : Φ.succ X = Φ.succ X
Tactic: cases hf
Cleared hypotheses: Y, f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
Φ : SuccStruct.{v, u} C
X Y : C
f : X ⟶ Y
hf : Φ.prop f
⊢ f = Φ.toSucc X ≫ eqToHom ⋯
have mk : Φ.toSucc X = Φ.toSucc X ≫ eqToHom sorry
Tactic: cases hf
Cleared hypotheses: Y, f, hf
-- 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
iter : Φ.Iteration j
i : J
hi : i < j
⊢ Φ.prop (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) (Y :=
    iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) ⋯)) (iter.F.map (homOfLE ⋯))
have rw : Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)) (Y :=
    iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) sorry)) (iter.F.map (homOfLE sorry)) =
  Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
Tactic: rw [prop_iff, ← arrowMap, ← arrowSucc_def _ _ hi, iter.arrowSucc_eq]
-- 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
iter : Φ.Iteration j
i : J
hi : i < j
rw :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) (Y :=
      iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) ⋯)) (iter.F.map (homOfLE ⋯)) =
    Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
⊢ Φ.prop (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) (Y :=
    iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) ⋯)) (iter.F.map (homOfLE ⋯))
have rw₁ : arrowMap iter.F i (Order.succ i) sorry sorry = Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
Tactic: rw [prop_iff, ← arrowMap, ← arrowSucc_def _ _ hi, iter.arrowSucc_eq]
-- 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
iter : Φ.Iteration j
i : J
hi : i < j
rw :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) (Y :=
      iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) ⋯)) (iter.F.map (homOfLE ⋯)) =
    Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₁ :
  arrowMap iter.F i (Order.succ i) ⋯ ⋯ = Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
⊢ Φ.prop (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) (Y :=
    iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) ⋯)) (iter.F.map (homOfLE ⋯))
have rw₂ : arrowSucc iter.F i hi = Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
Tactic: rw [prop_iff, ← arrowMap, ← arrowSucc_def _ _ hi, iter.arrowSucc_eq]
-- 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
iter : Φ.Iteration j
i : J
hi : i < j
rw :
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) (Y :=
      iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) ⋯)) (iter.F.map (homOfLE ⋯)) =
    Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₁ :
  arrowMap iter.F i (Order.succ i) ⋯ ⋯ = Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
rw₂ : arrowSucc iter.F i hi = Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯))
⊢ Φ.prop (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i ⋯)) (Y :=
    iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) (Order.succ i) ⋯)) (iter.F.map (homOfLE ⋯))
have rw₃ : Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry)) =
  Φ.toSuccArrow (iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i sorry))
Tactic: rw [prop_iff, ← arrowMap, ← arrowSucc_def _ _ hi, iter.arrowSucc_eq]
-- 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
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio i) : Type w) C := ⋯
⊢ IsColimit (coconeOfLE iter.F hij)
have refine : ∀ (j_1 : (↑(Set.Iio i) : Type w)),
  (colimit.cocone (restrictionLT iter.F hij)).ι.app j_1 ≫ Iso.hom (eqToIso sorry) = (coconeOfLE iter.F hij).ι.app j_1
Tactic: refine IsColimit.ofIsoColimit (colimit.isColimit (restrictionLT iter.F hij))
    (Cocone.ext (eqToIso (iter.obj_limit i hi hij).symm) ?_)
-- 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
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio i) : Type w) C := ⋯
k : J
hk : k ∈ Set.Iio i
⊢ Eq (α :=
    (restrictionLT iter.F hij).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ⟶ (coconeOfLE iter.F hij).pt)
    ((colimit.cocone (restrictionLT iter.F hij)).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫
      Iso.hom (eqToIso ⋯))
    ((coconeOfLE iter.F hij).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
have a : Arrow.mk (X := (restrictionLT iter.F hij).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
    ((colimit.cocone (restrictionLT iter.F hij)).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫
      Iso.hom (eqToIso sorry)) =
  Arrow.mk (X := (restrictionLT iter.F hij).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
    ((coconeOfLE iter.F hij).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
Tactic: apply Arrow.mk_injective
-- 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
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio i) : Type w) C := ⋯
k : J
hk : k ∈ Set.Iio i
⊢ Arrow.mk (X := (restrictionLT iter.F hij).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      ((colimit.cocone (restrictionLT iter.F hij)).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫
        Iso.hom (eqToIso ⋯)) =
    Arrow.mk (X := (restrictionLT iter.F hij).obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
      ((coconeOfLE iter.F hij).ι.app (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk))
have a : Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k sorry))
    (colimit.ι (restrictionLT iter.F hij) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫ eqToHom sorry :
      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) i hij)) =
  Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k sorry)) (Y :=
    iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hij)) (iter.F.map (homOfLE sorry))
Tactic: dsimp
-- 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
iter : Φ.Iteration j
i : J
hi : Order.IsSuccLimit i
hij : i ≤ j
this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio i) : Type w) C := ⋯
k : J
hk : k ∈ Set.Iio i
⊢ Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯))
      (colimit.ι (restrictionLT iter.F hij) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫ eqToHom ⋯ :
        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) i hij)) =
    Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k ⋯)) (Y :=
      iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) i hij)) (iter.F.map (homOfLE ⋯))
have a : Arrow.mk (X := iter.F.obj (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iic j) k sorry))
    (colimit.ι (restrictionLT iter.F hij) (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk) ≫ eqToHom sorry :
      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) i hij)) =
  arrowMap iter.F
    (↑(((Set.principalSegIioIicOfLE hij).toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s :=
              fun (x1 x2 : (↑(Set.Iic j) : Type w)) ↦ x1 < x2) :
            (a : (↑(Set.Iio i) : Type w)) → (↑(Set.Iic j) : Type w))
          (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio i) k hk)) :
      J)
    (↑((Set.principalSegIioIicOfLE hij).top (r := fun (x1 x2 : (↑(Set.Iio i) : Type w)) ↦ x1 < x2) (s :=
          fun (x1 x2 : (↑(Set.Iic j) : Type w)) ↦ x1 < x2)) :
      J)
    sorry hij
Tactic: rw [← arrowMap]
-- 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
K : Type w
inst_6 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯)
have rw : G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ sorry) =
  G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ sorry)
Tactic: rw [h.src]
-- 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
K : Type w
inst_6 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)
have rw : G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
  G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)
Tactic: rw [h.tgt]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
⊢ F.map (homOfLE h₁₂) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯
have this : ∃ (hX :
  F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ sorry) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ sorry))
  (hY :
  F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)),
  F.map (homOfLE h₁₂) = eqToHom hX ≫ G.map (homOfLE h₁₂) ≫ eqToHom sorry
Tactic: have := (Arrow.mk_eq_mk_iff _ _).1 h
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k₁ k₂ : K
h₁₂ : k₁ ≤ k₂
h₂ : k₂ ≤ x
h : MapEq F G k₁ k₂ h₁₂ h₂
this :
  ∃ (hX :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ ⋯))
    (hY :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)),
    F.map (homOfLE h₁₂) = eqToHom hX ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯
⊢ F.map (homOfLE h₁₂) = eqToHom ⋯ ≫ G.map (homOfLE h₁₂) ≫ eqToHom ⋯
have tauto : ∀
  (w :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ sorry) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₁ sorry))
  (w_1 :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k₂ h₂)),
  F.map (homOfLE h₁₂) = eqToHom w ≫ G.map (homOfLE h₁₂) ≫ eqToHom sorry →
    F.map (homOfLE h₁₂) = eqToHom sorry ≫ G.map (homOfLE h₁₂) ≫ eqToHom sorry
Tactic: tauto
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k : K
hk : k ≤ x
h :
  F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk)
⊢ MapEq F G k k ⋯ hk
have rw : arrowMap F k k sorry hk = arrowMap G k k sorry hk
Tactic: rw [MapEq, arrowMap_refl, arrowMap_refl, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k : K
hk : k ≤ x
h :
  F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk)
rw : arrowMap F k k ⋯ hk = arrowMap G k k ⋯ hk
⊢ MapEq F G k k ⋯ hk
have rw₁ : Arrow.mk (𝟙 (F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))) = arrowMap G k k sorry hk
Tactic: rw [MapEq, arrowMap_refl, arrowMap_refl, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k : K
hk : k ≤ x
h :
  F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk)
rw : arrowMap F k k ⋯ hk = arrowMap G k k ⋯ hk
rw₁ : Arrow.mk (𝟙 (F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))) = arrowMap G k k ⋯ hk
⊢ MapEq F G k k ⋯ hk
have rw₂ : Eq (α := Arrow.{v, u} C) (Arrow.mk (𝟙 (F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))))
  (Arrow.mk (𝟙 (G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))))
Tactic: rw [MapEq, arrowMap_refl, arrowMap_refl, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
k : K
hk : k ≤ x
h :
  F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk)
rw : arrowMap F k k ⋯ hk = arrowMap G k k ⋯ hk
rw₁ : Arrow.mk (𝟙 (F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))) = arrowMap G k k ⋯ hk
rw₂ :
  Eq (α := Arrow.{v, u} C) (Arrow.mk (𝟙 (F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))))
    (Arrow.mk (𝟙 (G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))))
⊢ MapEq F G k k ⋯ hk
have rw₃ : Eq (α := Arrow.{v, u} C) (Arrow.mk (𝟙 (G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))))
  (Arrow.mk (𝟙 (G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) k hk))))
Tactic: rw [MapEq, arrowMap_refl, arrowMap_refl, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ MapEq F G i₁ i₃ ⋯ h₃
have simp : ∃ (hX :
  F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₁ sorry) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₁ sorry))
  (hY :
  F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₃ h₃) =
    G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₃ h₃)),
  F.map (homOfLE sorry) = eqToHom hX ≫ G.map (homOfLE sorry) ≫ eqToHom sorry
Tactic: simp only [MapEq, arrowMap, Arrow.mk_eq_mk_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.Iteration.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Type w
inst_1 : LinearOrder K
x : K
F G : Functor.{w, v, w, u} (↑(Set.Iic x) : Type w) C
i₁ i₂ i₃ : K
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h₃ : i₃ ≤ x
m₁₂ : MapEq F G i₁ i₂ h₁₂ ⋯
m₂₃ : MapEq F G i₂ i₃ h₂₃ h₃
⊢ ∃ (hX :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₁ ⋯) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₁ ⋯))
    (hY :
    F.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₃ h₃) =
      G.obj (Subtype.mk (p := fun (x_1 : K) ↦ x_1 ∈ Set.Iic x) i₃ h₃)),
    F.map (homOfLE ⋯) = eqToHom hX ≫ G.map (homOfLE ⋯) ≫ eqToHom ⋯
have refine : F.map (homOfLE sorry) = eqToHom sorry ≫ G.map (homOfLE sorry) ≫ eqToHom sorry
Tactic: refine ⟨m₁₂.src, m₂₃.tgt, ?_⟩