refine Nat.le_antisymm ?_ ?_
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α = card β
case refine_1
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card α ≤ card β

case refine_2
α : Type u
β : Type v
inst✝² : BishopFin α
inst✝¹ inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
f_inj : ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂
⊢ card β ≤ card α