-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem tendsto_approxBounded_of_norm_le {β} {f : α → β} [NormedAddCommGroup β] [NormedSpace ℝ β]
    {m : MeasurableSpace α} (hf : StronglyMeasurable[m] f) {c : ℝ} {x : α} (hfx : ‖f x‖ ≤ c) :
    Tendsto (fun n => hf.approxBounded c n x) atTop (𝓝 (f x))

Proof state:
case pos
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ‖f x‖ = 0
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))

Tactic:
rw [norm_eq_zero] at hfx0

Result:
case pos
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : f x = 0
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))

Proof state:
case neg
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
this : 1 ⊓ c / ‖f x‖ = 1
⊢ Tendsto (fun n => c / ‖(hf.approx n) x‖) atTop (𝓝 (c / ‖f x‖))

Tactic:
exact Tendsto.div tendsto_const_nhds h_tendsto.norm hfx0

Result:
no goals

Proof state:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖(hf.approx n) x‖) atTop (𝓝 0)
n : ℕ
⊢ ‖1 ⊓ c / ‖(hf.approx n) x‖‖ ≤ ‖1‖

Tactic:
rw [norm_one, Real.norm_of_nonneg]

Result:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖(hf.approx n) x‖) atTop (𝓝 0)
n : ℕ
⊢ 1 ⊓ c / ‖(hf.approx n) x‖ ≤ 1

α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖(hf.approx n) x‖) atTop (𝓝 0)
n : ℕ
⊢ 0 ≤ 1 ⊓ c / ‖(hf.approx n) x‖

Proof state:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))

Tactic:
by_cases hfx0 : ‖f x‖ = 0

Result:
case pos
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ‖f x‖ = 0
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))

case neg
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))

Proof state:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ ‖f x‖ ≤ c

Tactic:
exact hfx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖(hf.approx n) x‖) atTop (𝓝 0)
n : ℕ
⊢ ‖1‖ * ‖(hf.approx n) x‖ = ‖(hf.approx n) x‖

Tactic:
rw [norm_one, one_mul]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖(hf.approx n) x‖) atTop (𝓝 0)
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 0)

Tactic:
refine squeeze_zero_norm (fun n => ?_) h_tendsto_norm

Result:
case pos
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖(hf.approx n) x‖) atTop (𝓝 0)
n : ℕ
⊢ ‖(1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x‖ ≤ ‖(hf.approx n) x‖

Proof state:
case neg
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
this : 1 ⊓ c / ‖f x‖ = 1
⊢ Tendsto (fun n => 1 ⊓ c / ‖(hf.approx n) x‖) atTop (𝓝 1)

Tactic:
nth_rw 2 [this.symm]

Result:
case neg
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
this : 1 ⊓ c / ‖f x‖ = 1
⊢ Tendsto (fun n => 1 ⊓ c / ‖(hf.approx n) x‖) atTop (𝓝 (1 ⊓ c / ‖f x‖))

Proof state:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (fun n => ‖(hf.approx n) x‖) atTop (𝓝 0)
n : ℕ
⊢ 0 ≤ 1 ⊓ c / ‖(hf.approx n) x‖

Tactic:
exact le_min zero_le_one (div_nonneg ((norm_nonneg _).trans hfx) (norm_nonneg _))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
⊢ Tendsto (fun n => ‖(hf.approx n) x‖) atTop (𝓝 0)

Tactic:
convert h_tendsto.norm

Result:
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 0)
hfx0 : f x = 0
⊢ 0 = ‖0‖

Proof state:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ 1 ⊓ c / ‖f x‖ = 1

Tactic:
rw [min_eq_left_iff, one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm hfx0))]

Result:
α : Type u_1
β : Type u_5
f : α → β
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
⊢ ‖f x‖ ≤ c