awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
simp_rw : Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure Ω) ↦ μ.testAgainstNN 1
⊢ Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure Ω) ↦ μ.mass

Tactic:
simp_rw [← testAgainstNN_one]

Premises used: MeasureTheory.FiniteMeasure.testAgainstNN_one
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure Ω) ↦ μ.testAgainstNN 1

Tactic:
continuous_testAgainstNN_eval 1

Premises used: MeasureTheory.FiniteMeasure.continuous_testAgainstNN_eval, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure Ω) ↦ μ.testAgainstNN 1

Tactic:
exact continuous_testAgainstNN_eval 1

Premises used: MeasureTheory.FiniteMeasure.continuous_testAgainstNN_eval, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
h : Tendsto μs F (𝓝 μ)
⊢ Tendsto (fun (i : γ) ↦ (μs i).mass) F (𝓝 μ.mass)

Tactic:
(continuous_mass.tendsto μ).comp h

Premises used: MeasureTheory.FiniteMeasure.mass, Continuous.tendsto, MeasureTheory.FiniteMeasure.continuous_mass, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔
    Tendsto (β := WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) (fun (i : γ) ↦ (μs i).toWeakDualBCNN) F (𝓝 μ.toWeakDualBCNN)

Tactic:
IsInducing.tendsto_nhds_iff ⟨rfl⟩

Premises used: Topology.IsInducing.tendsto_nhds_iff, Topology.IsInducing.mk, MeasureTheory.FiniteMeasure.toWeakDualBCNN, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
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)
⊢ 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)

Tactic:
rw [tendsto_iff_weakDual_tendsto, tendsto_iff_forall_eval_tendsto_topDualPairing]

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendsto, tendsto_iff_forall_eval_tendsto_topDualPairing
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (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:
rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
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))
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
rw [FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto]

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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 : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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
apply : Tendsto (β := ℝ) (fun (b : γ) ↦ dist ((μs b).testAgainstNN f) 0) F (𝓝 0)
⊢ Tendsto (β := ℝ≥0) (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 0)

Tactic:
apply tendsto_iff_dist_tendsto_zero.mpr

Premises used: Iff.mpr, tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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
⊢ ∀ (i : γ), (μs i).testAgainstNN f ≤ nndist f 0 * (μs i).mass

Tactic:
simp_rw [testAgainstNN_zero, zero_add] at obs

Premises used: zero_add, MeasureTheory.FiniteMeasure.testAgainstNN_zero
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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
⊢ ∀ (i : γ), dist ((μs i).testAgainstNN f) 0 = (↑((μs i).testAgainstNN f) : ℝ)

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

Premises used: dist_nndist, imp_true_iff, NNReal.nndist_zero_eq_val'
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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
simp_rw : Tendsto (β := ℝ) (fun (b : γ) ↦ (↑((μs b).testAgainstNN f) : ℝ)) F (𝓝 0)
⊢ 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', imp_true_iff]]
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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
apply : Tendsto (β := ℝ) (fun (t : γ) ↦ (↑(nndist f 0 * (μs t).mass) : ℝ)) F (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (b : γ) ↦ (↑((μs b).testAgainstNN f) : ℝ)) F (𝓝 0)

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

Premises used: squeeze_zero, NNReal.coe_nonneg
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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 (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⟩
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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
lim_pair : Tendsto (β := ℝ × ℝ) (fun (i : γ) ↦ ((↑(nndist f 0) : ℝ), (↑(μs i).mass : ℝ))) F (𝓝 ((↑(nndist f 0) : ℝ), 0))
⊢ Tendsto (β := ℝ) (fun (t : γ) ↦ (↑(nndist f 0 * (μs t).mass) : ℝ)) F (𝓝 0)

Tactic:
simpa using tendsto_mul.comp lim_pair

Premises used: tendsto_mul, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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)
rw : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))
⊢ Tendsto μs F (𝓝 0)

Tactic:
rw [tendsto_iff_forall_testAgainstNN_tendsto]

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_testAgainstNN_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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)

Tactic:
tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f

Premises used: MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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
h : testAgainstNN 0 f = 0
⊢ Tendsto (fun (i : γ) ↦ (μs i).testAgainstNN f) F (𝓝 (testAgainstNN 0 f))

Tactic:
convert! tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f

Premises used: MeasureTheory.FiniteMeasure.tendsto_zero_testAgainstNN_of_tendsto_zero_mass
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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
h h₁ : Eq (α := ℝ≥0) 0 0
⊢ testAgainstNN 0 f = 0

