no goals
α : Type ?u.239463
β : Type ?u.239466
γ : Type ?u.239469
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal
n : ℕ
⊢ card o = ↑n ↔ o = ↑n
simp only [le_antisymm_iff, card_le_nat, nat_le_card]