-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_const_sub_nhds_zero_iff {l : Filter α} {f : α → ℝ≥0∞} {a : ℝ≥0∞} (ha : a ≠ ∞)
    (hfa : ∀ n, f n ≤ a) :
    Tendsto (fun n ↦ a - f n) l (𝓝 0) ↔ Tendsto (fun n ↦ f n) l (𝓝 a)

Proof state:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a ≤ ε + f n
⊢ a ≤ f n + ε

Tactic:
rwa [add_comm]

Result:
no goals

Proof state:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
⊢ Tendsto (fun n => a - f n) l (𝓝 0) ↔ Tendsto (fun n => f n) l (𝓝 a)

Tactic:
rw [ENNReal.tendsto_nhds_zero, ENNReal.tendsto_nhds ha]

Result:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)

Proof state:
case refine_1
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)

Tactic:
filter_upwards [h ε hε] with n hn

Result:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ f n ∈ Icc (a - ε) (a + ε)

Proof state:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)

Tactic:
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩

Result:
case refine_1
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)

case refine_2
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, a - f x ≤ ε

Proof state:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a ≤ f n + ε
⊢ a ≤ ε + f n

Tactic:
rwa [add_comm]

Result:
no goals

Proof state:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ f n ∈ Icc (a - ε) (a + ε)

Tactic:
refine ⟨?_, (hfa n).trans (le_add_right le_rfl)⟩

Result:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ a - ε ≤ f n

Proof state:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a - ε ≤ f n
⊢ a - f n ≤ ε

Tactic:
rw [tsub_le_iff_right] at hN_left ⊢

Result:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a ≤ f n + ε
⊢ a ≤ ε + f n

Proof state:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ a - ε ≤ f n

Tactic:
rw [tsub_le_iff_right] at hn ⊢

Result:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a ≤ ε + f n
⊢ a ≤ f n + ε

Proof state:
case refine_2
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : α) in l, a - f x ≤ ε

Tactic:
filter_upwards [h ε hε] with n hn

Result:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
⊢ a - f n ≤ ε

Proof state:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
⊢ a - f n ≤ ε

Tactic:
have hN_left := hn.1

Result:
case h
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ⊤
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, f x ∈ Icc (a - ε) (a + ε)
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : f n ∈ Icc (a - ε) (a + ε)
hN_left : a - ε ≤ f n
⊢ a - f n ≤ ε