-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
/-- Let `C` be a Grothendieck abelian category. Assume that `G : C` is a generator
of `C`. Then, any morphism in `C` is a transfinite composition of pushouts
of monomorphisms in the family `generatingMonomorphisms G` which consists
of the inclusions of the subobjects of `G`. -/
lemma exists_transfiniteCompositionOfShape :
    ∃ (J : Type w) (_ : LinearOrder J) (_ : OrderBot J) (_ : SuccOrder J)
        (_ : WellFoundedLT J),
    Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
G : C
inst✝² : Abelian C
hG : IsSeparator G
X : C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝ : Mono f
o : Ordinal.{w}
j : o.toType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
this : OrderBot o.toType := Ordinal.toTypeOrderBot ⋯
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Tactic:
exact ⟨_, _, _, _, _, ⟨transfiniteCompositionOfShapeOfEqTop hG hj⟩⟩

Result:
no goals

Proof state:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
G : C
inst✝² : Abelian C
hG : IsSeparator G
X : C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝ : Mono f
o : Ordinal.{w}
j : o.toType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Tactic:
letI : OrderBot o.toType := Ordinal.toTypeOrderBot (by
  simpa only [← Ordinal.toType_nonempty_iff_ne_zero] using Nonempty.intro j)

Result:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
G : C
inst✝² : Abelian C
hG : IsSeparator G
X : C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝ : Mono f
o : Ordinal.{w}
j : o.toType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
this : OrderBot o.toType := Ordinal.toTypeOrderBot ⋯
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
G : C
inst✝² : Abelian C
hG : IsSeparator G
X : C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝ : Mono f
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Tactic:
obtain ⟨o, j, hj⟩ := exists_ordinal hG (Subobject.mk f)

Result:
case intro.intro
C : Type u
inst✝³ : Category.{v, u} C
G : C
inst✝² : Abelian C
hG : IsSeparator G
X : C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝ : Mono f
o : Ordinal.{w}
j : o.toType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
G : C
inst✝² : Abelian C
hG : IsSeparator G
X : C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝ : Mono f
o : Ordinal.{w}
j : o.toType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
⊢ o ≠ 0

Tactic:
simpa only [← Ordinal.toType_nonempty_iff_ne_zero] using Nonempty.intro j

Result:
no goals