refine Nat.le_antisymm ?_ ?_
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card α = card β
case refine_1
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card α ≤ card β

case refine_2
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
g : β → α
hgf : ∀ (a : α), g (f a) = a
hfg : ∀ (b : β), f (g b) = b
⊢ card β ≤ card α