case intro
α : Type ?u.94563
r : α → α → Prop
a : Ordinal
f : (b : Ordinal) → b < ord (cof a) → Ordinal
hf : IsFundamentalSequence a (ord (cof a)) f
⊢ cof (ord (cof a)) = cof a
α : Type ?u.94563
r : α → α → Prop
a : Ordinal
⊢ cof (ord (cof a)) = cof a
cases' exists_fundamental_sequence a with f hf
case intro.intro
α : Type ?u.94563
r : α → α → Prop
a : Ordinal
f : (b : Ordinal) → b < ord (cof a) → Ordinal
hf : IsFundamentalSequence a (ord (cof a)) f
g : (b : Ordinal) → b < ord (cof (ord (cof a))) → Ordinal
hg : IsFundamentalSequence (ord (cof a)) (ord (cof (ord (cof a)))) g
⊢ cof (ord (cof a)) = cof a
case intro
α : Type ?u.94563
r : α → α → Prop
a : Ordinal
f : (b : Ordinal) → b < ord (cof a) → Ordinal
hf : IsFundamentalSequence a (ord (cof a)) f
⊢ cof (ord (cof a)) = cof a
cases' exists_fundamental_sequence a.cof.ord with g hg
no goals
case intro.intro
α : Type ?u.94563
r : α → α → Prop
a : Ordinal
f : (b : Ordinal) → b < ord (cof a) → Ordinal
hf : IsFundamentalSequence a (ord (cof a)) f
g : (b : Ordinal) → b < ord (cof (ord (cof a))) → Ordinal
hg : IsFundamentalSequence (ord (cof a)) (ord (cof (ord (cof a)))) g
⊢ cof (ord (cof a)) = cof a
exact ord_injective (hf.trans hg).cof_eq.symm