awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g_1 : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g_1)) :
    Type (max v w))
i i' : (↑(Set.Iio j) : Type w)
g : i ⟶ i'
⊢ Eq (α :=
    Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          F)
        i ⟶
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (↑(Set.Iio j) : Type w)) X) i')
    (Functor.map
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          F)
        g ≫
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i')).f')
    (((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i)).f' ≫
      Functor.map (Functor.obj (Functor.const (↑(Set.Iio j) : Type w)) X) g)
have this : SqStruct.f' (c := c) (Y := Y) (p := p) (f := f) (g := g_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map
            (Functor.op
                (Monotone.functor (f :=
                  (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) sorry) ⋙
              sqFunctor c p f g_1)
            g.op) :
        (a : (fun (X : Type v) ↦ X) ((sorry.functor.op ⋙ sqFunctor c p f g_1).obj (Opposite.op i'))) →
          (fun (X : Type v) ↦ X) ((sorry.functor.op ⋙ sqFunctor c p f g_1).obj (Opposite.op i)))
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (sorry.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i'))) =
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (sorry.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i)).f'
Tactic: have := congr_arg SqStruct.f' (s.2 g.op)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g_1 : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g_1)) :
    Type (max v w))
i i' : (↑(Set.Iio j) : Type w)
g : i ⟶ i'
this :
  SqStruct.f' (c := c) (Y := Y) (p := p) (f := f) (g := g_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Functor.map
              (Functor.op
                  (Monotone.functor (f :=
                    (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
                sqFunctor c p f g_1)
              g.op) :
          (a : (fun (X : Type v) ↦ X) ((⋯.functor.op ⋙ sqFunctor c p f g_1).obj (Opposite.op i'))) →
            (fun (X : Type v) ↦ X) ((⋯.functor.op ⋙ sqFunctor c p f g_1).obj (Opposite.op i)))
        ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i'))) =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i)).f'
⊢ Eq (α :=
    Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          F)
        i ⟶
      Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (↑(Set.Iio j) : Type w)) X) i')
    (Functor.map
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          F)
        g ≫
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i')).f')
    (((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g_1).obj j_1) (Opposite.op i)).f' ≫
      Functor.map (Functor.obj (Functor.const (↑(Set.Iio j) : Type w)) X) g)
have dsimp : F.map
      (Functor.map
        (Monotone.functor (f :=
          (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
                x1 < x2) (Set.principalSegIio j)) :
            (a : (↑(Set.Iio j) : Type w)) → J))
          sorry)
        g) ≫
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i')).f' =
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' ≫ 𝟙 X
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g_1 : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g_1)) :
    Type (max v w))
i i' : (↑(Set.Iio j) : Type w)
g : i ⟶ i'
this :
  F.map (Functor.map (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) g) ≫
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J))
          (Opposite.op i')).f' =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f'
⊢ F.map
        (Functor.map
          (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯)
          g) ≫
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J))
          (Opposite.op i')).f' =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' ≫
      𝟙 X
have rw : ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' =
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' ≫ 𝟙 X
Tactic: rw [this, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g_1 : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g_1)) :
    Type (max v w))
i i' : (↑(Set.Iio j) : Type w)
g : i ⟶ i'
this :
  F.map (Functor.map (Monotone.functor (f := Subtype.val (p := fun (x : J) ↦ x ∈ Set.Iio j)) ⋯) g) ≫
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J))
          (Opposite.op i')).f' =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f'
rw :
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' ≫
      𝟙 X
⊢ F.map
        (Functor.map
          (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯)
          g) ≫
      ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J))
          (Opposite.op i')).f' =
    ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' ≫
      𝟙 X
have rw₁ : ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f' =
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g_1 (↑(Opposite.unop j_1) : J)) (Opposite.op i)).f'
Tactic: rw [this, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
⊢ F.map (homOfLE ⋯) ≫ liftHom hj s = f
have h : ⊥ < j
Tactic: have h : ⊥ < j := Ne.bot_lt' (by
      rintro rfl
      exact Order.not_isSuccLimit_bot hj)
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
h : ⊥ < j
⊢ F.map (homOfLE ⋯) ≫ liftHom hj s = f
have rw : ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (sorry.functor.op ⋙ sqFunctor c p f g).obj j_1)
      (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) ⊥ h))).f' =
  f
