no goals
α : Type u_1
β : Type ?u.23770
γ : Type ?u.23773
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ 1 < card α ↔ Nontrivial α
classical
  rw [← not_iff_not]
  push_neg
  rw [not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton]
α : Type u_1
β : Type ?u.23770
γ : Type ?u.23773
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ ¬1 < card α ↔ ¬Nontrivial α
α : Type u_1
β : Type ?u.23770
γ : Type ?u.23773
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ 1 < card α ↔ Nontrivial α
rw [← not_iff_not]
α : Type u_1
β : Type ?u.23770
γ : Type ?u.23773
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card α ≤ 1 ↔ ¬Nontrivial α
α : Type u_1
β : Type ?u.23770
γ : Type ?u.23773
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ ¬1 < card α ↔ ¬Nontrivial α
push_neg
no goals
α : Type u_1
β : Type ?u.23770
γ : Type ?u.23773
inst✝¹ : Fintype α
inst✝ : Fintype β
⊢ card α ≤ 1 ↔ ¬Nontrivial α
rw [not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton]