awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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
dsimp :
  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)
⊢ 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))

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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
rw₂ rw₃ : c.ι.app i ≫ g = 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)

Tactic:
rw [liftHom_fac_assoc _ _ _ hij, this, Cocone.w_assoc]

Premises used: CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac_assoc, CategoryTheory.Limits.Cocone.w_assoc
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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
f' :
  (SqStruct.map (lift hj s) (homOfLE ⋯)).f' =
    ((↑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'
⊢ 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))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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 ⋯)).f' =
    ((↑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'

Tactic:
apply liftHom_fac

Premises used: CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData.liftHom_fac
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
dsimp : CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) (CommSq.lift ⋯) = f
⊢ CategoryStruct.comp (Y := F.obj (Opposite.unop (Opposite.op (Order.succ j)))) (F.map (homOfLE ⋯)) (CommSq.lift ⋯) = f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
simp :
  Eq (α := F.obj ⊥ ⟶ X) (CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) (CommSq.lift ⋯))
    (F.map (homOfLE ⋯) ≫ sq'.f')
⊢ CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) (CommSq.lift ⋯) = f

Tactic:
simp only [← sq'.w₁]

Premises used: CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
rw :
  CategoryStruct.comp (Y := F.obj (Order.succ (Opposite.unop (Opposite.op j)))) (F.map (homOfLE ⋯ ≫ homOfLE ⋯))
    (CommSq.lift ⋯)
| F.map (homOfLE ⋯) ≫ sq'.f'

Tactic:
rw [← sq'.sq.fac_left, ← F.map_comp_assoc]

Premises used: CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.sq, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.CommSq.fac_left
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
conv_rhs :
  Eq (α := F.obj ⊥ ⟶ X) (CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) (CommSq.lift ⋯))
    (CategoryStruct.comp (Y := F.obj (Order.succ (Opposite.unop (Opposite.op j)))) (F.map (homOfLE ⋯ ≫ homOfLE ⋯))
      (CommSq.lift ⋯))
⊢ Eq (α := F.obj ⊥ ⟶ X) (CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) (CommSq.lift ⋯))
    (F.map (homOfLE ⋯) ≫ sq'.f')

