case inl
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
⊢ cof 0 ≤ cof (f 0)

case inr.inl.intro
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
b : Ordinal
⊢ cof (succ b) ≤ cof (f (succ b))

case inr.inr
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a : Ordinal
ha : IsLimit a
⊢ cof a ≤ cof (f a)
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a : Ordinal
⊢ cof a ≤ cof (f a)
rcases zero_or_succ_or_limit a with (rfl | ⟨b, rfl⟩ | ha)
case inl
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
⊢ 0 ≤ cof (f 0)
case inl
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
⊢ cof 0 ≤ cof (f 0)
rw [cof_zero]
no goals
case inl
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
⊢ 0 ≤ cof (f 0)
exact zero_le _
case inr.inl.intro
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
b : Ordinal
⊢ 0 < f (succ b)
case inr.inl.intro
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
b : Ordinal
⊢ cof (succ b) ≤ cof (f (succ b))
rw [cof_succ, Cardinal.one_le_iff_ne_zero, cof_ne_zero, ← Ordinal.pos_iff_ne_zero]
no goals
case inr.inl.intro
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
b : Ordinal
⊢ 0 < f (succ b)
exact (Ordinal.zero_le (f b)).trans_lt (hf.1 b)
no goals
case inr.inr
α : Type ?u.99458
r : α → α → Prop
f : Ordinal → Ordinal
hf : IsNormal f
a : Ordinal
ha : IsLimit a
⊢ cof a ≤ cof (f a)
rw [hf.cof_eq ha]