-- 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 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‖) atTop (𝓝 1)

Tactic:
have : min 1 (c / ‖f x‖) = 1 := by
  rw [min_eq_left_iff, one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm hfx0))]
  exact hfx

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)

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‖‖ * ‖(hf.approx n) x‖ ≤ ‖1‖ * ‖(hf.approx n) x‖

Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_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‖

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 => (hf.approxBounded c n) x) atTop (𝓝 (f x))

Tactic:
simp only [StronglyMeasurable.approxBounded, SimpleFunc.coe_map, Function.comp_apply]

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))
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx 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 (𝓝 0)
hfx0 : f x = 0
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 0)

Tactic:
have h_tendsto_norm : Tendsto (fun n => ‖hf.approx n x‖) atTop (𝓝 0) := by
  convert h_tendsto.norm
  rw [norm_zero]

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)
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 0)

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 ⊓ c / ‖f x‖))

Tactic:
refine Tendsto.min tendsto_const_nhds ?_

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 => c / ‖(hf.approx n) x‖) atTop (𝓝 (c / ‖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
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (f x))

Tactic:
rw [← one_smul ℝ (f x)]

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
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (1 • 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
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 (1 • f x))

Tactic:
refine Tendsto.smul ?_ h_tendsto

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
⊢ Tendsto (fun n => 1 ⊓ c / ‖(hf.approx n) x‖) atTop (𝓝 1)

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 [hfx0] at h_tendsto ⊢

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
⊢ Tendsto (fun n => (1 ⊓ c / ‖(hf.approx n) x‖) • (hf.approx n) x) atTop (𝓝 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
⊢ Tendsto (fun n => (hf.approxBounded c n) x) atTop (𝓝 (f x))

Tactic:
have h_tendsto := hf.tendsto_approx x

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))
⊢ Tendsto (fun n => (hf.approxBounded c n) x) atTop (𝓝 (f x))

Proof state:
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‖

Tactic:
rw [norm_zero]

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:
exact min_le_left _ _

Result:
no goals