chore(*): simp lemmas for tendsto, Ixx, and coe (#5296)

* For `(f : α → β) (l : filter β)`, simplify `tendsto (λ a : Ixx*, f x) at_top l`
  to `tendsto f _ l`, and similarly for `at_bot`.

* For `(f : α → Ixx*) (l : filter α)`, simplify
  `tendsto f l at_top` to `tendsto (λ x, (f x : β)) l _`, and
  similarly for `at_bot`.

Here `Ixx*` is one of the intervals `Ici a`, `Ioi a`, `Ioo a b` etc,
and `_` is a filter that depends on the choice of `Ixx` and
`at_top`/`at_bot`.

* Drop some “nontriviality” assumptions like `no_top_order` for lemmas
about `Ioi a`.

Author: urkud

src/analysis/special_functions/exp_log.lean

@@ -30,7 +30,7 @@ exp, log
 
 noncomputable theory
 
-open finset filter metric asymptotics
+open finset filter metric asymptotics set function
 open_locale classical topological_space
 
 namespace complex
@@ -41,11 +41,9 @@ begin
   rw has_deriv_at_iff_is_o_nhds_zero,
   have : (1 : ℕ) < 2 := by norm_num,
   refine (is_O.of_bound (∥exp x∥) _).trans_is_o (is_o_pow_id this),
-  have : metric.ball (0 : ℂ) 1 ∈ nhds (0 : ℂ) := metric.ball_mem_nhds 0 zero_lt_one,
-  apply filter.mem_sets_of_superset this (λz hz, _),
-  simp only [metric.mem_ball, dist_zero_right] at hz,
-  simp only [exp_zero, mul_one, one_mul, add_comm, normed_field.norm_pow,
-             zero_add, set.mem_set_of_eq],
+  filter_upwards [metric.ball_mem_nhds (0 : ℂ) zero_lt_one],
+  simp only [metric.mem_ball, dist_zero_right, normed_field.norm_pow],
+  intros z hz,
   calc ∥exp (x + z) - exp x - z * exp x∥
     = ∥exp x * (exp z - 1 - z)∥ : by { congr, rw [exp_add], ring }
     ... = ∥exp x∥ * ∥exp z - 1 - z∥ : normed_field.norm_mul _ _
@@ -64,7 +62,7 @@ funext $ λ x, (has_deriv_at_exp x).deriv
 
 @[simp] lemma iter_deriv_exp : ∀ n : ℕ, (deriv^[n] exp) = exp
 | 0 := rfl
-| (n+1) := by rw [function.iterate_succ_apply, deriv_exp, iter_deriv_exp n]
+| (n+1) := by rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
 
 lemma continuous_exp : continuous exp :=
 differentiable_exp.continuous
@@ -177,7 +175,7 @@ funext $ λ x, (has_deriv_at_exp x).deriv
 
 @[simp] lemma iter_deriv_exp : ∀ n : ℕ, (deriv^[n] exp) = exp
 | 0 := rfl
-| (n+1) := by rw [function.iterate_succ_apply, deriv_exp, iter_deriv_exp n]
+| (n+1) := by rw [iterate_succ_apply, deriv_exp, iter_deriv_exp n]
 
 lemma continuous_exp : continuous exp :=
 differentiable_exp.continuous
@@ -305,26 +303,25 @@ lemma tendsto_exp_at_bot : tendsto exp at_bot (𝓝 0) :=
 (tendsto_exp_neg_at_top_nhds_0.comp tendsto_neg_at_bot_at_top).congr $
   λ x, congr_arg exp $ neg_neg x
 
-lemma tendsto_exp_at_bot_nhds_within : tendsto exp at_bot (𝓝[set.Ioi 0] 0) :=
+lemma tendsto_exp_at_bot_nhds_within : tendsto exp at_bot (𝓝[Ioi 0] 0) :=
 tendsto_inf.2 ⟨tendsto_exp_at_bot, tendsto_principal.2 $ eventually_of_forall exp_pos⟩
 
-lemma range_exp : set.range exp = set.Ioi 0 :=
-set.ext $ λ y, ⟨λ ⟨x, hx⟩, hx ▸ exp_pos x,
-  λ hy, mem_range_of_exists_le_of_exists_ge continuous_exp
-    (tendsto_exp_at_bot.eventually (ge_mem_nhds hy)).exists
-    (tendsto_exp_at_top.eventually (eventually_ge_at_top y)).exists⟩
-
 /-- `real.exp` as an order isomorphism between `ℝ` and `(0, +∞)`. -/
-def exp_order_iso : ℝ ≃o set.Ioi (0 : ℝ) :=
-(exp_strict_mono.order_iso _).trans $ order_iso.set_congr _ _ range_exp
+def exp_order_iso : ℝ ≃o Ioi (0 : ℝ) :=
+strict_mono.order_iso_of_surjective _ (exp_strict_mono.cod_restrict exp_pos) $
+  surjective_of_continuous (continuous_subtype_mk _ continuous_exp)
+    (by simp only [tendsto_Ioi_at_top, coe_cod_restrict_apply, tendsto_exp_at_top])
+    (by simp [tendsto_exp_at_bot_nhds_within])
 
 @[simp] lemma coe_exp_order_iso_apply (x : ℝ) : (exp_order_iso x : ℝ) = exp x := rfl
 
 @[simp] lemma coe_comp_exp_order_iso : coe ∘ exp_order_iso = exp := rfl
 
+@[simp] lemma range_exp : range exp = Ioi 0 :=
+by rw [← coe_comp_exp_order_iso, range_comp, exp_order_iso.range_eq, image_univ, subtype.range_coe]
+
 @[simp] lemma map_exp_at_top : map exp at_top = at_top :=
-by rw [← coe_comp_exp_order_iso, ← filter.map_map, order_iso.map_at_top,
-  map_coe_Ioi_at_top]
+by rw [← coe_comp_exp_order_iso, ← filter.map_map, order_iso.map_at_top, map_coe_Ioi_at_top]
 
 @[simp] lemma comap_exp_at_top : comap exp at_top = at_top :=
 by rw [← map_exp_at_top, comap_map exp_injective, map_exp_at_top]
@@ -337,15 +334,14 @@ lemma tendsto_comp_exp_at_top {α : Type*} {l : filter α} {f : ℝ → α} :
   tendsto (λ x, f (exp x)) at_top l ↔ tendsto f at_top l :=
 by rw [← tendsto_map'_iff, map_exp_at_top]
 
-@[simp] lemma map_exp_at_bot : map exp at_bot = 𝓝[set.Ioi 0] 0 :=
-by rw [← coe_comp_exp_order_iso, ← filter.map_map, order_iso.map_at_bot,
-  ← map_coe_Ioi_at_bot]
+@[simp] lemma map_exp_at_bot : map exp at_bot = 𝓝[Ioi 0] 0 :=
+by rw [← coe_comp_exp_order_iso, ← filter.map_map, exp_order_iso.map_at_bot, ← map_coe_Ioi_at_bot]
 
-lemma comap_exp_nhds_within_Ioi_zero : comap exp (𝓝[set.Ioi 0] 0) = at_bot :=
+lemma comap_exp_nhds_within_Ioi_zero : comap exp (𝓝[Ioi 0] 0) = at_bot :=
 by rw [← map_exp_at_bot, comap_map exp_injective]
 
 lemma tendsto_comp_exp_at_bot {α : Type*} {l : filter α} {f : ℝ → α} :
-  tendsto (λ x, f (exp x)) at_bot l ↔ tendsto f (𝓝[set.Ioi 0] 0) l :=
+  tendsto (λ x, f (exp x)) at_bot l ↔ tendsto f (𝓝[Ioi 0] 0) l :=
 by rw [← map_exp_at_bot, tendsto_map'_iff]
 
 /-- The real logarithm function, equal to the inverse of the exponential for `x > 0`,
@@ -372,17 +368,16 @@ by { rw exp_log_eq_abs (ne_of_lt hx), exact abs_of_neg hx }
 @[simp] lemma log_exp (x : ℝ) : log (exp x) = x :=
 exp_injective $ exp_log (exp_pos x)
 
-lemma surj_on_log : set.surj_on log (set.Ioi 0) set.univ :=
+lemma surj_on_log : surj_on log (Ioi 0) univ :=
 λ x _, ⟨exp x, exp_pos x, log_exp x⟩
 
-lemma log_surjective : function.surjective log :=
+lemma log_surjective : surjective log :=
 λ x, ⟨exp x, log_exp x⟩
 
-@[simp] lemma range_log : set.range log = set.univ :=
+@[simp] lemma range_log : range log = univ :=
 log_surjective.range_eq
 
-@[simp] lemma log_zero : log 0 = 0 :=
-by simp [log]
+@[simp] lemma log_zero : log 0 = 0 := dif_pos rfl
 
 @[simp] lemma log_one : log 1 = 0 :=
 exp_injective $ by rw [exp_log zero_lt_one, exp_zero]
@@ -397,7 +392,7 @@ end
 @[simp] lemma log_neg_eq_log (x : ℝ) : log (-x) = log x :=
 by rw [← log_abs x, ← log_abs (-x), abs_neg]
 
-lemma surj_on_log' : set.surj_on log (set.Iio 0) set.univ :=
+lemma surj_on_log' : surj_on log (Iio 0) univ :=
 λ x _, ⟨-exp x, neg_lt_zero.2 $ exp_pos x, by rw [log_neg_eq_log, log_exp]⟩
 
 lemma log_mul (hx : x ≠ 0) (hy : y ≠ 0) : log (x * y) = log x + log y :=
@@ -420,13 +415,13 @@ lemma log_lt_log_iff (hx : 0 < x) (hy : 0 < y) : log x < log y ↔ x < y :=
 by { rw [← exp_lt_exp, exp_log hx, exp_log hy] }
 
 lemma log_pos_iff (hx : 0 < x) : 0 < log x ↔ 1 < x :=
-by { rw ← log_one, exact log_lt_log_iff (by norm_num) hx }
+by { rw ← log_one, exact log_lt_log_iff zero_lt_one hx }
 
 lemma log_pos (hx : 1 < x) : 0 < log x :=
 (log_pos_iff (lt_trans zero_lt_one hx)).2 hx
 
 lemma log_neg_iff (h : 0 < x) : log x < 0 ↔ x < 1 :=
-by { rw ← log_one, exact log_lt_log_iff h (by norm_num) }
+by { rw ← log_one, exact log_lt_log_iff h zero_lt_one }
 
 lemma log_neg (h0 : 0 < x) (h1 : x < 1) : log x < 0 := (log_neg_iff h0).2 h1
 
@@ -467,15 +462,15 @@ tendsto_comp_exp_at_top.1 $ by simpa only [log_exp] using tendsto_id
 lemma tendsto_log_nhds_within_zero : tendsto log (𝓝[{0}ᶜ] 0) at_bot :=
 begin
   rw [← (show _ = log, from funext log_abs)],
-  refine tendsto.comp (_ : tendsto log (𝓝[set.Ioi 0] (abs 0)) at_bot)
+  refine tendsto.comp (_ : tendsto log (𝓝[Ioi 0] (abs 0)) at_bot)
     ((continuous_abs.tendsto 0).inf (tendsto_principal_principal.2 $ λ a, abs_pos.2)),
   rw [abs_zero, ← tendsto_comp_exp_at_bot],
   simpa using tendsto_id
 end
 
 lemma continuous_on_log : continuous_on log {0}ᶜ :=
 begin
-  rw [continuous_on_iff_continuous_restrict, set.restrict],
+  rw [continuous_on_iff_continuous_restrict, restrict],
   conv in (log _) { rw [log_of_ne_zero (show (x : ℝ) ≠ 0, from x.2)] },
   exact exp_order_iso.symm.continuous.comp (continuous_subtype_mk _ continuous_subtype_coe.norm)
 end
@@ -686,7 +681,7 @@ end
 /-- The function `x^n * exp(-x)` tends to `0` at `+∞`, for any natural number `n`. -/
 lemma tendsto_pow_mul_exp_neg_at_top_nhds_0 (n : ℕ) : tendsto (λx, x^n * exp (-x)) at_top (𝓝 0) :=
 (tendsto_inv_at_top_zero.comp (tendsto_exp_div_pow_at_top n)).congr $ λx,
-  by rw [function.comp_app, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]
+  by rw [comp_app, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]
 
 /-- The function `(b * exp x + c) / (x ^ n)` tends to `+∞` at `+∞`, for any positive natural number
 `n` and any real numbers `b` and `c` such that `b` is positive. -/
@@ -733,7 +728,7 @@ begin
   and then apply the mean value inequality. -/
   let F : ℝ → ℝ := λ x, ∑ i in range n, x^(i+1)/(i+1) + log (1-x),
   -- First step: compute the derivative of `F`
-  have A : ∀ y ∈ set.Ioo (-1 : ℝ) 1, deriv F y = - (y^n) / (1 - y),
+  have A : ∀ y ∈ Ioo (-1 : ℝ) 1, deriv F y = - (y^n) / (1 - y),
   { assume y hy,
     have : (∑ i in range n, (↑i + 1) * y ^ i / (↑i + 1)) = (∑ i in range n, y ^ i),
     { congr' with i,
@@ -743,9 +738,9 @@ begin
                 sub_ne_zero_of_ne (ne_of_gt hy.2), sub_ne_zero_of_ne (ne_of_lt hy.2)],
     ring },
   -- second step: show that the derivative of `F` is small
-  have B : ∀ y ∈ set.Icc (-abs x) (abs x), abs (deriv F y) ≤ (abs x)^n / (1 - abs x),
+  have B : ∀ y ∈ Icc (-abs x) (abs x), abs (deriv F y) ≤ (abs x)^n / (1 - abs x),
   { assume y hy,
-    have : y ∈ set.Ioo (-(1 : ℝ)) 1 := ⟨lt_of_lt_of_le (neg_lt_neg h) hy.1, lt_of_le_of_lt hy.2 h⟩,
+    have : y ∈ Ioo (-(1 : ℝ)) 1 := ⟨lt_of_lt_of_le (neg_lt_neg h) hy.1, lt_of_le_of_lt hy.2 h⟩,
     calc abs (deriv F y) = abs (-(y^n) / (1 - y)) : by rw [A y this]
     ... ≤ (abs x)^n / (1 - abs x) :
       begin
@@ -757,7 +752,7 @@ begin
       end },
   -- third step: apply the mean value inequality
   have C : ∥F x - F 0∥ ≤ ((abs x)^n / (1 - abs x)) * ∥x - 0∥,
-  { have : ∀ y ∈ set.Icc (- abs x) (abs x), differentiable_at ℝ F y,
+  { have : ∀ y ∈ Icc (- abs x) (abs x), differentiable_at ℝ F y,
     { assume y hy,
       have : 1 - y ≠ 0 := sub_ne_zero_of_ne (ne_of_gt (lt_of_le_of_lt hy.2 h)),
       simp [F, this] },

src/order/filter/at_top_bot.lean

@@ -722,9 +722,13 @@ end
 
 /-- The `at_top` filter for an open interval `Ioi a` comes from the `at_top` filter in the ambient
 order. -/
-lemma at_top_Ioi_eq [semilattice_sup α] [no_top_order α] (a : α) :
+lemma at_top_Ioi_eq [semilattice_sup α] (a : α) :
   at_top = comap (coe : Ioi a → α) at_top :=
-by rw [← map_coe_Ioi_at_top a, comap_map subtype.coe_injective]
+begin
+  nontriviality,
+  rcases nontrivial_iff_nonempty.1 ‹_› with ⟨b, hb⟩,
+  rw [← map_coe_at_top_of_Ici_subset (Ici_subset_Ioi.2 hb), comap_map subtype.coe_injective]
+end
 
 /-- The `at_top` filter for an open interval `Ici a` comes from the `at_top` filter in the ambient
 order. -/
@@ -740,9 +744,9 @@ order. -/
 
 /-- The `at_bot` filter for an open interval `Iio a` comes from the `at_bot` filter in the ambient
 order. -/
-lemma at_bot_Iio_eq [semilattice_inf α] [no_bot_order α] (a : α) :
+lemma at_bot_Iio_eq [semilattice_inf α] (a : α) :
   at_bot = comap (coe : Iio a → α) at_bot :=
-@at_top_Ioi_eq (order_dual α) _ _ _
+@at_top_Ioi_eq (order_dual α) _ _
 
 /-- The `at_bot` filter for an open interval `Iic a` comes from the `at_bot` filter in the ambient
 order. -/
@@ -756,6 +760,44 @@ lemma at_bot_Iic_eq [semilattice_inf α] (a : α) :
   at_bot = comap (coe : Iic a → α) at_bot :=
 @at_top_Ici_eq (order_dual α) _ _
 
+lemma tendsto_Ioi_at_top [semilattice_sup α] {a : α} {f : β → Ioi a}
+  {l : filter β} :
+  tendsto f l at_top ↔ tendsto (λ x, (f x : α)) l at_top :=
+by rw [at_top_Ioi_eq, tendsto_comap_iff]
+
+lemma tendsto_Iio_at_bot [semilattice_inf α] {a : α} {f : β → Iio a}
+  {l : filter β} :
+  tendsto f l at_bot ↔ tendsto (λ x, (f x : α)) l at_bot :=
+by rw [at_bot_Iio_eq, tendsto_comap_iff]
+
+lemma tendsto_Ici_at_top [semilattice_sup α] {a : α} {f : β → Ici a} {l : filter β} :
+  tendsto f l at_top ↔ tendsto (λ x, (f x : α)) l at_top :=
+by rw [at_top_Ici_eq, tendsto_comap_iff]
+
+lemma tendsto_Iic_at_bot [semilattice_inf α] {a : α} {f : β → Iic a} {l : filter β} :
+  tendsto f l at_bot ↔ tendsto (λ x, (f x : α)) l at_bot :=
+by rw [at_bot_Iic_eq, tendsto_comap_iff]
+
+@[simp] lemma tendsto_comp_coe_Ioi_at_top [semilattice_sup α] [no_top_order α] {a : α}
+  {f : α → β} {l : filter β} :
+  tendsto (λ x : Ioi a, f x) at_top l ↔ tendsto f at_top l :=
+by rw [← map_coe_Ioi_at_top a, tendsto_map'_iff]
+
+@[simp] lemma tendsto_comp_coe_Ici_at_top [semilattice_sup α] {a : α}
+  {f : α → β} {l : filter β} :
+  tendsto (λ x : Ici a, f x) at_top l ↔ tendsto f at_top l :=
+by rw [← map_coe_Ici_at_top a, tendsto_map'_iff]
+
+@[simp] lemma tendsto_comp_coe_Iio_at_bot [semilattice_inf α] [no_bot_order α] {a : α}
+  {f : α → β} {l : filter β} :
+  tendsto (λ x : Iio a, f x) at_bot l ↔ tendsto f at_bot l :=
+by rw [← map_coe_Iio_at_bot a, tendsto_map'_iff]
+
+@[simp] lemma tendsto_comp_coe_Iic_at_bot [semilattice_inf α] {a : α}
+  {f : α → β} {l : filter β} :
+  tendsto (λ x : Iic a, f x) at_bot l ↔ tendsto f at_bot l :=
+by rw [← map_coe_Iic_at_bot a, tendsto_map'_iff]
+
 lemma map_add_at_top_eq_nat (k : ℕ) : map (λa, a + k) at_top = at_top :=
 map_at_top_eq_of_gc (λa, a - k) k
   (assume a b h, add_le_add_right h k)

src/order/filter/basic.lean

@@ -522,6 +522,12 @@ lemma forall_sets_nonempty_iff_ne_bot {f : filter α} :
   (∀ (s : set α), s ∈ f → s.nonempty) ↔ ne_bot f :=
 ⟨λ h hf, empty_not_nonempty (h ∅ $ hf.symm ▸ mem_bot_sets), @nonempty_of_mem_sets _ _⟩
 
+lemma nontrivial_iff_nonempty : nontrivial (filter α) ↔ nonempty α :=
+⟨λ ⟨⟨f, g, hfg⟩⟩, by_contra $
+  λ h, hfg $ (filter_eq_bot_of_not_nonempty f h).trans (filter_eq_bot_of_not_nonempty g h).symm,
+  λ ⟨x⟩, ⟨⟨⊤, ⊥, forall_sets_nonempty_iff_ne_bot.1 $ λ s hs,
+    by rwa [mem_top_sets.1 hs, ← nonempty_iff_univ_nonempty]⟩⟩⟩
+
 lemma mem_sets_of_eq_bot {f : filter α} {s : set α} (h : f ⊓ 𝓟 sᶜ = ⊥) : s ∈ f :=
 have ∅ ∈ f ⊓ 𝓟 sᶜ, from h.symm ▸ mem_bot_sets,
 let ⟨s₁, hs₁, s₂, (hs₂ : sᶜ ⊆ s₂), (hs : s₁ ∩ s₂ ⊆ ∅)⟩ := this in

src/order/rel_iso.lean

@@ -413,6 +413,8 @@ protected lemma bijective (e : r ≃r s) : bijective e := e.to_equiv.bijective
 protected lemma injective (e : r ≃r s) : injective e := e.to_equiv.injective
 protected lemma surjective (e : r ≃r s) : surjective e := e.to_equiv.surjective
 
+@[simp] lemma range_eq (e : r ≃r s) : set.range e = set.univ := e.surjective.range_eq
+
 /-- Any equivalence lifts to a relation isomorphism between `s` and its preimage. -/
 protected def preimage (f : α ≃ β) (s : β → β → Prop) : f ⁻¹'o s ≃r s := ⟨f, λ a b, iff.rfl⟩
 
@@ -502,6 +504,8 @@ protected lemma bijective (e : α ≃o β) : bijective e := e.to_equiv.bijective
 protected lemma injective (e : α ≃o β) : injective e := e.to_equiv.injective
 protected lemma surjective (e : α ≃o β) : surjective e := e.to_equiv.surjective
 
+@[simp] lemma range_eq (e : α ≃o β) : set.range e = set.univ := e.surjective.range_eq
+
 @[simp] lemma apply_eq_iff_eq (e : α ≃o β) {x y : α} : e x = e y ↔ x = y :=
 e.to_equiv.apply_eq_iff_eq