diff --git a/src/order/disjoint.lean b/src/order/disjoint.lean
index bdff98cb1479d..86f11e8ca96b4 100644
--- a/src/order/disjoint.lean
+++ b/src/order/disjoint.lean
@@ -309,7 +309,7 @@ lemma sup_eq_top (h : is_compl x y) : x ⊔ y = ⊤ := h.codisjoint.eq_top
 
 end bounded_lattice
 
-variables [distrib_lattice α] [bounded_order α] {a b x y z : α}
+variables [distrib_lattice α] [bounded_order α] {a b c x y z : α}
 
 lemma inf_left_le_of_le_sup_right (h : is_compl x y) (hle : a ≤ b ⊔ y) : a ⊓ x ≤ b :=
 calc a ⊓ x ≤ (b ⊔ y) ⊓ x : inf_le_inf hle le_rfl
@@ -320,6 +320,18 @@ calc a ⊓ x ≤ (b ⊔ y) ⊓ x : inf_le_inf hle le_rfl
 lemma le_sup_right_iff_inf_left_le {a b} (h : is_compl x y) : a ≤ b ⊔ y ↔ a ⊓ x ≤ b :=
 ⟨h.inf_left_le_of_le_sup_right, h.symm.dual.inf_left_le_of_le_sup_right⟩
 
+lemma sup_inf_sup_eq (h : is_compl x y) : (a ⊔ x) ⊓ (b ⊔ y) = (b ⊓ x) ⊔ (a ⊓ y) :=
+calc (a ⊔ x) ⊓ (b ⊔ y) = ((a ⊓ y) ⊔ x) ⊓ ((b ⊓ x) ⊔ y) :
+  by rw [sup_inf_right, h.symm.sup_eq_top, inf_top_eq, sup_inf_right, h.sup_eq_top, inf_top_eq]
+... = (b ⊓ x) ⊔ (a ⊓ y) :
+  by rw [inf_sup_left, inf_sup_right, inf_sup_right, h.inf_eq_bot, sup_bot_eq, inf_assoc,
+    inf_left_comm y, h.symm.inf_eq_bot, inf_bot_eq, inf_bot_eq, bot_sup_eq, inf_right_idem,
+    inf_left_comm, inf_idem]
+
+lemma le_inf_sup_inf (h : is_compl x y) : a ≤ b ⊓ x ⊔ c ⊓ y ↔ a ⊓ x ≤ b ∧ a ⊓ y ≤ c :=
+by rw [← h.le_sup_right_iff_inf_left_le, ← h.symm.le_sup_right_iff_inf_left_le, ← le_inf_iff,
+  ← h.sup_inf_sup_eq, inf_comm]
+
 lemma inf_left_eq_bot_iff (h : is_compl y z) : x ⊓ y = ⊥ ↔ x ≤ z :=
 by rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]
 
diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean
index 6748130b7d2ef..e902c58e19668 100644
--- a/src/order/filter/basic.lean
+++ b/src/order/filter/basic.lean
@@ -2588,19 +2588,29 @@ lemma tendsto.not_tendsto {f : α → β} {a : filter α} {b₁ b₂ : filter β
   ¬ tendsto f a b₂ :=
 λ hf', (tendsto_inf.2 ⟨hf, hf'⟩).ne_bot.ne hb.eq_bot
 
