awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) univ
have simp_rw : Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
  ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
    (SProd.sprod (α := Set α) (β := Set β) univ univ)
Tactic: simp_rw [← Set.univ_prod_univ, Measure.prod_prod, Heval MeasurableSet.univ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
simp_rw :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞)
      (SProd.sprod (α := Set α) (β := Set β) univ univ)
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) univ
have simp_rw₁ : Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: simp_rw [← Set.univ_prod_univ, Measure.prod_prod, Heval MeasurableSet.univ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
⊢ ∀ (s : Set (α × β)),
    Membership.mem (γ := Set (Set (α × β)))
        (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
        s →
      Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
        ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
have simp : ∀ (s : Set (α × β)) (x : Set α),
  MeasurableSet x →
    ∀ (x_1 : Set β),
      MeasurableSet x_1 →
        x ×ˢ x_1 = s →
          Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
            ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
Tactic: simp only [mem_image2, mem_setOf_eq, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
s : Set (α × β)
x : Set α
Hu : MeasurableSet x
x_1 : Set β
Hv : MeasurableSet x_1
Heq : x ×ˢ x_1 = s
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
have simp_rw : Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
  ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) (x ×ˢ x_1)
Tactic: simp_rw [← Heq, Measure.prod_prod, Heval Hu Hv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
s : Set (α × β)
x : Set α
Hu : MeasurableSet x
x_1 : Set β
Hv : MeasurableSet x_1
Heq : x ×ˢ x_1 = s
simp_rw :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) (x ×ˢ x_1)
⊢ Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
have simp_rw₁ : Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞)
    (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) x_1 : ℝ≥0∞)
Tactic: simp_rw [← Heq, Measure.prod_prod, Heval Hu Hv]
-- 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 :
  ∀ (f : Ω →ᵇ ℝ≥0),
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
      ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
⊢ μ = ν
have a : (↑μ : Measure Ω) = (↑ν : Measure Ω)
Tactic: apply Subtype.ext
-- 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 :
  ∀ (f : Ω →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑ν : Measure Ω))
⊢ μ = ν
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 (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (f : Ω →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑ν : Measure Ω))
f : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)
have h₁ : (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal =
  (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)).toReal
Tactic: apply (ENNReal.toReal_eq_toReal_iff' (lintegral_lt_top_of_nnreal μ f).ne
      (lintegral_lt_top_of_nnreal ν f).ne).mp
-- 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 :
  ∀ (f : Ω →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω)) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑ν : Measure Ω))
f : Ω →ᵇ ℝ≥0
⊢ (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑μ : Measure Ω)).toReal =
    (∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂(↑ν : Measure Ω)).toReal
have h₁ : Eq (α := ℝ) (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑μ : Measure Ω))
  (∫ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ) ∂(↑ν : Measure Ω))
