-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem tendsto_zero_testAgainstNN_of_tendsto_zero_mass {γ : Type*} {F : Filter γ}
    {μs : γ → FiniteMeasure Ω} (mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 0)) (f : Ω →ᵇ ℝ≥0) :
    Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 0)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 0)

Tactic:
apply tendsto_iff_dist_tendsto_zero.mpr

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun b => dist ((μs b).testAgainstNN f) 0) F (𝓝 0)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun b => dist ((μs b).testAgainstNN f) 0) F (𝓝 0)

Tactic:
have obs := fun i ↦ (μs i).testAgainstNN_lipschitz_estimate f 0

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ (μs i).testAgainstNN 0 + nndist f 0 * (μs i).mass
⊢ Tendsto (fun b => dist ((μs b).testAgainstNN f) 0) F (𝓝 0)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
⊢ Tendsto (fun t => (fun a => ↑a) (nndist f 0 * (μs t).mass)) F (𝓝 0)

Tactic:
have lim_pair : Tendsto (fun i ↦ (⟨nndist f 0, (μs i).mass⟩ : ℝ × ℝ)) F (𝓝 ⟨nndist f 0, 0⟩) :=
  (Prod.tendsto_iff _ _).mpr ⟨tendsto_const_nhds, (NNReal.continuous_coe.tendsto 0).comp mass_lim⟩

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
lim_pair : Tendsto (fun i => (↑(nndist f 0), ↑(μs i).mass)) F (𝓝 (↑(nndist f 0), 0))
⊢ Tendsto (fun t => (fun a => ↑a) (nndist f 0 * (μs t).mass)) F (𝓝 0)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ (μs i).testAgainstNN 0 + nndist f 0 * (μs i).mass
⊢ Tendsto (fun b => dist ((μs b).testAgainstNN f) 0) F (𝓝 0)

Tactic:
simp_rw [testAgainstNN_zero, zero_add] at obs

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
⊢ Tendsto (fun b => dist ((μs b).testAgainstNN f) 0) F (𝓝 0)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
lim_pair : Tendsto (fun i => (↑(nndist f 0), ↑(μs i).mass)) F (𝓝 (↑(nndist f 0), 0))
⊢ Tendsto (fun t => (fun a => ↑a) (nndist f 0 * (μs t).mass)) F (𝓝 0)

Tactic:
simpa using tendsto_mul.comp lim_pair

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
⊢ Tendsto (fun b => dist ((μs b).testAgainstNN f) 0) F (𝓝 0)

Tactic:
simp_rw [show ∀ i, dist ((μs i).testAgainstNN f) 0 = (μs i).testAgainstNN f by
    simp only [dist_nndist, NNReal.nndist_zero_eq_val', eq_self_iff_true, imp_true_iff]]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
⊢ Tendsto (fun b => ↑((μs b).testAgainstNN f)) F (𝓝 0)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
⊢ Tendsto (fun b => ↑((μs b).testAgainstNN f)) F (𝓝 0)

Tactic:
apply squeeze_zero (fun i ↦ NNReal.coe_nonneg _) obs

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
⊢ Tendsto (fun t => (fun a => ↑a) (nndist f 0 * (μs t).mass)) F (𝓝 0)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
⊢ ∀ (i : γ), dist ((μs i).testAgainstNN f) 0 = ↑((μs i).testAgainstNN f)

Tactic:
simp only [dist_nndist, NNReal.nndist_zero_eq_val', eq_self_iff_true, imp_true_iff]

Result:
no goals