no goals
α : Type ?u.68576
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
i : Ordinal
hi : i < ord (cof a)
⊢ ord (cof a) ≤ o
rw [hf.cof_eq]
α : Type ?u.68576
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
H : ord (cof a) = o
⊢ IsFundamentalSequence a (ord (cof a)) fun i hi => f i (_ : i < o)
α : Type ?u.68576
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
⊢ IsFundamentalSequence a (ord (cof a)) fun i hi => f i (_ : i < o)
have H := hf.cof_eq
α : Type ?u.68576
r : α → α → Prop
a : Ordinal
f : (b : Ordinal) → b < ord (cof a) → Ordinal
hf : IsFundamentalSequence a (ord (cof a)) f
⊢ IsFundamentalSequence a (ord (cof a)) fun i hi => f i (_ : i < ord (cof a))
α : Type ?u.68576
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
H : ord (cof a) = o
⊢ IsFundamentalSequence a (ord (cof a)) fun i hi => f i (_ : i < o)
subst H
no goals
α : Type ?u.68576
r : α → α → Prop
a : Ordinal
f : (b : Ordinal) → b < ord (cof a) → Ordinal
hf : IsFundamentalSequence a (ord (cof a)) f
⊢ IsFundamentalSequence a (ord (cof a)) fun i hi => f i (_ : i < ord (cof a))
exact hf