Tactic: rw [toReal_lintegral_coe_eq_integral f μ, toReal_lintegral_coe_eq_integral f ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : LE.le (α := (a : Ω) → ℝ≥0) (⇑f : (a : Ω) → ℝ≥0) (⇑g : (a : Ω) → ℝ≥0)
⊢ μ.testAgainstNN f ≤ μ.testAgainstNN g
have simp : ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≤
  ∫⁻ (ω : Ω), (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)
Tactic: simp only [← ENNReal.coe_le_coe, testAgainstNN_coe_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
f_le_g : LE.le (α := (a : Ω) → ℝ≥0) (⇑f : (a : Ω) → ℝ≥0) (⇑g : (a : Ω) → ℝ≥0)
⊢ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≤
    ∫⁻ (ω : Ω), (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)
have hfg : ∀ (x : Ω), LE.le (α := ℝ≥0) ((f : (a : Ω) → ℝ≥0) x : ℝ≥0) ((g : (a : Ω) → ℝ≥0) x : ℝ≥0)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
μ : FiniteMeasure Ω
⊢ μ.testAgainstNN 1 = μ.mass
have simp : ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) = μ.mass
Tactic: simp only [testAgainstNN, coe_one, Pi.one_apply, ENNReal.coe_one, lintegral_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
⊢ Eq.{u_1 + 1} (α := (f : Ω →ᵇ ℝ≥0) → ℝ≥0) (testAgainstNN 0) 0
have h : ∀ (x : Ω →ᵇ ℝ≥0), testAgainstNN 0 x = 0 x
Tactic: funext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN (f₁ + f₂) = μ.testAgainstNN f₁ + μ.testAgainstNN f₂
have simp : ∫⁻ (ω : Ω), (↑((f₁ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + (↑((f₂ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
  ∫⁻ (ω : Ω), (↑((f₁ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) +
    ∫⁻ (ω : Ω), (↑((f₂ : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)
Tactic: simp only [← ENNReal.coe_inj, BoundedContinuousFunction.coe_add, ENNReal.coe_add, Pi.add_apply,
    testAgainstNN_coe_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ μ.testAgainstNN (c • f) = c • μ.testAgainstNN f
have simp : ∫⁻ (ω : Ω), c • (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
  c • ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)
Tactic: simp only [← ENNReal.coe_inj, BoundedContinuousFunction.coe_smul, testAgainstNN_coe_eq,
    ENNReal.coe_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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
⊢ ∫⁻ (ω : Ω), c • (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
    c • ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω)
have simp_rw : ∫⁻ (ω : Ω), HSMul.hSMul (β := ℝ≥0∞) c 1 * (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) =
  HSMul.hSMul (β := ℝ≥0∞) c 1 * ∫⁻ (ω : Ω), (↑((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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ μ.testAgainstNN f ≤ μ.testAgainstNN g + nndist f g * μ.mass
have simp : ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≤
  ∫⁻ (ω : Ω), (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + edist f g ∂(↑μ : Measure Ω)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ ∫⁻ (ω : Ω), (↑((f : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂(↑μ : Measure Ω) ≤
    ∫⁻ (ω : Ω), (↑((g : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) + edist f g ∂(↑μ : Measure Ω)
have hfg : LE.le.{u_1} (α := Ω → ℝ≥0∞) (fun (a : Ω) ↦ (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) fun (a : Ω) ↦
  (↑((g : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) + edist f g
Tactic: apply lintegral_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f g : Ω →ᵇ ℝ≥0
⊢ LE.le.{u_1} (α := Ω → ℝ≥0∞) (fun (a : Ω) ↦ (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) fun (a : Ω) ↦
    (↑((g : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) + edist f g
have le_dist : ∀ (ω : Ω), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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.le (α := (fun (a : Ω) ↦ ℝ≥0∞) ω) ((fun (a : Ω) ↦ (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) ω)
    ((fun (a : Ω) ↦ (↑((g : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) + edist f g) ω)
have le' : (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 ω)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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.le (α := (fun (a : Ω) ↦ ℝ≥0∞) ω) ((fun (a : Ω) ↦ (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) ω)
    ((fun (a : Ω) ↦ (↑((g : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) + edist f g) ω)
have le : (↑((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')
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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∞)
⊢ LE.le (α := (fun (a : Ω) ↦ ℝ≥0∞) ω) ((fun (a : Ω) ↦ (↑((f : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) ω)
    ((fun (a : Ω) ↦ (↑((g : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) + edist f g) ω)
have 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) ω)
Tactic: rwa [coe_nnreal_ennreal_nndist] at le
Cleared hypotheses: le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ LipschitzWith (β := ℝ≥0) μ.mass fun (f : Ω →ᵇ ℝ≥0) ↦ μ.testAgainstNN f
have rw : ∀ (x y : Ω →ᵇ ℝ≥0), dist (μ.testAgainstNN x) (μ.testAgainstNN y) ≤ (↑μ.mass : ℝ) * dist x y
Tactic: rw [lipschitzWith_iff_dist_le_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ dist (μ.testAgainstNN f₁) (μ.testAgainstNN f₂) ≤ (↑μ.mass : ℝ) * dist f₁ f₂
have suffices : |(↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)| ≤ (↑μ.mass : ℝ) * dist f₁ f₂
Tactic: suffices abs (μ.testAgainstNN f₁ - μ.testAgainstNN f₂ : ℝ) ≤ μ.mass * dist f₁ f₂ by
    rwa [NNReal.dist_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ |(↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)| ≤ (↑μ.mass : ℝ) * dist f₁ f₂
have apply : -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ∧
  (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂
Tactic: apply abs_le.mpr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ∧
    (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂
have left : -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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₂) : ℝ)
⊢ -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ∧
    (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂
have right : (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)
have key : μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + nndist f₂ f₁ * μ.mass
Tactic: have key := μ.testAgainstNN_lipschitz_estimate f₂ f₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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
⊢ -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)
have key₁ : μ.testAgainstNN f₂ ≤ μ.testAgainstNN f₁ + μ.mass * nndist f₂ f₁
Tactic: rw [mul_comm] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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₂
⊢ -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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₁
⊢ -((↑μ.mass : ℝ) * dist f₁ f₂) ≤ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ)
have left : (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑(μ.testAgainstNN f₁) : ℝ) + (↑μ.mass : ℝ) * dist f₁ f₂
Tactic: suffices ↑(μ.testAgainstNN f₂) ≤ ↑(μ.testAgainstNN f₁) + ↑μ.mass * dist f₁ f₂ by linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : FiniteMeasure Ω
f₁ f₂ : Ω →ᵇ ℝ≥0
⊢ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂
have key : μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + nndist f₁ f₂ * μ.mass
Tactic: have key := μ.testAgainstNN_lipschitz_estimate f₁ f₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
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 : ℝ) * dist f₁ f₂
have key₁ : μ.testAgainstNN f₁ ≤ μ.testAgainstNN f₂ + μ.mass * nndist f₁ f₂
Tactic: rw [mul_comm] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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₂
⊢ (↑(μ.testAgainstNN f₁) : ℝ) - (↑(μ.testAgainstNN f₂) : ℝ) ≤ (↑μ.mass : ℝ) * dist f₁ f₂
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
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₂
have right : (↑(μ.testAgainstNN f₁) : ℝ) ≤ (↑(μ.testAgainstNN f₂) : ℝ) + (↑μ.mass : ℝ) * dist f₁ f₂
Tactic: suffices ↑(μ.testAgainstNN f₁) ≤ ↑(μ.testAgainstNN f₂) + ↑μ.mass * dist f₁ f₂ by linarith