-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_atTop_zero_iff_lt_of_antitone {β : Type*} [Nonempty β] [SemilatticeSup β]
    {f : β → ℝ≥0∞} (hf : Antitone f) :
    Filter.Tendsto f Filter.atTop (𝓝 0) ↔ ∀ ε, 0 < ε → ∃ n : β, f n < ε

Proof state:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ¬ε = ⊤
⊢ 1 < 2

Tactic:
norm_num

Result:
no goals

Proof state:
case mp.intro
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
⊢ ∃ n, f n < ε

Tactic:
refine ⟨n, hn.trans_lt ?_⟩

Result:
case mp.intro
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
⊢ 1 ⊓ ε / 2 < ε

Proof state:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ¬ε = ⊤
⊢ ε * 1 < ε * 2

Tactic:
rw [ENNReal.mul_lt_mul_left hε.ne' hε_top]

Result:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ¬ε = ⊤
⊢ 1 < 2

Proof state:
case mp
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n < ε

Tactic:
obtain ⟨n, hn⟩ := h (min 1 (ε / 2))
  (lt_min_iff.mpr ⟨zero_lt_one, (ENNReal.div_pos_iff.mpr ⟨ne_of_gt hε, ENNReal.ofNat_ne_top⟩)⟩)

Result:
case mp.intro
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
⊢ ∃ n, f n < ε

Proof state:
case mpr
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε

Result:
case mpr.intro
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n < ε
⊢ ∃ n, f n ≤ ε

Proof state:
case mpr.intro
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n < ε
⊢ ∃ n, f n ≤ ε

Tactic:
exact ⟨n, hn.le⟩

Result:
no goals

Proof state:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ¬ε = ⊤
⊢ ε / 2 < ε

Tactic:
rw [ENNReal.div_lt_iff (Or.inr hε.ne') (Or.inr hε_top)]

Result:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ¬ε = ⊤
⊢ ε < ε * 2

Proof state:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ¬ε = ⊤
⊢ 1 ⊓ ε / 2 < ε

Tactic:
refine (min_le_right _ _).trans_lt ?_

Result:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ¬ε = ⊤
⊢ ε / 2 < ε

Proof state:
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ Tendsto f atTop (𝓝 0) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε

Tactic:
rw [ENNReal.tendsto_atTop_zero_iff_le_of_antitone hf]

Result:
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε

Proof state:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ¬ε = ⊤
⊢ ε < ε * 2

Tactic:
conv_lhs => rw [← mul_one ε]

Result:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ¬ε = ⊤
⊢ ε * 1 < ε * 2

Proof state:
case mp.intro
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
⊢ 1 ⊓ ε / 2 < ε

Tactic:
by_cases hε_top : ε = ∞

Result:
case pos
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ε = ⊤
⊢ 1 ⊓ ε / 2 < ε

case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ¬ε = ⊤
⊢ 1 ⊓ ε / 2 < ε

Proof state:
case pos
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ε = ⊤
⊢ 1 ⊓ ⊤ / 2 < ⊤

Tactic:
exact (min_le_left _ _).trans_lt ENNReal.one_lt_top

Result:
no goals

Proof state:
case pos
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ε = ⊤
⊢ 1 ⊓ ε / 2 < ε

Tactic:
rw [hε_top]

Result:
case pos
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ 1 ⊓ ε / 2
hε_top : ε = ⊤
⊢ 1 ⊓ ⊤ / 2 < ⊤

Proof state:
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε

Tactic:
constructor <;> intro h ε hε

Result:
case mp
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n < ε

case mpr
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n < ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n ≤ ε