feat(Order/Cover): empty_covBy_singleton (#30915)

Author: eric-wieser

Mathlib/Data/Finset/Grade.lean

@@ -102,6 +102,9 @@ variable [DecidableEq α]
 lemma covBy_insert (ha : a ∉ s) : s ⋖ insert a s :=
   (wcovBy_insert _ _).covBy_of_lt <| ssubset_insert ha
 
+@[simp] lemma empty_covBy_singleton (a : α) : ∅ ⋖ ({a} : Finset α) :=
+  insert_empty_eq (β := Finset α) a ▸ covBy_insert <| notMem_empty a
+
 @[simp] lemma erase_covBy (ha : a ∈ s) : s.erase a ⋖ s := ⟨erase_ssubset ha, (erase_wcovBy _ _).2⟩
 
 lemma _root_.CovBy.exists_finset_insert (h : s ⋖ t) : ∃ a ∉ s, insert a s = t := by

Mathlib/Order/Cover.lean

@@ -459,6 +459,9 @@ variable {s t : Set α} {a : α}
 @[simp] lemma covBy_insert (ha : a ∉ s) : s ⋖ insert a s :=
   (wcovBy_insert _ _).covBy_of_lt <| ssubset_insert ha
 
+@[simp] lemma empty_covBy_singleton (a : α) : ∅ ⋖ ({a} : Set α) :=
+  insert_empty_eq (β := Set α) a ▸ covBy_insert <| notMem_empty a
+
 @[simp] lemma sdiff_singleton_covBy (ha : a ∈ s) : s \ {a} ⋖ s :=
   ⟨sdiff_lt (singleton_subset_iff.2 ha) <| singleton_ne_empty _, (sdiff_singleton_wcovBy _ _).2⟩