Tactic: rw [liftHom_fac hj s ⊥ h]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
x : (↑(Set.Iio j) : Type w)
i : J
hij : i ∈ Set.Iio j
⊢ Eq (α :=
    Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          F)
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij) ⟶
      Y)
    (NatTrans.app (Cocone.ι (PrincipalSeg.cocone (Set.principalSegIio j) F))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij) ≫
      liftHom hj s ≫ p)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u}
        (Functor.obj (Functor.const (↑(Set.Iio j) : Type w))
          (Cocone.pt (J := (↑(Set.Iio j) : Type w)) (F :=
            Monotone.functor (f :=
                (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                      fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
                  (a : (↑(Set.Iio j) : Type w)) → J))
                ⋯ ⋙
              F)
            (PrincipalSeg.cocone (Set.principalSegIio j) F)))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))
      (NatTrans.app (Cocone.ι (PrincipalSeg.cocone (Set.principalSegIio j) F))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))
      (c.ι.app (Opposite.unop (Opposite.op j)) ≫ g))
have this : ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (sorry.functor.op ⋙ sqFunctor c p f g).obj j_1)
        (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))).f' ≫
    p =
  c.ι.app
      (Opposite.unop
        (Functor.obj
          (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) sorry))
          (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij)))) ≫
    g
Tactic: have := (s.1 ⟨i, hij⟩).w₂
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
x : (↑(Set.Iio j) : Type w)
i : J
hij : i ∈ Set.Iio j
this :
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g).obj j_1)
          (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))).f' ≫
      p =
    c.ι.app
        (Opposite.unop
          (Functor.obj
            (Functor.op
              (Monotone.functor (f :=
                (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯))
            (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij)))) ≫
      g
⊢ Eq (α :=
    Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
              (a : (↑(Set.Iio j) : Type w)) → J))
            ⋯ ⋙
          F)
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij) ⟶
      Y)
    (NatTrans.app (Cocone.ι (PrincipalSeg.cocone (Set.principalSegIio j) F))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij) ≫
      liftHom hj s ≫ p)
    (CategoryStruct.comp (Y :=
      Functor.obj.{w, v, w, u}
        (Functor.obj (Functor.const (↑(Set.Iio j) : Type w))
          (Cocone.pt (J := (↑(Set.Iio j) : Type w)) (F :=
            Monotone.functor (f :=
                (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s :=
                      fun (x1 x2 : J) ↦ x1 < x2) (Set.principalSegIio j)) :
                  (a : (↑(Set.Iio j) : Type w)) → J))
                ⋯ ⋙
              F)
            (PrincipalSeg.cocone (Set.principalSegIio j) F)))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))
      (NatTrans.app (Cocone.ι (PrincipalSeg.cocone (Set.principalSegIio j) F))
        (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))
      (c.ι.app (Opposite.unop (Opposite.op j)) ≫ g))
have dsimp : Eq (α := F.obj i ⟶ Y) (F.map (homOfLE sorry) ≫ liftHom hj s ≫ p : F.obj i ⟶ Y)
  (F.map (homOfLE sorry) ≫ c.ι.app j ≫ g : F.obj i ⟶ Y)
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
x : (↑(Set.Iio j) : Type w)
i : J
hij : i ∈ Set.Iio j
this :
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g (↑(Opposite.unop j_1) : J))
          (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))).f' ≫
      p =
    c.ι.app i ≫ g
⊢ Eq (α := F.obj i ⟶ Y) (F.map (homOfLE ⋯) ≫ liftHom hj s ≫ p : F.obj i ⟶ Y)
    (F.map (homOfLE ⋯) ≫ c.ι.app j ≫ g : F.obj i ⟶ Y)
have rw : ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (sqFunctor c p f g).obj (sorry.functor.op.obj j_1))
        (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))).f' ≫
    p =
  F.map (homOfLE sorry) ≫ c.ι.app j ≫ g
Tactic: rw [liftHom_fac_assoc _ _ _ hij, this, Cocone.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
x : (↑(Set.Iio j) : Type w)
i : J
hij : i ∈ Set.Iio j
this :
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g (↑(Opposite.unop j_1) : J))
          (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))).f' ≫
      p =
    c.ι.app i ≫ g
