awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 f = 0

Tactic:
simp only [testAgainstNN, toMeasure_zero, lintegral_zero_measure, ENNReal.toNNReal_zero]

Premises used: MeasureTheory.FiniteMeasure.testAgainstNN, MeasureTheory.lintegral_zero_measure, MeasureTheory.FiniteMeasure.toMeasure_zero, ENNReal.toNNReal_zero
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
h : ∀ (x : Ω →ᵇ ℝ≥0), testAgainstNN 0 x = 0 x
⊢ Eq.{u_1 + 1} (α := (f : Ω →ᵇ ℝ≥0) → ℝ≥0) (testAgainstNN 0) 0

Tactic:
funext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
x : Ω →ᵇ ℝ≥0
⊢ testAgainstNN 0 x = 0 x

Tactic:
simp only [zero_testAgainstNN_apply, Pi.zero_apply]

Premises used: MeasureTheory.FiniteMeasure.zero_testAgainstNN_apply, Pi.zero_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
c : ℝ≥0
μ : FiniteMeasure Ω
f : Ω →ᵇ ℝ≥0
⊢ (c • μ).testAgainstNN f = c • μ.testAgainstNN f

Tactic:
simp only [testAgainstNN, toMeasure_smul, smul_eq_mul, ← ENNReal.smul_toNNReal, ENNReal.smul_def,
    lintegral_smul_measure]

