-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_sub : ∀ {a b : ℝ≥0∞}, (a ≠ ∞ ∨ b ≠ ∞) →
    Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 - p.2) (𝓝 (a, b)) (𝓝 (a - b))
  | ∞, ∞, h => by simp only [ne_eq, not_true_eq_false, or_self] at h
  | ∞, (b : ℝ≥0), _ => by
    rw [top_sub_coe, tendsto_nhds_top_iff_nnreal]
    refine fun x => ((lt_mem_nhds <| @coe_lt_top (b + 1 + x)).prod_nhds
      (ge_mem_nhds <| coe_lt_coe.2 <| lt_add_one b)).mono fun y hy => ?_
    rw [lt_tsub_iff_left]
    calc y.2 + x ≤ ↑(b + 1) + x := add_le_add_right hy.2 _
    _ < y.1 := hy.1
  | (a : ℝ≥0), ∞, _ => by
    rw [sub_top]
    refine (tendsto_pure.2 ?_).mono_right (pure_le_nhds _)
    exact ((gt_mem_nhds <| coe_lt_coe.2 <| lt_add_one a).prod_nhds
      (lt_mem_nhds <| @coe_lt_top (a + 1))).mono fun x hx =>
        tsub_eq_zero_iff_le.2 (hx.1.trans hx.2).le
  | (a : ℝ≥0), (b : ℝ≥0), _ => by
    simp only [nhds_coe_coe, tendsto_map'_iff, ← ENNReal.coe_sub, Function.comp_def, tendsto_coe]
    exact continuous_sub.tendsto (a, b)

Proof state:
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ Tendsto (fun p => p.1 - p.2) (𝓝 (⊤, ↑b)) (𝓝 (⊤ - ↑b))

Tactic:
rw [top_sub_coe, tendsto_nhds_top_iff_nnreal]

Result:
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, ↑b), ↑x < a.1 - a.2

Proof state:
a : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ Tendsto (fun p => p.1 - p.2) (𝓝 (↑a, ⊤)) (𝓝 (↑a - ⊤))

Tactic:
rw [sub_top]

Result:
a : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ Tendsto (fun p => p.1 - p.2) (𝓝 (↑a, ⊤)) (𝓝 0)

Proof state:
a b : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ Tendsto (fun a => a.1 - a.2) (𝓝 (a, b)) (𝓝 (a - b))

Tactic:
exact continuous_sub.tendsto (a, b)

Result:
no goals

Proof state:
a : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ∀ᶠ (x : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (↑a, ⊤), x.1 - x.2 = 0

Tactic:
exact ((gt_mem_nhds <| coe_lt_coe.2 <| lt_add_one a).prod_nhds
  (lt_mem_nhds <| @coe_lt_top (a + 1))).mono fun x hx =>
    tsub_eq_zero_iff_le.2 (hx.1.trans hx.2).le

Result:
no goals

Proof state:
a : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ Tendsto (fun p => p.1 - p.2) (𝓝 (↑a, ⊤)) (𝓝 0)

Tactic:
refine (tendsto_pure.2 ?_).mono_right (pure_le_nhds _)

Result:
a : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ ∀ᶠ (x : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (↑a, ⊤), x.1 - x.2 = 0

Proof state:
a b : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ Tendsto (fun p => p.1 - p.2) (𝓝 (↑a, ↑b)) (𝓝 (↑a - ↑b))

Tactic:
simp only [nhds_coe_coe, tendsto_map'_iff, ← ENNReal.coe_sub, Function.comp_def, tendsto_coe]

Result:
a b : ℝ≥0
x✝ : ↑a ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ Tendsto (fun a => a.1 - a.2) (𝓝 (a, b)) (𝓝 (a - b))

Proof state:
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
⊢ ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞ × ℝ≥0∞) in 𝓝 (⊤, ↑b), ↑x < a.1 - a.2

Tactic:
refine fun x => ((lt_mem_nhds <| @coe_lt_top (b + 1 + x)).prod_nhds
  (ge_mem_nhds <| coe_lt_coe.2 <| lt_add_one b)).mono fun y hy => ?_

Result:
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ ↑x < y.1 - y.2

Proof state:
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ y.2 + ↑x < y.1

Tactic:
calc y.2 + x ≤ ↑(b + 1) + x := add_le_add_right hy.2 _
_ < y.1 := hy.1

Result:
no goals

Proof state:
h : ⊤ ≠ ⊤ ∨ ⊤ ≠ ⊤
⊢ Tendsto (fun p => p.1 - p.2) (𝓝 (⊤, ⊤)) (𝓝 (⊤ - ⊤))

Tactic:
simp only [ne_eq, not_true_eq_false, or_self] at h

Result:
no goals

Proof state:
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ ↑x < y.1 - y.2

Tactic:
rw [lt_tsub_iff_left]

Result:
b : ℝ≥0
x✝ : ⊤ ≠ ⊤ ∨ ↑b ≠ ⊤
x : ℝ≥0
y : ℝ≥0∞ × ℝ≥0∞
hy : ↑(b + 1 + x) < y.1 ∧ y.2 ≤ ↑(b + 1)
⊢ y.2 + ↑x < y.1