α : Type u_1
β : Type ?u.1718
γ : Type ?u.1721
inst✝ : Finite α
this : Fintype α
⊢ 1 < Nat.card α ↔ Nontrivial α
α : Type u_1
β : Type ?u.1718
γ : Type ?u.1721
inst✝ : Finite α
⊢ 1 < Nat.card α ↔ Nontrivial α
haveI := Fintype.ofFinite α
no goals
α : Type u_1
β : Type ?u.1718
γ : Type ?u.1721
inst✝ : Finite α
this : Fintype α
⊢ 1 < Nat.card α ↔ Nontrivial α
simp only [Nat.card_eq_fintype_card, Fintype.one_lt_card_iff_nontrivial]