-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
/-- If `κ` is a suitable cardinal for the small object argument for `I : MorphismProperty C`,
then the class `I.rlp.llp` is exactly the class of morphisms that are retracts
of transfinite compositions (of shape `κ.ord.toType`) of pushouts of coproducts
of maps in `I`. -/
lemma llp_rlp_of_isCardinalForSmallObjectArgument' :
    I.rlp.llp = (transfiniteCompositionsOfShape
      (coproducts.{w} I).pushouts κ.ord.toType).retracts

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp = ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts

Tactic:
refine le_antisymm ?_
  (retracts_transfiniteCompositionsOfShape_pushouts_coproducts_le_llp_rlp I κ.ord.toType)

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp ≤ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
⊢ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts f

Tactic:
have := hf _ (rlp_πObj I κ f)

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
this : HasLiftingProperty f (πObj I κ f)
⊢ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
⊢ ιObj I κ f ≫ πObj I κ f = f ≫ 𝟙 Y

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
⊢ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts f

Tactic:
have sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 _) := ⟨by simp⟩

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
⊢ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
this : HasLiftingProperty f (πObj I κ f)
⊢ RetractArrow f (ιObj I κ f)

Tactic:
exact
  { i := Arrow.homMk (𝟙 _) sq.lift
    r := Arrow.homMk (𝟙 _) (πObj I κ f) }

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
⊢ I.rlp.llp ≤ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts

Tactic:
intro X Y f hf

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
⊢ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
this : HasLiftingProperty f (πObj I κ f)
⊢ ((coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.toType).retracts f

Tactic:
refine ⟨_, _, _, ?_, transfiniteCompositionsOfShape_ιObj I κ f⟩

Result:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
hf : I.rlp.llp f
sq : CommSq (ιObj I κ f) f (πObj I κ f) (𝟙 Y)
this : HasLiftingProperty f (πObj I κ f)
⊢ RetractArrow f (ιObj I κ f)