feat(data/set/basic): A set is either a subsingleton or nontrivial (#…

…17901)

Also make the argument to `set.finite_or_infinite` explicit.

src/data/finset/basic.lean

@@ -432,7 +432,7 @@ end empty
 /-! ### singleton -/
 
 section singleton
-variables {a : α}
+variables {s : finset α} {a : α}
 
 /--
 `{a} : finset a` is the set `{a}` containing `a` and nothing else.
@@ -520,6 +520,9 @@ by rw [←coe_ssubset, coe_singleton, set.ssubset_singleton_iff, coe_eq_empty]
 lemma eq_empty_of_ssubset_singleton {s : finset α} {x : α} (hs : s ⊂ {x}) : s = ∅ :=
 ssubset_singleton_iff.1 hs
 
+lemma eq_singleton_or_nontrivial (ha : a ∈ s) : s = {a} ∨ (s : set α).nontrivial :=
+by { rw ←coe_eq_singleton, exact set.eq_singleton_or_nontrivial ha }
+
 instance [nonempty α] : nontrivial (finset α) :=
 ‹nonempty α›.elim $ λ a, ⟨⟨{a}, ∅, singleton_ne_empty _⟩⟩
 

src/data/set/basic.lean

@@ -1549,6 +1549,12 @@ iff.not_left not_subsingleton_iff.symm
 alias not_nontrivial_iff ↔ _ subsingleton.not_nontrivial
 alias not_subsingleton_iff ↔ _ nontrivial.not_subsingleton
 
+protected lemma subsingleton_or_nontrivial (s : set α) : s.subsingleton ∨ s.nontrivial :=
+by simp [or_iff_not_imp_right]
+
+lemma eq_singleton_or_nontrivial (ha : a ∈ s) : s = {a} ∨ s.nontrivial :=
+by { rw ←subsingleton_iff_singleton ha, exact s.subsingleton_or_nontrivial }
+
 theorem univ_eq_true_false : univ = ({true, false} : set Prop) :=
 eq.symm $ eq_univ_of_forall $ classical.cases (by simp) (by simp)
 

src/data/set/finite.lean

@@ -114,8 +114,8 @@ protected def infinite (s : set α) : Prop := ¬ s.finite
 
 @[simp] lemma not_infinite {s : set α} : ¬ s.infinite ↔ s.finite := not_not
 
-/-- See also `fintype_or_infinite`. -/
-lemma finite_or_infinite {s : set α} : s.finite ∨ s.infinite := em _
+/-- See also `finite_or_infinite`, `fintype_or_infinite`. -/
+protected lemma finite_or_infinite (s : set α) : s.finite ∨ s.infinite := em _
 
 /-! ### Basic properties of `set.finite.to_finset` -/
 

src/order/well_founded_set.lean

@@ -251,7 +251,7 @@ lemma _root_.is_antichain.finite_of_partially_well_ordered_on (ha : is_antichain
   (hp : s.partially_well_ordered_on r) :
   s.finite :=
 begin
-  refine finite_or_infinite.resolve_right (λ hi, _),
+  refine not_infinite.1 (λ hi, _),
   obtain ⟨m, n, hmn, h⟩ := hp (λ n, hi.nat_embedding _ n) (λ n, (hi.nat_embedding _ n).2),
   exact hmn.ne ((hi.nat_embedding _).injective $ subtype.val_injective $
     ha.eq (hi.nat_embedding _ m).2 (hi.nat_embedding _ n).2 h),