α : Type u_1
β : Type ?u.20214
γ : Type ?u.20217
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x
α : Type u_1
β : Type ?u.20214
γ : Type ?u.20217
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card α = 1 ↔ ∃ x, ∀ (y : α), y = x
rw [← card_unit, card_eq]
no goals
α : Type u_1
β : Type ?u.20214
γ : Type ?u.20217
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ Nonempty (α ≃ Unit) ↔ ∃ x, ∀ (y : α), y = x
exact
  ⟨fun ⟨a⟩ => ⟨a.symm (), fun y => a.injective (Subsingleton.elim _ _)⟩,
   fun ⟨x, hx⟩ =>
    ⟨⟨fun _ => (), fun _ => x, fun _ => (hx _).trans (hx _).symm, fun _ =>
        Subsingleton.elim _ _⟩⟩⟩