Tactic:
conv_rhs => rw [← sq'.sq.fac_left, ← F.map_comp_assoc]

Premises used: CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.sq, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.CommSq.fac_left
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
⊢ Eq (α := F.obj ⊥ ⟶ X) (CategoryStruct.comp (Y := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) (CommSq.lift ⋯))
    (CategoryStruct.comp (Y := F.obj (Order.succ (Opposite.unop (Opposite.op j)))) (F.map (homOfLE ⋯ ≫ homOfLE ⋯))
      (CommSq.lift ⋯))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
sq : CommSq f (c.ι.app ⊥) p g
obtain :
  ∀ (s : (↑(sqFunctor c p f g).sections : Type (max w v)))
    (hs :
      ((fun (s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ s (Opposite.op ⊥)) ∘
            Subtype.val (p := fun (x : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ x ∈ (sqFunctor c p f g).sections))
          s =
        { f' := f, w₁ := ⋯, w₂ := ⋯ : SqStruct c p f g (Opposite.unop (Opposite.op ⊥)) }),
    sq.HasLift
⊢ sq.HasLift

Tactic:
obtain ⟨s, hs⟩ := (wellOrderInductionData c f g hF).surjective { w₂ := sq.w, .. }

Premises used: CategoryTheory.HasLiftingProperty.transfiniteComposition.wellOrderInductionData, CategoryTheory.Functor.WellOrderInductionData.surjective, CategoryTheory.CommSq.w, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.mk
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
sq : CommSq f (c.ι.app ⊥) p g
s : (↑(sqFunctor c p f g).sections : Type (max w v))
hs :
  ((fun (s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ s (Opposite.op ⊥)) ∘
        Subtype.val (p := fun (x : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ x ∈ (sqFunctor c p f g).sections))
      s =
    { f' := f, w₁ := ⋯, w₂ := ⋯ : SqStruct c p f g (Opposite.unop (Opposite.op ⊥)) }
⊢ SqStruct.f' (c := c) (Y := Y) (p := p) (f := f) (g := g)
      (((fun (s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ s (Opposite.op ⊥)) ∘
          Subtype.val (p := fun (x : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) ↦ x ∈ (sqFunctor c p f g).sections))
        s) =
    { f' := f, w₁ := ⋯, w₂ := ⋯ : SqStruct c p f g (Opposite.unop (Opposite.op ⊥)) }.f'

Tactic:
replace hs := congr_arg SqStruct.f' hs
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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
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_1)
sq : CommSq f (c.ι.app ⊥) p g_1
s : (↑(sqFunctor c p f g_1).sections : Type (max w v))
hs : ((↑s : (j : Jᵒᵖ) → SqStruct c p f g_1 (Opposite.unop j)) (Opposite.op ⊥)).f' = f
j j' : J
g : j ⟶ j'
⊢ F.map g ≫ ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g_1).obj j) (Opposite.op j')).f' =
    ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g_1).obj j) (Opposite.op j)).f' ≫
      Functor.map (Functor.obj (Functor.const J) X) g

Tactic:
simpa using congr_arg SqStruct.f' (s.2 g.op)

Premises used: Quiver.Hom.op, congr_arg, CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.f', Subtype.property
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
sq : CommSq f (c.ι.app ⊥) p g
s : (↑(sqFunctor c p f g).sections : Type (max w v))
hs : ((↑s : (j : Jᵒᵖ) → SqStruct c p f g (Opposite.unop j)) (Opposite.op ⊥)).f' = f
t : Cocone F :=
  { pt := X,
    ι := { app := fun (j : J) ↦ ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
⊢ ∀ (j : J), c.ι.app j ≫ l = ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f'

Tactic:
have hl (j : J) : c.ι.app j ≫ l = (s.1 ⟨j⟩).f' := hc.fac t j
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
sq : CommSq f (c.ι.app ⊥) p g
s : (↑(sqFunctor c p f g).sections : Type (max w v))
hs : ((↑s : (j : Jᵒᵖ) → SqStruct c p f g (Opposite.unop j)) (Opposite.op ⊥)).f' = f
t : Cocone F :=
  { pt := X,
    ι := { app := fun (j : J) ↦ ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f'
rw : ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op ⊥)).f' = f
rw₁ rw₂ : f = f
⊢ c.ι.app ⊥ ≫ l = f

Tactic:
rw [hl, hs]
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
sq : CommSq f (c.ι.app ⊥) p g
s : (↑(sqFunctor c p f g).sections : Type (max w v))
hs : ((↑s : (j : Jᵒᵖ) → SqStruct c p f g (Opposite.unop j)) (Opposite.op ⊥)).f' = f
t : Cocone F :=
  { pt := X,
    ι := { app := fun (j : J) ↦ ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f'
j : J
rw : ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f' ≫ p = c.ι.app j ≫ g
rw₁ rw₂ : c.ι.app j ≫ g = c.ι.app j ≫ g
⊢ c.ι.app j ≫ l ≫ p = c.ι.app j ≫ g

Tactic:
rw [reassoc_of% (hl j), SqStruct.w₂]

Premises used: CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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)
sq : CommSq f (c.ι.app ⊥) p g
s : (↑(sqFunctor c p f g).sections : Type (max w v))
hs : ((↑s : (j : Jᵒᵖ) → SqStruct c p f g (Opposite.unop j)) (Opposite.op ⊥)).f' = f
t : Cocone F :=
  { pt := X,
    ι := { app := fun (j : J) ↦ ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f', naturality := ⋯ } }
l : c.pt ⟶ t.pt := hc.desc t
hl : ∀ (j : J), c.ι.app j ≫ l = ((↑s : (j : Jᵒᵖ) → (sqFunctor c p f g).obj j) (Opposite.op j)).f'
⊢ sq.HasLift

Tactic:
exact ⟨⟨{
    l := l
    fac_left := by rw [hl, hs]
    fac_right := hc.hom_ext (fun j ↦ by rw [reassoc_of% (hl j), SqStruct.w₂])}⟩⟩
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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
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)
⊢ HasLiftingPropertyFixedBot (A := F.obj ⊥) (c.ι.app ⊥) p g

Tactic:
fun _ sq ↦ hasLift hc hF sq

Premises used: CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLift, CategoryTheory.HasLiftingPropertyFixedBot
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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
inst_3 : F.IsWellOrderContinuous
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p
f : F.obj ⊥ ⟶ X
g : Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) ⊥ ⟶ Y
sq : CommSq f (c.ι.app ⊥) p g
j : J
hj : ¬IsMax j
x : F.obj j ⟶ X
h : CommSq x (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
⊢ HasLiftingProperty (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p

Tactic:
have := hF j hj
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
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
inst_3 : F.IsWellOrderContinuous
inst_4 : SuccOrder J
inst_5 : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingProperty (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p
f : F.obj ⊥ ⟶ X
g : Functor.obj.{w, v, w, u} (Functor.obj (Functor.const J) c.pt) ⊥ ⟶ Y
sq : CommSq f (c.ι.app ⊥) p g
j : J
hj : ¬IsMax j
x : F.obj j ⟶ X
h : CommSq x (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
this : HasLiftingProperty (B := F.obj (Order.succ j)) (F.map (homOfLE ⋯)) p
⊢ h.HasLift

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
rw : W.llp.transfiniteCompositionsOfShape J ≤ W.llp
⊢ W.llp.IsStableUnderTransfiniteCompositionOfShape J

Tactic:
rw [isStableUnderTransfiniteCompositionOfShape_iff]

Premises used: CategoryTheory.MorphismProperty.isStableUnderTransfiniteCompositionOfShape_iff
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : W.llp.TransfiniteCompositionOfShape J f
⊢ W.llp (X := h.toTransfiniteCompositionOfShape (W := W.llp).F.obj ⊥)
    (h.toTransfiniteCompositionOfShape (W := W.llp).incl.app ⊥)

Tactic:
have : W.llp (h.incl.app ⊥) := fun _ _ p hp ↦
    HasLiftingProperty.transfiniteComposition.hasLiftingProperty_ι_app_bot
      (hc := h.isColimit) (fun j hj ↦ h.map_mem j hj _ hp)
-- Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type w
inst_1 : LinearOrder J
inst_2 : SuccOrder J
inst_3 : OrderBot J
inst_4 : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : W.llp.TransfiniteCompositionOfShape J f
this :
  W.llp (X := h.toTransfiniteCompositionOfShape (W := W.llp).F.obj ⊥)
    (h.toTransfiniteCompositionOfShape (W := W.llp).incl.app ⊥)
⊢ W.llp f

Tactic:
(MorphismProperty.arrow_mk_iso_iff _
    (Arrow.isoMk h.isoBot.symm (Iso.refl _))).2 this

Premises used: Iff.mpr, CategoryTheory.Iso.refl, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.toTransfiniteCompositionOfShape, CategoryTheory.Iso.symm, CategoryTheory.TransfiniteCompositionOfShape.isoBot, CategoryTheory.Arrow.isoMk