Premises used: MeasureTheory.lintegral_smul_measure, ENNReal.smul_def, MeasureTheory.FiniteMeasure.testAgainstNN, ENNReal.smul_toNNReal, MeasureTheory.FiniteMeasure.toMeasure_smul, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
simp :
  ∫⁻ (ω : Ω), (↑((f₁ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + (↑((f₂ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    ∫⁻ (ω : Ω), (↑((f₁ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) +
      ∫⁻ (ω : Ω), (↑((f₂ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)
⊢ μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂

Tactic:
simp only [← ENNReal.coe_inj, BoundedContinuousFunction.coe_add, ENNReal.coe_add, Pi.add_apply,
    testAgainstNN_coe_eq]

Premises used: ENNReal.coe_inj, MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq, ENNReal.coe_add, BoundedContinuousFunction.coe_add, Pi.add_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), (↑((f₁ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + (↑((f₂ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    ∫⁻ (ω : Ω), (↑((f₁ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) +
      ∫⁻ (ω : Ω), (↑((f₂ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)

Tactic:
lintegral_add_left (BoundedContinuousFunction.measurable_coe_ennreal_comp _) _

Premises used: MeasureTheory.lintegral_add_left, BoundedContinuousFunction.measurable_coe_ennreal_comp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), (↑((f₁ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + (↑((f₂ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    ∫⁻ (ω : Ω), (↑((f₁ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) +
      ∫⁻ (ω : Ω), (↑((f₂ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)

Tactic:
exact lintegral_add_left (BoundedContinuousFunction.measurable_coe_ennreal_comp _) _

Premises used: MeasureTheory.lintegral_add_left, BoundedContinuousFunction.measurable_coe_ennreal_comp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
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 Ω
inst_7 : IsScalarTower R ℝ≥0 ℝ≥0
inst_8 : PseudoMetricSpace R
inst_9 : Zero R
inst_10 : IsBoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
simp :
  ∫⁻ (ω : Ω), c • (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    c • ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)
⊢ μ.testAgainstNN (c • f) = c • μ.testAgainstNN f

Tactic:
simp only [← ENNReal.coe_inj, BoundedContinuousFunction.coe_smul, testAgainstNN_coe_eq,
    ENNReal.coe_smul]

Premises used: ENNReal.coe_inj, BoundedContinuousFunction.coe_smul, MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq, ENNReal.coe_smul
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
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 Ω
inst_7 : IsScalarTower R ℝ≥0 ℝ≥0
inst_8 : PseudoMetricSpace R
inst_9 : Zero R
inst_10 : IsBoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
simp_rw :
  ∫⁻ (ω : Ω), HSMul.hSMul (β := ℝ≥0∞) c 1 * (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    HSMul.hSMul (β := ℝ≥0∞) c 1 * ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)
⊢ ∫⁻ (ω : Ω), c • (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    c • ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)

Tactic:
simp_rw [← smul_one_smul ℝ≥0∞ c (f _ : ℝ≥0∞), ← smul_one_smul ℝ≥0∞ c (lintegral _ _ : ℝ≥0∞),
    smul_eq_mul]

Premises used: ENNReal.ofNNReal, smul_one_smul, ENNReal, smul_eq_mul, DFunLike.coe, MeasureTheory.lintegral
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
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 Ω
inst_7 : IsScalarTower R ℝ≥0 ℝ≥0
inst_8 : PseudoMetricSpace R
inst_9 : Zero R
inst_10 : IsBoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), HSMul.hSMul (β := ℝ≥0∞) c 1 * (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    HSMul.hSMul (β := ℝ≥0∞) c 1 * ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)

Tactic:
lintegral_const_mul (c • (1 : ℝ≥0∞)) f.measurable_coe_ennreal_comp

Premises used: BoundedContinuousFunction.measurable_coe_ennreal_comp, HSMul.hSMul, OfNat.ofNat, MeasureTheory.lintegral_const_mul
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
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 Ω
inst_7 : IsScalarTower R ℝ≥0 ℝ≥0
inst_8 : PseudoMetricSpace R
inst_9 : Zero R
inst_10 : IsBoundedSMul R ℝ≥0
μ : FiniteMeasure Ω
c : R
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), HSMul.hSMul (β := ℝ≥0∞) c 1 * (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    HSMul.hSMul (β := ℝ≥0∞) c 1 * ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)

Tactic:
exact lintegral_const_mul (c • (1 : ℝ≥0∞)) f.measurable_coe_ennreal_comp

Premises used: BoundedContinuousFunction.measurable_coe_ennreal_comp, HSMul.hSMul, OfNat.ofNat, MeasureTheory.lintegral_const_mul
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
simp :
  ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≤
    ∫⁻ (ω : Ω), (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + edist f g ∂(↑μ : Measure Ω)
⊢ μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass

Tactic:
simp only [← μ.testAgainstNN_const (nndist f g), ← testAgainstNN_add, ← ENNReal.coe_le_coe,
    BoundedContinuousFunction.coe_add, const_apply, ENNReal.coe_add, Pi.add_apply,
    coe_nnreal_ennreal_nndist, testAgainstNN_coe_eq]

Premises used: NNDist.nndist, MeasureTheory.FiniteMeasure.testAgainstNN_const, MeasureTheory.FiniteMeasure.testAgainstNN_coe_eq, ENNReal.coe_le_coe, coe_nnreal_ennreal_nndist, MeasureTheory.FiniteMeasure.testAgainstNN_add, ENNReal.coe_add, BoundedContinuousFunction.coe_add, Pi.add_apply, BoundedContinuousFunction.const_apply
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
hfg :
  LE.le.{u_1} (α := Ω → ℝ≥0∞) (fun (a : Ω) ↦ (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) fun (a : Ω) ↦
    (↑((g : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) + edist f g
⊢ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≤
    ∫⁻ (ω : Ω), (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + edist f g ∂(↑μ : Measure Ω)

Tactic:
apply lintegral_mono

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ ∀ (ω : Ω), dist (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) ω : ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) ≤ (↑(nndist f g) : ℝ)

Tactic:
have le_dist : ∀ ω, dist (f ω) (g ω) ≤ nndist f g := BoundedContinuousFunction.dist_coe_le_dist
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) ω : ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) ≤ (↑(nndist f g) : ℝ)
ω : Ω
⊢ (f : (a : Ω) → ℝ≥0) ω ≤
    HAdd.hAdd (α := ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0)
      (nndist (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) ω : ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0))

Tactic:
NNReal.le_add_nndist (f ω) (g ω)

Premises used: NNReal.le_add_nndist, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) ω : ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) ≤ (↑(nndist f g) : ℝ)
ω : Ω
⊢ HAdd.hAdd (α := ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0)
      (nndist (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) ω : ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0)) ≤
    HAdd.hAdd (α := ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) (nndist f g)

Tactic:
(add_le_add_iff_left (g ω)).mpr (le_dist ω)

Premises used: Iff.mpr, add_le_add_iff_left, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) ω : ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) ≤ (↑(nndist f g) : ℝ)
ω : Ω
⊢ (f : (a : Ω) → ℝ≥0) ω ≤ HAdd.hAdd (α := ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) (nndist f g)

Tactic:
calc f ω
     _ ≤ g ω + nndist (f ω) (g ω) := NNReal.le_add_nndist (f ω) (g ω)
     _ ≤ g ω + nndist f g := (add_le_add_iff_left (g ω)).mpr (le_dist ω)

Premises used: Iff.mpr, NNDist.nndist, add_le_add_iff_left, NNReal.le_add_nndist, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) ω : ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) ≤ (↑(nndist f g) : ℝ)
ω : Ω
⊢ (f : (a : Ω) → ℝ≥0) ω ≤ HAdd.hAdd (α := ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) (nndist f g)

Tactic:
have le' : f ω ≤ g ω + nndist f g := by
    calc f ω
     _ ≤ g ω + nndist (f ω) (g ω) := NNReal.le_add_nndist (f ω) (g ω)
     _ ≤ g ω + nndist f g := (add_le_add_iff_left (g ω)).mpr (le_dist ω)
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) ω : ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) ≤ (↑(nndist f g) : ℝ)
ω : Ω
le' : (f : (a : Ω) → ℝ≥0) ω ≤ HAdd.hAdd (α := ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) (nndist f g)
⊢ (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ≤ (↑(HAdd.hAdd (α := ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) (nndist f g)) : ℝ≥0∞)

Tactic:
exact_mod_cast le'
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) ω : ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) ≤ (↑(nndist f g) : ℝ)
ω : Ω
le' : (f : (a : Ω) → ℝ≥0) ω ≤ HAdd.hAdd (α := ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) (nndist f g)
⊢ (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ≤ (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + (↑(nndist f g) : ℝ≥0∞)

Tactic:
have le : (f ω : ℝ≥0∞) ≤ (g ω : ℝ≥0∞) + nndist f g := by
    simpa only [← ENNReal.coe_add] using (by exact_mod_cast le')
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
le_dist : ∀ (ω : Ω), dist (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) ω : ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) ≤ (↑(nndist f g) : ℝ)
ω : Ω
le' : (f : (a : Ω) → ℝ≥0) ω ≤ HAdd.hAdd (α := ℝ≥0) ((g : (a : Ω) → ℝ≥0) ω : ℝ≥0) (nndist f g)
le : (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ≤ (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + (↑(nndist f g) : ℝ≥0∞)
hfg hfg₁ hfg₂ hfg₃ :
  ∀ (le : (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ≤ (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + edist f g),
    LE.le (α := (fun (a : Ω) ↦ ℝ≥0∞) ω) ((fun (a : Ω) ↦ (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) ω)
      ((fun (a : Ω) ↦ (↑((g : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) + edist f g) ω)
⊢ LE.le (α := (fun (a : Ω) ↦ ℝ≥0∞) ω) ((fun (a : Ω) ↦ (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) ω)
    ((fun (a : Ω) ↦ (↑((g : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) + edist f g) ω)

Tactic:
rwa [coe_nnreal_ennreal_nndist] at le

Premises used: coe_nnreal_ennreal_nndist
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
rw : ∀ (x y : Ω →ᵇ ℝ≥0), dist (μ.testAgainstNN x) (μ.testAgainstNN y) ≤ (↑μ.mass : ℝ) * dist x y
⊢ LipschitzWith (β := ℝ≥0) μ.mass fun (f : Ω →ᵇ ℝ≥0) ↦ μ.testAgainstNN f

Tactic:
rw [lipschitzWith_iff_dist_le_mul]

Premises used: lipschitzWith_iff_dist_le_mul
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
this : |(↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)| ≤ (↑μ.mass : ℝ) * dist f₁ f₂
rwa rwa₁ rwa₂ rwa₃ : |(↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)| ≤ (↑μ.mass : ℝ) * dist f₁ f₂
⊢ dist (μ.testAgainstNN f₁) (μ.testAgainstNN f₂) ≤ (↑μ.mass : ℝ) * dist f₁ f₂

Tactic:
rwa [NNReal.dist_eq]

Premises used: NNReal.dist_eq
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
suffices : |(↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)| ≤ (↑μ.mass : ℝ) * dist f₁ f₂
⊢ dist (μ.testAgainstNN f₁) (μ.testAgainstNN f₂) ≤ (↑μ.mass : ℝ) * dist f₁ f₂

Tactic:
suffices abs (μ.testAgainstNN f₁ - μ.testAgainstNN f₂ : ℝ) ≤ μ.mass * dist f₁ f₂ by
    rwa [NNReal.dist_eq]
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
apply :
  -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ∧
    (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂
⊢ |(↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)| ≤ (↑μ.mass : ℝ) * dist f₁ f₂

Tactic:
apply abs_le.mpr

Premises used: Iff.mpr, abs_le
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
left : -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)
right : (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂
⊢ -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ∧
    (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + nndist f₂ f₁ * μ.mass

Tactic:
have key := μ.testAgainstNN_lipschitz_estimate f₂ f₁
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + nndist f₂ f₁ * μ.mass
⊢ μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + μ.mass * nndist f₂ f₁

Tactic:
rw [mul_comm] at key

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + μ.mass * nndist f₂ f₁
this : (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑(μ.testAgainstNN f₁) : ℝ) + (↑μ.mass : ℝ) * dist f₁ f₂
linarith :
  (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) < -((↑μ.mass : ℝ) * dist f₁ f₂) →
    (↑(μ.testAgainstNN f₂) : ℝ) - ((↑(μ.testAgainstNN f₁) : ℝ) + (↑μ.mass : ℝ) * dist f₁ f₂) +
        ((↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) - -((↑μ.mass : ℝ) * dist f₁ f₂)) =
      0
⊢ -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + μ.mass * nndist f₂ f₁
left : (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑(μ.testAgainstNN f₁) : ℝ) + (↑μ.mass : ℝ) * dist f₁ f₂
⊢ -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)

Tactic:
suffices ↑(μ.testAgainstNN f₂) ≤ ↑(μ.testAgainstNN f₁) + ↑μ.mass * dist f₁ f₂ by linarith
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + μ.mass * nndist f₂ f₁
⊢ (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑(μ.testAgainstNN f₁) : ℝ) + (↑μ.mass : ℝ) * dist f₁ f₂

Tactic:
simpa [nndist_comm] using NNReal.coe_mono key

Premises used: nndist_comm, NNReal.coe_mono
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + nndist f₁ f₂ * μ.mass

Tactic:
have key := μ.testAgainstNN_lipschitz_estimate f₁ f₂
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + nndist f₁ f₂ * μ.mass
⊢ μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + μ.mass * nndist f₁ f₂

Tactic:
rw [mul_comm] at key

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + μ.mass * nndist f₁ f₂
this : (↑(μ.testAgainstNN f₁) : ℝ) ≤ (↑(μ.testAgainstNN f₂) : ℝ) + (↑μ.mass : ℝ) * dist f₁ f₂
linarith :
  (↑μ.mass : ℝ) * dist f₁ f₂ < (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) →
    (↑(μ.testAgainstNN f₁) : ℝ) - ((↑(μ.testAgainstNN f₂) : ℝ) + (↑μ.mass : ℝ) * dist f₁ f₂) +
        ((↑μ.mass : ℝ) * dist f₁ f₂ - ((↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ))) =
      0
⊢ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + μ.mass * nndist f₁ f₂
right : (↑(μ.testAgainstNN f₁) : ℝ) ≤ (↑(μ.testAgainstNN f₂) : ℝ) + (↑μ.mass : ℝ) * dist f₁ f₂
⊢ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂

Tactic:
suffices ↑(μ.testAgainstNN f₁) ≤ ↑(μ.testAgainstNN f₂) + ↑μ.mass * dist f₁ f₂ by linarith
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
key : μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + μ.mass * nndist f₁ f₂
⊢ (↑(μ.testAgainstNN f₁) : ℝ) ≤ (↑(μ.testAgainstNN f₂) : ℝ) + (↑μ.mass : ℝ) * dist f₁ f₂

Tactic:
simpa using NNReal.coe_mono key

Premises used: NNReal.coe_mono
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ Eq (α := (a : Ω →ᵇ ℝ≥0) → ℝ≥0) (⇑μ.toWeakDualBCNN : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) μ.testAgainstNN

Tactic:
rfl

Premises used: ENNReal.toNNReal, MeasureTheory.FiniteMeasure.testAgainstNN, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f : Ω →ᵇ ℝ≥0
⊢ ((μ.toWeakDualBCNN : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f =
    (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toNNReal

Tactic:
rfl

Premises used: ENNReal.toNNReal, MeasureTheory.FiniteMeasure.testAgainstNN, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ Continuous[instTopologicalSpace, _] toWeakDualBCNN

Tactic:
continuous_induced_dom

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

Tactic:
Continuous.comp ?_ (toWeakDualBCNN_continuous (Ω := Ω))

Premises used: Continuous.comp, MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
refine : Continuous (Y := ℝ≥0) fun (φ : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) ↦ (φ : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f
⊢ Continuous[instTopologicalSpace, _]
    ((fun (φ : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) ↦ (φ : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f) ∘ toWeakDualBCNN)

Tactic:
refine Continuous.comp ?_ (toWeakDualBCNN_continuous (Ω := Ω))

Premises used: Continuous.comp, MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuous
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous (Y := ℝ≥0) fun (φ : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) ↦ (φ : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f

Tactic:
WeakBilin.eval_continuous _ _

Premises used: WeakDual, WeakBilin.eval_continuous
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous (Y := ℝ≥0) fun (φ : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)) ↦ (φ : (a : Ω →ᵇ ℝ≥0) → ℝ≥0) f

Tactic:
exact WeakBilin.eval_continuous _ _

Premises used: WeakBilin.eval_continuous