-- Mathlib/Analysis/Normed/Group/ZeroAtInfty.lean
theorem zero_at_infty_of_norm_le (f : E → F)
    (h : ∀ (ε : ℝ) (_hε : 0 < ε), ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε) :
    Tendsto f (cocompact E) (𝓝 0)

Proof state:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
hs : s ∈ 𝓝 0
⊢ ∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s

Tactic:
rw [Metric.mem_nhds_iff] at hs

Result:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
hs : ∃ ε > 0, Metric.ball 0 ε ⊆ s
⊢ ∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s

Proof state:
case intro.intro
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
⊢ ∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s

Tactic:
rcases h ε hε with ⟨r, hr⟩

Result:
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ ∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s

Proof state:
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ ∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s

Tactic:
use r

Result:
case h
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s

Proof state:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ Tendsto f (cocompact E) (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Result:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ Tendsto (fun x => ‖f x‖) (cocompact E) (𝓝 0)

Proof state:
case h
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
a✝ : E
⊢ a✝ ∈ (Metric.closedBall 0 r)ᶜ → a✝ ∈ (fun x => ‖f x‖) ⁻¹' s

Tactic:
aesop

Result:
no goals

Proof state:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
hs : s ∈ 𝓝 0
⊢ s ∈ map (fun x => ‖f x‖) (cocompact E)

Tactic:
rw [mem_map, Metric.mem_cocompact_iff_closedBall_compl_subset 0]

Result:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
hs : s ∈ 𝓝 0
⊢ ∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s

Proof state:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ Tendsto (fun x => ‖f x‖) (cocompact E) (𝓝 0)

Tactic:
intro s hs

Result:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
hs : s ∈ 𝓝 0
⊢ s ∈ map (fun x => ‖f x‖) (cocompact E)

Proof state:
case h
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
⊢ (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s

Tactic:
intro

Result:
case h
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
r : ℝ
hr : ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
a✝ : E
⊢ a✝ ∈ (Metric.closedBall 0 r)ᶜ → a✝ ∈ (fun x => ‖f x‖) ⁻¹' s

Proof state:
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
hs : ∃ ε > 0, Metric.ball 0 ε ⊆ s
⊢ ∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s

Tactic:
rcases hs with ⟨ε, hε, hs⟩

Result:
case intro.intro
E : Type u_1
F : Type u_2
inst✝² : SeminormedAddGroup E
inst✝¹ : SeminormedAddCommGroup F
inst✝ : ProperSpace E
f : E → F
h : ∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε
s : Set ℝ
ε : ℝ
hε : ε > 0
hs : Metric.ball 0 ε ⊆ s
⊢ ∃ r, (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' s