feat(order/filter/small_sets): yet another squeeze theorem (#16286)

* Add a very general version of the squeeze theorem.
* Use it to golf the proof of the usual squeeze theorem.
* Add docstrings.

src/order/filter/small_sets.lean

@@ -106,6 +106,17 @@ begin
   exact λ u hu, (ht u hu).mp (hst.mono $ λ a hst ht, subset.trans hst ht)
 end
 
+/-- Generalized **squeeze theorem** (also known as **sandwich theorem**). If `s : α → set β` is a
+family of sets that tends to `filter.small_sets lb` along `la` and `f : α → β` is a function such
+that `f x ∈ s x` eventually along `la`, then `f` tends to `lb` along `la`.
+
+If `s x` is the closed interval `[g x, h x]` for some functions `g`, `h` that tend to the same limit
+`𝓝 y`, then we obtain the standard squeeze theorem, see
+`tendsto_of_tendsto_of_tendsto_of_le_of_le'`. -/
+lemma tendsto.of_small_sets {s : α → set β} {f : α → β} (hs : tendsto s la lb.small_sets)
+  (hf : ∀ᶠ x in la, f x ∈ s x) : tendsto f la lb :=
+λ t ht, hf.mp $ (tendsto_small_sets_iff.mp hs t ht).mono $ λ x h₁ h₂, h₁ h₂
+
 @[simp] lemma eventually_small_sets_eventually {p : α → Prop} :
   (∀ᶠ s in l.small_sets, ∀ᶠ x in l', x ∈ s → p x) ↔ ∀ᶠ x in l ⊓ l', p x :=
 calc _ ↔ ∃ s ∈ l, ∀ᶠ x in l', x ∈ s → p x :

src/topology/algebra/order/basic.lean

@@ -762,22 +762,16 @@ tendsto_Ixx_class_of_subset (λ _ _, Ioc_subset_Icc_self)
 instance tendsto_Ioo_class_nhds (a : α) : tendsto_Ixx_class Ioo (𝓝 a) (𝓝 a) :=
 tendsto_Ixx_class_of_subset (λ _ _, Ioo_subset_Icc_self)
 
-/-- Also known as squeeze or sandwich theorem. This version assumes that inequalities hold
-eventually for the filter. -/
+/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
+hold eventually for the filter. -/
 lemma tendsto_of_tendsto_of_tendsto_of_le_of_le' {f g h : β → α} {b : filter β} {a : α}
   (hg : tendsto g b (𝓝 a)) (hh : tendsto h b (𝓝 a))
   (hgf : ∀ᶠ b in b, g b ≤ f b) (hfh : ∀ᶠ b in b, f b ≤ h b) :
   tendsto f b (𝓝 a) :=
-tendsto_order.2
-  ⟨assume a' h',
-    have ∀ᶠ b in b, a' < g b, from (tendsto_order.1 hg).left a' h',
-    by filter_upwards [this, hgf] with _ using lt_of_lt_of_le,
-    assume a' h',
-    have ∀ᶠ b in b, h b < a', from (tendsto_order.1 hh).right a' h',
-    by filter_upwards [this, hfh] with a h₁ h₂ using lt_of_le_of_lt h₂ h₁⟩
-
-/-- Also known as squeeze or sandwich theorem. This version assumes that inequalities hold
-everywhere. -/
+(hg.Icc hh).of_small_sets $ hgf.and hfh
+
+/-- **Squeeze theorem** (also known as **sandwich theorem**). This version assumes that inequalities
+hold everywhere. -/
 lemma tendsto_of_tendsto_of_tendsto_of_le_of_le {f g h : β → α} {b : filter β} {a : α}
   (hg : tendsto g b (𝓝 a)) (hh : tendsto h b (𝓝 a)) (hgf : g ≤ f) (hfh : f ≤ h) :
   tendsto f b (𝓝 a) :=