+lemma comap_ite (p : α → Prop) [decidable_pred p] (f g : α → β) (l : filter β) :
+  comap (λ x, ite (p x) (f x) (g x)) l = comap f l ⊓ 𝓟 {x | p x} ⊔ comap g l ⊓ 𝓟 {x | ¬p x} :=
+begin
+  ext s,
+  simp only [mem_comap', ite_eq_iff, mem_sup, mem_inf_principal, mem_set_of_eq, or_imp_distrib,
+    forall_and_distrib, set_of_and, inter_mem_iff, and_imp, imp.swap]
+end
+
+lemma comap_max [linear_order β] (f g : α → β) (l : filter β) :
+  comap (λ x, max (f x) (g x)) l = comap f l ⊓ 𝓟 {x | g x < f x} ⊔ comap g l ⊓ 𝓟 {x | f x ≤ g x} :=
+by simp only [max_def, comap_ite, not_le, sup_comm]
+
+lemma tendsto_ite {l₁ : filter α} {l₂ : filter β} {f g : α → β} {p : α → Prop} [decidable_pred p] :
+  tendsto (λ x, if p x then f x else g x) l₁ l₂ ↔
+    tendsto f (l₁ ⊓ 𝓟 {x | p x}) l₂ ∧ tendsto g (l₁ ⊓ 𝓟 { x | ¬ p x }) l₂ :=
+by simp only [tendsto_iff_comap, comap_ite, ← compl_set_of,
+  (is_compl_principal {x | p x}).le_inf_sup_inf]
+
 protected lemma tendsto.if {l₁ : filter α} {l₂ : filter β} {f g : α → β} {p : α → Prop}
   [∀ x, decidable (p x)] (h₀ : tendsto f (l₁ ⊓ 𝓟 {x | p x}) l₂)
   (h₁ : tendsto g (l₁ ⊓ 𝓟 { x | ¬ p x }) l₂) :
   tendsto (λ x, if p x then f x else g x) l₁ l₂ :=
-begin
-  simp only [tendsto_def, mem_inf_principal] at *,
-  intros s hs,
-  filter_upwards [h₀ s hs, h₁ s hs],
-  simp only [mem_preimage],
-  intros x hp₀ hp₁,
-  split_ifs,
-  exacts [hp₀ h, hp₁ h],
-end
+tendsto_ite.2 ⟨h₀, h₁⟩
 
 protected lemma tendsto.if' {α β : Type*} {l₁ : filter α} {l₂ : filter β} {f g : α → β}
   {p : α → Prop} [decidable_pred p] (hf : tendsto f l₁ l₂) (hg : tendsto g l₁ l₂) :
diff --git a/src/topology/instances/ennreal.lean b/src/topology/instances/ennreal.lean
index 4937ad6818752..f76eb7c19c83e 100644
--- a/src/topology/instances/ennreal.lean
+++ b/src/topology/instances/ennreal.lean
@@ -172,8 +172,12 @@ tendsto_nhds_top $ λ n, mem_at_top_sets.2
 by rw [tendsto_nhds_top_iff_nnreal, at_top_basis_Ioi.tendsto_right_iff];
   [simp, apply_instance, apply_instance]
 
+@[simp] lemma tendsto_of_real_nhds_top {f : α → ℝ} {l : filter α} :
+  tendsto (λ x, ennreal.of_real (f x)) l (𝓝 ∞) ↔ tendsto f l at_top :=
+tendsto_coe_nhds_top.trans real.tendsto_to_nnreal_at_top_iff
+
 lemma tendsto_of_real_at_top : tendsto ennreal.of_real at_top (𝓝 ∞) :=
-tendsto_coe_nhds_top.2 tendsto_real_to_nnreal_at_top
+tendsto_of_real_nhds_top.2 tendsto_id
 
 lemma nhds_zero : 𝓝 (0 : ℝ≥0∞) = ⨅ a ≠ 0, 𝓟 (Iio a) :=
 nhds_bot_order.trans $ by simp [bot_lt_iff_ne_bot, Iio]
diff --git a/src/topology/instances/nnreal.lean b/src/topology/instances/nnreal.lean
index ceb03496d65d4..cce6f2bc1f393 100644
--- a/src/topology/instances/nnreal.lean
+++ b/src/topology/instances/nnreal.lean
@@ -99,21 +99,32 @@ map_coe_Ici_at_top 0
 lemma comap_coe_at_top : comap (coe : ℝ≥0 → ℝ) at_top = at_top :=
 (at_top_Ici_eq 0).symm
 
