α : Type u_1
β : Type u_2
γ : Type ?u.1360
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
α : Type u_1
β : Type u_2
γ : Type ?u.1360
inst✝¹ : Finite α
inst✝ : Finite β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
haveI := Fintype.ofFinite α
α : Type u_1
β : Type u_2
γ : Type ?u.1360
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
α : Type u_1
β : Type u_2
γ : Type ?u.1360
inst✝¹ : Finite α
inst✝ : Finite β
this : Fintype α
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
haveI := Fintype.ofFinite β
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1360
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
simp only [Nat.card_eq_fintype_card, Fintype.card_eq]