-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem tendsto_normalize_iff_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
    (nonzero : μ ≠ 0) :
    Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize) ∧
        Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass) ↔
      Tendsto μs F (𝓝 μ)

Proof state:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass) ↔
    Tendsto μs F (𝓝 μ)

Tactic:
constructor

Result:
case mp
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass) →
    Tendsto μs F (𝓝 μ)

case mpr
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto μs F (𝓝 μ) →
    Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)

Proof state:
case mp
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass) →
    Tendsto μs F (𝓝 μ)

Tactic:
rintro ⟨normalized_lim, mass_lim⟩

Result:
case mp.intro
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
normalized_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)
⊢ Tendsto μs F (𝓝 μ)

Proof state:
case mp.intro
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
normalized_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)
⊢ Tendsto μs F (𝓝 μ)

Tactic:
exact tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass normalized_lim mass_lim

Result:
no goals

Proof state:
case mpr
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
μs_lim : Tendsto μs F (𝓝 μ)
⊢ Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)

Tactic:
exact ⟨tendsto_normalize_of_tendsto μs_lim nonzero, μs_lim.mass⟩

Result:
no goals

Proof state:
case mpr
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ Tendsto μs F (𝓝 μ) →
    Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)

Tactic:
intro μs_lim

Result:
case mpr
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
nonzero : μ ≠ 0
μs_lim : Tendsto μs F (𝓝 μ)
⊢ Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize) ∧ Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)