+@[simp] lemma _root_.real.map_to_nnreal_at_top : map real.to_nnreal at_top = at_top :=
+by simp only [← map_coe_at_top, filter.map_map, (∘), real.to_nnreal_coe, map_id']
+
+@[simp] lemma _root_.real.comap_to_nnreal_at_top : comap real.to_nnreal at_top = at_top :=
+begin
+  have := Ioi_mem_at_top (0 : ℝ),
+  simp only [← comap_coe_at_top, comap_comap, real.coe_to_nnreal', (∘), comap_max, comap_id'],
+  rw [inf_of_le_left, comap_const_of_not_mem this (lt_irrefl _)],
+  { simp },
+  { rwa le_principal_iff }
+end
+
 @[simp, norm_cast] lemma tendsto_coe_at_top {f : filter α} {m : α → ℝ≥0} :
   tendsto (λ a, (m a : ℝ)) f at_top ↔ tendsto m f at_top :=
 tendsto_Ici_at_top.symm
 
-lemma _root_.tendsto_real_to_nnreal {f : filter α} {m : α → ℝ} {x : ℝ} (h : tendsto m f (𝓝 x)) :
-  tendsto (λa, real.to_nnreal (m a)) f (𝓝 (real.to_nnreal x)) :=
+lemma _root_.filter.tendsto.real_to_nnreal {f : filter α} {m : α → ℝ} {x : ℝ}
+  (h : tendsto m f (𝓝 x)) : tendsto (λa, real.to_nnreal (m a)) f (𝓝 (real.to_nnreal x)) :=
 (continuous_real_to_nnreal.tendsto _).comp h
 
-lemma _root_.tendsto_real_to_nnreal_at_top : tendsto real.to_nnreal at_top at_top :=
-begin
-  rw ← tendsto_coe_at_top,
-  apply tendsto_id.congr' _,
-  filter_upwards [Ici_mem_at_top (0 : ℝ)] with x hx,
-  simp only [max_eq_left (set.mem_Ici.1 hx), id.def, real.coe_to_nnreal'],
-end
+@[simp] lemma _root_.real.tendsto_to_nnreal_at_top_iff {l : filter α} {f : α → ℝ} :
+  tendsto (λ x, real.to_nnreal (f x)) l at_top ↔ tendsto f l at_top :=
+by rw [← real.comap_to_nnreal_at_top, tendsto_comap_iff]
+
+lemma _root_.real.tendsto_to_nnreal_at_top : tendsto real.to_nnreal at_top at_top :=
+real.tendsto_to_nnreal_at_top_iff.2 tendsto_id
 
 lemma nhds_zero : 𝓝 (0 : ℝ≥0) = ⨅a ≠ 0, 𝓟 (Iio a) :=
 nhds_bot_order.trans $ by simp [bot_lt_iff_ne_bot]
@@ -142,7 +153,7 @@ begin
   have h_sum : (λ s, ∑ b in s, real.to_nnreal (f b)) = λ s, real.to_nnreal (∑ b in s, f b),
     from funext (λ _, (real.to_nnreal_sum_of_nonneg (λ n _, hf_nonneg n)).symm),
   simp_rw [has_sum, h_sum],
-  exact tendsto_real_to_nnreal hf.has_sum,
+  exact hf.has_sum.real_to_nnreal,
 end
 
 @[norm_cast] lemma summable_coe {f : α → ℝ≥0} : summable (λa, (f a : ℝ)) ↔ summable f :=
@@ -214,7 +225,7 @@ lemma tendsto_cofinite_zero_of_summable {α} {f : α → ℝ≥0} (hf : summable
 begin
   have h_f_coe : f = λ n, real.to_nnreal (f n : ℝ), from funext (λ n, real.to_nnreal_coe.symm),
   rw [h_f_coe, ← @real.to_nnreal_coe 0],
-  exact tendsto_real_to_nnreal ((summable_coe.mpr hf).tendsto_cofinite_zero),
+  exact (summable_coe.mpr hf).tendsto_cofinite_zero.real_to_nnreal,
 end
 
 lemma tendsto_at_top_zero_of_summable {f : ℕ → ℝ≥0} (hf : summable f) :