α : Type ?u.283171
β : Type ?u.283174
γ : Type ?u.283177
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (i : ι), f i ≠ sup f
a : Ordinal
hao : a < sup f
hoa : sup f ≤ succ a
⊢ False
α : Type ?u.283171
β : Type ?u.283174
γ : Type ?u.283177
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (i : ι), f i ≠ sup f
a : Ordinal
hao : a < sup f
⊢ succ a < sup f
by_contra' hoa
no goals
α : Type ?u.283171
β : Type ?u.283174
γ : Type ?u.283177
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
hf : ∀ (i : ι), f i ≠ sup f
a : Ordinal
hao : a < sup f
hoa : sup f ≤ succ a
⊢ False
exact
  hao.not_le (sup_le fun i => le_of_lt_succ <| (lt_of_le_of_ne (le_sup _ _) (hf i)).trans_le hoa)