awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous[instTopologicalSpace, _]
    ((fun (φ : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) ↦ (φ : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f) ∘ toWeakDualBCNN)
have refine : Continuous (Y := ℝ≥0) fun (φ : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) ↦ (φ : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f
Tactic: refine Continuous.comp ?_ (toWeakDualBCNN_continuous (Ω := Ω))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure Ω) ↦ μ.mass
have simp_rw : Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure Ω) ↦ μ.testAgainstNN 1
Tactic: simp_rw [← testAgainstNN_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (β := ℝ≥0)
        (fun (i : γ) ↦ ((((μs i).toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)) F
        (𝓝 (((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f) : Filter ℝ≥0)
have rw : (∀ (y : Ω →ᵇ ℝ≥0),
    Tendsto (β := ℝ≥0)
      (fun (i : γ) ↦
        ((((topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0) : (a : (Ω →ᵇ ℝ≥0) →L[ℝ≥0] ℝ≥0) → (Ω →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0)
                  (μs i).toWeakDualBCNN :
                (Ω →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) :
              (a : Ω →ᵇ ℝ≥0) → ℝ≥0)
            y :
          ℝ≥0))
      F
      (𝓝
          ((((topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0) : (a : (Ω →ᵇ ℝ≥0) →L[ℝ≥0] ℝ≥0) → (Ω →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) μ.toWeakDualBCNN :
                (Ω →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0) :
              (a : Ω →ᵇ ℝ≥0) → ℝ≥0)
            y) :
        Filter ℝ≥0)) ↔
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (β := ℝ≥0)
      (fun (i : γ) ↦ ((((μs i).toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)) F
      (𝓝 (((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f) : Filter ℝ≥0)
Tactic: rw [tendsto_iff_weakDual_tendsto, tendsto_iff_forall_eval_tendsto_topDualPairing]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
have rw : (∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (β := ℝ≥0)
      (fun (i : γ) ↦ ((((μs i).toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)) F
      (𝓝 (((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f) : Filter ℝ≥0)) ↔
  ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
Tactic: rw [FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 0)
have apply : Tendsto (β := ℝ) (fun (b : γ) ↦ dist ((μs b).testAgainstNN f) 0) F (𝓝 0)
Tactic: apply tendsto_iff_dist_tendsto_zero.mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (β := ℝ) (fun (b : γ) ↦ dist ((μs b).testAgainstNN f) 0) F (𝓝 0)
have obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ (μs i).testAgainstNN 0 + nndist f 0 * (μs i).mass
Tactic: have obs := fun i ↦ (μs i).testAgainstNN_lipschitz_estimate f 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (β := ℝ≥0) (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)
have obs₁ : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
Tactic: simp_rw [testAgainstNN_zero, zero_add] at obs
Cleared hypotheses: obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (β := ℝ≥0) (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)
have simp_rw : Tendsto (β := ℝ) (fun (b : γ) ↦ (↑((μs b).testAgainstNN f) : ℝ)) 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', imp_true_iff]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (β := ℝ≥0) (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)
have apply : Tendsto (β := ℝ) (fun (t : γ) ↦ (↑(nndist f 0 * (μs t).mass) : ℝ)) F (𝓝 0)
Tactic: apply squeeze_zero (fun i ↦ NNReal.coe_nonneg _) obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
obs : ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass
⊢ Tendsto (β := ℝ) (fun (t : γ) ↦ (↑(nndist f 0 * (μs t).mass) : ℝ)) F (𝓝 0)
have lim_pair : Tendsto (β := ℝ × ℝ) (fun (i : γ) ↦ ((↑(nndist f 0) : ℝ), (↑(μs i).mass : ℝ))) F (𝓝 ((↑(nndist f 0) : ℝ), 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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).mass) F (𝓝 0)
⊢ Tendsto μs F (𝓝 0)
have rw : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))
Tactic: rw [tendsto_iff_forall_testAgainstNN_tendsto]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))
have h : testAgainstNN 0 f = 0
Tactic: convert! tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
mass_lim : Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).mass) F (𝓝 0)
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0
have h : Eq (α := ℝ≥0) 0 0
Tactic: rw [zero_testAgainstNN_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
have rw : (∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (β := ℝ≥0)
      (fun (i : γ) ↦ ((((μs i).toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)) F
      (𝓝 (((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f) : Filter ℝ≥0)) ↔
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
Tactic: rw [tendsto_iff_forall_toWeakDualBCNN_tendsto]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (β := ℝ≥0)
        (fun (i : γ) ↦ ((((μs i).toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)) F
        (𝓝 (((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f) : Filter ℝ≥0)) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
have simp_rw : (∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toNNReal) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toNNReal)) ↔
  ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
Tactic: simp_rw [toWeakDualBCNN_apply _ _, ← testAgainstNN_coe_eq, ENNReal.tendsto_coe,
    ENNReal.toNNReal_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
simp_rw :
  (∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toNNReal) F
        (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toNNReal)) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
⊢ (∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (β := ℝ≥0)
        (fun (i : γ) ↦ ((((μs i).toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)) F
        (𝓝 (((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f) : Filter ℝ≥0)) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
have simp_rw₁ : (∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ (↑((μs i).testAgainstNN f) : ℝ≥0∞).toNNReal) F (𝓝 (↑(μ.testAgainstNN f) : ℝ≥0∞).toNNReal)) ↔
  ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (↑((μs i).testAgainstNN f) : ℝ≥0∞)) F (𝓝 (↑(μ.testAgainstNN f) : ℝ≥0∞))
Tactic: simp_rw [toWeakDualBCNN_apply _ _, ← testAgainstNN_coe_eq, ENNReal.tendsto_coe,
    ENNReal.toNNReal_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
simp_rw :
  (∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)).toNNReal) F
        (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toNNReal)) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
simp_rw₁ :
  (∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ (↑((μs i).testAgainstNN f) : ℝ≥0∞).toNNReal) F
        (𝓝 (↑(μ.testAgainstNN f) : ℝ≥0∞).toNNReal)) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (↑((μs i).testAgainstNN f) : ℝ≥0∞)) F (𝓝 (↑(μ.testAgainstNN f) : ℝ≥0∞))
⊢ (∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (β := ℝ≥0)
        (fun (i : γ) ↦ ((((μs i).toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)) F
        (𝓝 (((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f) : Filter ℝ≥0)) ↔
    ∀ (f : Ω →ᵇ ℝ≥0),
      Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
have simp_rw₂ : (∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun (i : γ) ↦ (↑((μs i).testAgainstNN f) : ℝ≥0∞).toNNReal) F (𝓝 (↑(μ.testAgainstNN f) : ℝ≥0∞).toNNReal)) ↔
  ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (a : γ) ↦ (μs a).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
Tactic: simp_rw [toWeakDualBCNN_apply _ _, ← testAgainstNN_coe_eq, ENNReal.tendsto_coe,
    ENNReal.toNNReal_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : Eq (α := WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) μ.toWeakDualBCNN ν.toWeakDualBCNN
⊢ μ = ν
have h : ∀ (f : Ω →ᵇ ℝ≥0),
  ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
Tactic: apply ext_of_forall_lintegral_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : Eq (α := WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) μ.toWeakDualBCNN ν.toWeakDualBCNN
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
have key : Eq (α := ℝ≥0) (((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)
  (((ν.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)
Tactic: have key := congr_fun (congrArg DFunLike.coe hμν) f
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : Eq (α := WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) μ.toWeakDualBCNN ν.toWeakDualBCNN
f : Ω →ᵇ ℝ≥0
key :
  Eq (α := ℝ≥0) (((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)
    (((ν.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)
⊢ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
have apply : ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≠ ∞
Tactic: apply (ENNReal.toNNReal_eq_toNNReal_iff' ?_ ?_).mp key
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : Eq (α := WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) μ.toWeakDualBCNN ν.toWeakDualBCNN
f : Ω →ᵇ ℝ≥0
key :
  Eq (α := ℝ≥0) (((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)
    (((ν.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f : ℝ≥0)
apply : ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≠ ∞
⊢ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
have apply₁ : ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω) ≠ ∞
Tactic: apply (ENNReal.toNNReal_eq_toNNReal_iff' ?_ ?_).mp key
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : FiniteMeasure Ω
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂(↑μ : Measure Ω), (fs i : (a : Ω) → ℝ≥0) ω ≤ c
f : Ω →ᵇ ℝ≥0
fs_lim :
  ∀ᵐ (ω : Ω) ∂(↑μ : Measure Ω),
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ((fs i : (a : Ω) → ℝ≥0) ω : ℝ≥0)) L (𝓝 ((f : (a : Ω) → ℝ≥0) ω) : Filter ℝ≥0)
⊢ Tendsto (fun (i : ι) ↦ μ.testAgainstNN (fs i)) L (𝓝 (μ.testAgainstNN f))
have apply : Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((fs i : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) L
  (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
Tactic: apply (ENNReal.tendsto_toNNReal (f.lintegral_lt_top_of_nnreal (μ : Measure Ω)).ne).comp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
⊢ Tendsto μs F (𝓝 μ)
have apply : ∀ (f : Ω →ᵇ ℝ≥0),
  Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
Tactic: apply tendsto_iff_forall_lintegral_tendsto.mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun (i : γ) ↦ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs i) : Measure Ω)) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
have apply : Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
  (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
Tactic: apply (ENNReal.tendsto_toReal_iff (fi := F)
      (fun i ↦ (f.lintegral_lt_top_of_nnreal (μs i)).ne) (f.lintegral_lt_top_of_nnreal μ).ne).mp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
have lip : LipschitzWith 1 NNReal.toReal
Tactic: have lip : LipschitzWith 1 ((↑) : ℝ≥0 → ℝ) := NNReal.isometry_coe.lipschitz
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
have _def_f₀ : let f₀ := comp NNReal.toReal lip f;
f₀ = comp NNReal.toReal lip f
Tactic: set f₀ := BoundedContinuousFunction.comp _ lip f with _def_f₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
have f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
Tactic: have f₀_eq : ⇑f₀ = ((↑) : ℝ≥0 → ℝ) ∘ ⇑f := rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
have f₀_nn : LE.le (α := (a : Ω) → ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
Tactic: have f₀_nn : 0 ≤ ⇑f₀ := fun _ ↦ by
    simp only [f₀_eq, Pi.zero_apply, Function.comp_apply, NNReal.zero_le_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)))
f : Ω →ᵇ ℝ≥0
lip : LipschitzWith 1 NNReal.toReal
f₀ : Ω →ᵇ ℝ := comp NNReal.toReal lip f
_def_f₀ : f₀ = comp NNReal.toReal lip f
f₀_eq : Eq (α := (a : Ω) → ℝ) (⇑f₀ : (a : Ω) → ℝ) (NNReal.toReal ∘ (⇑f : (a : Ω) → ℝ≥0))
f₀_nn : LE.le (α := (a : Ω) → ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
⊢ Tendsto (fun (n : γ) ↦ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑(μs n) : Measure Ω)).toReal) F
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal)
have f₀_ae_nn : (ae (↑μ : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f₀ : (a : Ω) → ℝ)
Tactic: have f₀_ae_nn : 0 ≤ᵐ[(μ : Measure Ω)] ⇑f₀ := .of_forall f₀_nn