Tactic:
rw [zero_testAgainstNN_apply]

Premises used: MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
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 Ω)))
⊢ 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 Ω)))

Tactic:
rw [tendsto_iff_forall_toWeakDualBCNN_tendsto]

Premises used: MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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∞))
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))
⊢ (∀ (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:
simp_rw [toWeakDualBCNN_apply _ _, ← testAgainstNN_coe_eq, ENNReal.tendsto_coe,
    ENNReal.toNNReal_coe]

Premises used: MeasureTheory.FiniteMeasure.toWeakDualBCNN_apply, ENNReal.toNNReal_coe, MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq, ENNReal.tendsto_coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s t : Set Ω
R : Type u_2
inst_1 : SMul R ℝ≥0
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_5 : TopologicalSpace Ω
inst_6 : OpensMeasurableSpace Ω
⊢ R1Space.{u_1} (FiniteMeasure Ω)

Tactic:
IsInducing.r1Space (f := toWeakDualBCNN) ⟨rfl⟩

Premises used: Topology.IsInducing.r1Space, Topology.IsInducing.mk, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
hμν : Eq (α := WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) μ.toWeakDualBCNN ν.toWeakDualBCNN
h :
  ∀ (f : Ω →ᵇ ℝ≥0),
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
      ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
⊢ μ = ν

Tactic:
apply ext_of_forall_lintegral_eq

Premises used: MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eq
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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 Ω) ≠ ∞
apply₁ : ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω) ≠ ∞
⊢ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)

Tactic:
apply (ENNReal.toNNReal_eq_toNNReal_iff' ?_ ?_).mp key

Premises used: ENNReal.toNNReal_eq_toNNReal_iff', Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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)
⊢ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≠ ∞

Tactic:
(lintegral_lt_top_of_nnreal μ f).ne

Premises used: BoundedContinuousFunction.lintegral_lt_top_of_nnreal, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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)
⊢ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≠ ∞

Tactic:
exact (lintegral_lt_top_of_nnreal μ f).ne

Premises used: BoundedContinuousFunction.lintegral_lt_top_of_nnreal, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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)
⊢ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω) ≠ ∞

Tactic:
(lintegral_lt_top_of_nnreal ν f).ne

Premises used: BoundedContinuousFunction.lintegral_lt_top_of_nnreal, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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)
⊢ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑ν : Measure Ω) ≠ ∞

Tactic:
exact (lintegral_lt_top_of_nnreal ν f).ne

Premises used: BoundedContinuousFunction.lintegral_lt_top_of_nnreal, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s t : Set Ω
R : Type u_2
inst_1 : SMul R ℝ≥0
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_5 : TopologicalSpace Ω
inst_6 : HasOuterApproxClosed Ω
inst_7 : BorelSpace Ω
⊢ T2Space.{u_1} (FiniteMeasure Ω)

Tactic:
(isEmbedding_toWeakDualBCNN Ω).t2Space

Premises used: MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN, Topology.IsEmbedding.t2Space
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
fs : ℕ → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ (n : ℕ) (ω : Ω), (fs n : (a : Ω) → ℝ≥0) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ (ω : Ω), Tendsto (fun (n : ℕ) ↦ (fs n : (a : Ω) → ℝ≥0) ω) atTop (𝓝 (f ω))
⊢ Tendsto (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) atTop
    (𝓝 (∫⁻ (ω : Ω), (↑(f ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)))

Tactic:
tendsto_lintegral_nn_filter_of_le_const μ
    (.of_forall fun n ↦ .of_forall (fs_le_const n))
    (.of_forall fs_lim)

Premises used: Filter.Eventually.of_forall, MeasureTheory.tendsto_lintegral_nn_filter_of_le_const
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
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)
apply :
  Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((fs i : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)) L
    (𝓝 (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)))
⊢ Tendsto (fun (i : ι) ↦ μ.testAgainstNN (fs i)) L (𝓝 (μ.testAgainstNN f))

Tactic:
apply (ENNReal.tendsto_toNNReal (f.lintegral_lt_top_of_nnreal (μ : Measure Ω)).ne).comp

Premises used: BoundedContinuousFunction.lintegral_lt_top_of_nnreal, ENNReal.tendsto_toNNReal, Filter.Tendsto.comp, MeasureTheory.FiniteMeasure.toMeasure, LT.lt.ne