no goals
α : Type ?u.376135
β : Type ?u.376138
γ : Type ?u.376141
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ι : Type u_1
f : ι → Ordinal
a : Ordinal
ha : ∀ (i : ι), f i ≠ a
⊢ a ∈ range fᶜ
simp [ha]