case inl
α : Type ?u.69712
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
i j : Ordinal
hi : i < o
hj : j < o
hij✝ : i ≤ j
hij : i < j
⊢ f i hi ≤ f j hj

case inr
α : Type ?u.69712
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
i : Ordinal
hi hj : i < o
hij : i ≤ i
⊢ f i hi ≤ f i hj
α : Type ?u.69712
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
i j : Ordinal
hi : i < o
hj : j < o
hij : i ≤ j
⊢ f i hi ≤ f j hj
rcases lt_or_eq_of_le hij with (hij | rfl)
no goals
case inl
α : Type ?u.69712
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
i j : Ordinal
hi : i < o
hj : j < o
hij✝ : i ≤ j
hij : i < j
⊢ f i hi ≤ f j hj
exact (hf.2.1 hi hj hij).le
no goals
case inr
α : Type ?u.69712
r : α → α → Prop
a o : Ordinal
f : (b : Ordinal) → b < o → Ordinal
hf : IsFundamentalSequence a o f
i : Ordinal
hi hj : i < o
hij : i ≤ i
⊢ f i hi ≤ f i hj
rfl