-- Mathlib/Analysis/Normed/Group/ZeroAtInfty.lean
theorem ZeroAtInftyContinuousMapClass.norm_le (f : 𝓕) (ε : ℝ) (hε : 0 < ε) :
    ∃ (r : ℝ), ∀ (x : E) (_hx : r < ‖x‖), ‖f x‖ < ε

Proof state:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Tactic:
have h := zero_at_infty f

Result:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : Tendsto (⇑f) (cocompact E) (𝓝 0)
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Proof state:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Tactic:
rcases Metric.closedBall_compl_subset_of_mem_cocompact h 0 with ⟨r, hr⟩

Result:
case intro
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
r : ℝ
hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Proof state:
case h
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
r : ℝ
hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
x : E
hr' : r < ‖x‖
⊢ x ∈ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε

Tactic:
apply hr

Result:
case h.a
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
r : ℝ
hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
x : E
hr' : r < ‖x‖
⊢ x ∈ (Metric.closedBall 0 r)ᶜ

Proof state:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
r : ℝ
hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
x : E
hr' : r < ‖x‖
this : x ∈ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
⊢ ‖f x‖ < ε

Tactic:
aesop

Result:
no goals

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

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero, tendsto_def] at h

Result:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : ∀ s ∈ 𝓝 0, (fun x => ‖f x‖) ⁻¹' s ∈ cocompact E
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Proof state:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : ∀ s ∈ 𝓝 0, (fun x => ‖f x‖) ⁻¹' s ∈ cocompact E
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Tactic:
specialize h (Metric.ball 0 ε) (Metric.ball_mem_nhds 0 hε)

Result:
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
⊢ ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Proof state:
case h
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
r : ℝ
hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
⊢ ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Tactic:
intro x hr'

Result:
case h
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
r : ℝ
hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
x : E
hr' : r < ‖x‖
⊢ ‖f x‖ < ε

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

Tactic:
use r

Result:
case h
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
r : ℝ
hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
⊢ ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε

Proof state:
case h
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
r : ℝ
hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
x : E
hr' : r < ‖x‖
⊢ ‖f x‖ < ε

Tactic:
suffices x ∈ (fun x ↦ ‖f x‖) ⁻¹' Metric.ball 0 ε by aesop

Result:
case h
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
r : ℝ
hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
x : E
hr' : r < ‖x‖
⊢ x ∈ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε

Proof state:
case h.a
E : Type u_1
F : Type u_2
𝓕 : Type u_3
inst✝³ : SeminormedAddGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : FunLike 𝓕 E F
inst✝ : ZeroAtInftyContinuousMapClass 𝓕 E F
f : 𝓕
ε : ℝ
hε : 0 < ε
h : (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε ∈ cocompact E
r : ℝ
hr : (Metric.closedBall 0 r)ᶜ ⊆ (fun x => ‖f x‖) ⁻¹' Metric.ball 0 ε
x : E
hr' : r < ‖x‖
⊢ x ∈ (Metric.closedBall 0 r)ᶜ

Tactic:
aesop

Result:
no goals