case intro
α : Type ?u.278295
β : Type ?u.278298
γ : Type ?u.278301
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
i : ι
⊢ f i ≤ ord (iSup (succ ∘ card ∘ f))
α : Type ?u.278295
β : Type ?u.278298
γ : Type ?u.278301
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
⊢ ord (iSup (succ ∘ card ∘ f)) ∈ upperBounds (range f)
rintro a ⟨i, rfl⟩
no goals
case intro
α : Type ?u.278295
β : Type ?u.278298
γ : Type ?u.278301
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u
f : ι → Ordinal
i : ι
⊢ f i ≤ ord (iSup (succ ∘ card ∘ f))
exact le_of_lt (Cardinal.lt_ord.2 ((lt_succ _).trans_le
  (le_ciSup (Cardinal.bddAbove_range.{_, v} _) _)))