-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
lemma exists_ordinal (A₀ : Subobject X) :
    ∃ (o : Ordinal.{w}) (j : o.toType), transfiniteIterate (largerSubobject hG) j A₀ = ⊤

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₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
⊢ ∃ o j, transfiniteIterate (largerSubobject hG) j A₀ = ⊤

Tactic:
have : OrderBot κ.ord.toType := Ordinal.toTypeOrderBot (by
  simp only [ne_eq, Cardinal.ord_eq_zero]
  apply Cardinal.succ_ne_zero)

Result:
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₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
this : OrderBot κ.ord.toType
⊢ ∃ o j, transfiniteIterate (largerSubobject hG) j A₀ = ⊤

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₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
⊢ ¬κ = 0

Tactic:
apply Cardinal.succ_ne_zero

Result:
no goals

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₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
this : OrderBot κ.ord.toType
⊢ Order.succ (Cardinal.lift.{w, max u v} (Cardinal.mk (Subobject X))) ≤
    Cardinal.lift.{max u v, w} (Cardinal.mk κ.ord.toType)

Tactic:
simp [κ]

Result:
no goals

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₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
this : OrderBot κ.ord.toType
⊢ ∃ o j, transfiniteIterate (largerSubobject hG) j A₀ = ⊤

Tactic:
exact ⟨κ.ord, top_mem_range hG A₀ (lt_of_lt_of_le (Order.lt_succ _) (by simp [κ]))⟩

Result:
no goals

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₀ : Subobject X
⊢ ∃ o j, transfiniteIterate (largerSubobject hG) j A₀ = ⊤

Tactic:
let κ := Order.succ (Cardinal.mk (Shrink.{w} (Subobject X)))

Result:
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₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
⊢ ∃ o j, transfiniteIterate (largerSubobject hG) j A₀ = ⊤

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₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
⊢ κ.ord ≠ 0

Tactic:
simp only [ne_eq, Cardinal.ord_eq_zero]

Result:
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₀ : Subobject X
κ : Cardinal.{w} := Order.succ (Cardinal.mk (Shrink.{w, max u v} (Subobject X)))
⊢ ¬κ = 0