rw :
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (sqFunctor c p f g).obj (⋯.functor.op.obj j_1))
          (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))).f' ≫
      p =
    F.map (homOfLE ⋯) ≫ c.ι.app j ≫ g
⊢ Eq (α := F.obj i ⟶ Y) (F.map (homOfLE ⋯) ≫ liftHom hj s ≫ p : F.obj i ⟶ Y)
    (F.map (homOfLE ⋯) ≫ c.ι.app j ≫ g : F.obj i ⟶ Y)
have rw₁ : c.ι.app i ≫ g = F.map (homOfLE sorry) ≫ c.ι.app j ≫ g
Tactic: rw [liftHom_fac_assoc _ _ _ hij, this, Cocone.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
x : (↑(Set.Iio j) : Type w)
i : J
hij : i ∈ Set.Iio j
this :
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → SqStruct c p f g (↑(Opposite.unop j_1) : J))
          (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))).f' ≫
      p =
    c.ι.app i ≫ g
rw :
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (sqFunctor c p f g).obj (⋯.functor.op.obj j_1))
          (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))).f' ≫
      p =
    F.map (homOfLE ⋯) ≫ c.ι.app j ≫ g
rw₁ : c.ι.app i ≫ g = F.map (homOfLE ⋯) ≫ c.ι.app j ≫ g
⊢ Eq (α := F.obj i ⟶ Y) (F.map (homOfLE ⋯) ≫ liftHom hj s ≫ p : F.obj i ⟶ Y)
    (F.map (homOfLE ⋯) ≫ c.ι.app j ≫ g : F.obj i ⟶ Y)
have rw₂ : c.ι.app i ≫ g = c.ι.app i ≫ g
Tactic: rw [liftHom_fac_assoc _ _ _ hij, this, Cocone.w_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
j : J
hj : Order.IsSuccLimit j
s :
  (↑(Functor.sections
        (Functor.op
            (Monotone.functor (f :=
              (⇑(OrderHom.Subtype.val fun (x : J) ↦ x ∈ Set.Iio j) : (a : { x : J // x ∈ Set.Iio j }) → J)) ⋯) ⋙
          sqFunctor c p f g)) :
    Type (max v w))
i : J
hij : i < j
⊢ SqStruct.map (lift hj s) (homOfLE ⋯) =
    (↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (⋯.functor.op ⋙ sqFunctor c p f g).obj j_1)
      (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))
have f' : (SqStruct.map (lift hj s) (homOfLE sorry)).f' =
  ((↑s : (j_1 : { x : J // x ∈ Set.Iio j }ᵒᵖ) → (sorry.functor.op ⋙ sqFunctor c p f g).obj j_1)
      (Opposite.op (Subtype.mk (p := fun (x : J) ↦ x ∈ Set.Iio j) i hij))).f'
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF :
  ∀ (j : J),
    ¬IsMax j → HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this_1 :
  ∀ (sq : CommSq (Y := F.obj (Order.succ j)) sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
⊢ CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) (CommSq.lift ⋯) = f
have simp : Eq (α := F.obj ⊥ ⟶ X) (CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE sorry)) (CommSq.lift sorry))
  (F.map (homOfLE sorry) ≫ sq'.f')
Tactic: simp only [← sq'.w₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
F : Functor.{w, v, w, u} J C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst_3 : F.IsWellOrderContinuous
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF :
  ∀ (j : J),
    ¬IsMax j → HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
j : J
hj : ¬IsMax j
sq' : (sqFunctor c p f g).obj (Opposite.op j)
this_1 :
  ∀ (sq : CommSq (Y := F.obj (Order.succ j)) sq'.f' (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)), sq.HasLift
this : HasLiftingPropertyFixedBot (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
| F.map (homOfLE ⋯) ≫ sq'.f'
have rw : CategoryStruct.comp (Y := F.obj (Order.succ (Opposite.unop (Opposite.op j)))) (F.map (homOfLE sorry ≫ homOfLE sorry))
  (CommSq.lift sorry)
Tactic: rw [← sq'.sq.fac_left, ← F.map_comp_assoc]