feat(Data/Finset): Add a few Finset lemmas (#5933)

Adds four `Finset` lemmas:
- `Nonempty.inl` and `Nonempty.inr` - unions with Nonempty sets are Nonempty
- `sup'_mono` and `inf'_mono` - analogues of `sup_mono` and `inf_mono`.



Co-authored-by: Oliver Nash <github@olivernash.org>

Mathlib/Data/Finset/Basic.lean

@@ -1448,6 +1448,12 @@ theorem empty_union (s : Finset α) : ∅ ∪ s = s :=
   ext fun x => mem_union.trans <| by simp
 #align finset.empty_union Finset.empty_union
 
+theorem Nonempty.inl {s t : Finset α} (h : s.Nonempty) : (s ∪ t).Nonempty :=
+  h.mono $ subset_union_left s t
+
+theorem Nonempty.inr {s t : Finset α} (h : t.Nonempty) : (s ∪ t).Nonempty :=
+  h.mono $ subset_union_right s t
+
 theorem insert_eq (a : α) (s : Finset α) : insert a s = {a} ∪ s :=
   rfl
 #align finset.insert_eq Finset.insert_eq

Mathlib/Data/Finset/Lattice.lean

@@ -884,6 +884,10 @@ theorem sup'_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (s.map f)
   rfl
 #align finset.sup'_map Finset.sup'_map
 
+theorem sup'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty):
+    s₁.sup' h₁ f ≤ s₂.sup' (h₁.mono h) f :=
+  Finset.sup'_le h₁ _ (fun _ hb => le_sup' _ (h hb))
+
 end Sup'
 
 section Inf'
@@ -980,6 +984,10 @@ theorem inf'_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : (s.map f)
   sup'_map (α := αᵒᵈ) _ hs hs'
 #align finset.inf'_map Finset.inf'_map
 
+theorem inf'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) :
+    s₂.inf' (h₁.mono h) f ≤ s₁.inf' h₁ f :=
+  Finset.le_inf' h₁ _ (fun _ hb => inf'_le _ (h hb))
+
 end Inf'
 
 section Sup