awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
indicator :
  ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      ∫⁻ (a : α), s.indicator (fun (x : α) ↦ c) a ∂μ.withDensity f =
        ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (s.indicator fun (x : α) ↦ c) a ∂μ
add :
  ∀ ⦃f_1 g : α → ℝ≥0∞⦄,
    Disjoint (Function.support f_1) (Function.support g) →
      Measurable f_1 →
        Measurable g →
          ∫⁻ (a : α), f_1 a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1) a ∂μ →
            ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
              ∫⁻ (a : α), (f_1 + g) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ
⊢ ∀ {g : α → ℝ≥0∞}, Measurable g → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
have iSup : ∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄,
  (∀ (n : ℕ), Measurable (f_1 n)) →
    Monotone f_1 →
      (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) →
        ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), f_1 n x : ℝ≥0∞)) a ∂μ.withDensity f =
          ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ⨆ (n : ℕ), f_1 n x) a ∂μ
Tactic: apply Measurable.ennreal_induction
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
m n : ℕ
hmn : m ≤ n
x : α
⊢ f x * g m x ≤ f x * g n x
have grw : f x * g n x ≤ f x * g n x
Tactic: grw [h_mono_g hmn x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g : ℕ → α → ℝ≥0∞
h_mea_g : ∀ (n : ℕ), Measurable (g n)
h_mono_g : Monotone g
h_ind : ∀ (n : ℕ), ∫⁻ (a : α), g n a ∂μ.withDensity f = ∫⁻ (a : α), (f * g n) a ∂μ
⊢ ∫⁻ (a : α), (fun (x : α) ↦ (⨆ (n : ℕ), g n x : ℝ≥0∞)) a ∂μ.withDensity f =
    ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (x : α) ↦ ⨆ (n : ℕ), g n x) a ∂μ
have this : Monotone.{0, u_1} (β := (a : α) → ℝ≥0∞) fun (n : ℕ) (a : α) ↦ f a * g n a
Tactic: have : Monotone fun n a => f a * g n a := fun m n hmn x => by dsimp; grw [h_mono_g hmn x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ
have rw : ∫⁻ (x : α), g x ∂(μ.restrict s).withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ
Tactic: rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul _ hf hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
hs : MeasurableSet s
rw : ∫⁻ (x : α), g x ∂(μ.restrict s).withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.withDensity f = ∫⁻ (x : α) in s, (f * g) x ∂μ
have rw₁ : ∫⁻ (a : α) in s, (f * g) a ∂μ = ∫⁻ (x : α) in s, (f * g) x ∂μ
Tactic: rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul _ hf hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
have this : μ.withDensity f = μ.withDensity f'
Tactic: have : μ.withDensity f = μ.withDensity f' := withDensity_congr_ae hf.ae_eq_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
this : μ.withDensity f = μ.withDensity f'
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
have rw : ∀ (hg : AEMeasurable g (μ.withDensity f')) (this : μ.withDensity f = μ.withDensity f'),
  ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f * g) a ∂μ
Tactic: rw [this] at hg ⊢
Cleared hypotheses: hg, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∫⁻ (a : α), (f' * g') a ∂μ = ∫⁻ (a : α), (f' * g) a ∂μ
have h : f' * g' =ᶠ[ae μ] f' * g
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ f' * g' =ᶠ[ae μ] f' * g
have h : ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}, (f' * g') x = (f' * g) x
Tactic: apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
h : ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}, (f' * g') x = (f' * g) x
⊢ f' * g' =ᶠ[ae μ] f' * g
have h₁ : ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x
Tactic: apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}, (f' * g') x = (f' * g) x
have Z : g =ᶠ[ae (μ.withDensity f')] AEMeasurable.mk g hg
Tactic: have Z := hg.ae_eq_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : g =ᶠ[ae (μ.withDensity f')] AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}, (f' * g') x = (f' * g) x
have Z₁ : ∀ᵐ (x : α) ∂μ.restrict {x : α | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
Tactic: rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z
Cleared hypotheses: Z
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
Z : ∀ᵐ (x : α) ∂μ.restrict {x : α | AEMeasurable.mk f hf x ≠ 0}, g x = AEMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}, (f' * g') x = (f' * g) x
have h : ∀ (a : α), g a = AEMeasurable.mk g hg a → (f' * g') a = (f' * g) a
Tactic: filter_upwards [Z]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x
have M : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}ᶜ
Tactic: have M : MeasurableSet { x : α | f' x ≠ 0 }ᶜ :=
          (hf.measurable_mk (measurableSet_singleton 0).compl).compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}ᶜ
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f' x ≠ 0}ᶜ, (f' * g') x = (f' * g) x
have h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | f' x ≠ 0}ᶜ a → (f' * g') a = (f' * g) a
Tactic: filter_upwards [ae_restrict_mem M]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
M : MeasurableSet.{u_1} (α := α) {x : α | f' x ≠ 0}ᶜ
x : α
hx : Membership.mem (γ := Set α) {x : α | f' x ≠ 0}ᶜ x
⊢ (f' * g') x = (f' * g) x
have hx₁ : f' x = 0
Tactic: simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ
have h : f' * g =ᶠ[ae μ] f * g
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ f' * g =ᶠ[ae μ] f * g
have h : ∀ (a : α), f a = AEMeasurable.mk f hf a → (f' * g) a = (f * g) a
Tactic: filter_upwards [hf.ae_eq_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f * g) a ∂μ
have g₁ : ∫⁻ (a : α), (f' * g') a ∂μ = ∫⁻ (a : α), (f' * g) a ∂μ
Tactic: calc
    ∫⁻ a, g a ∂μ.withDensity f' = ∫⁻ a, g' a ∂μ.withDensity f' := lintegral_congr_ae hg.ae_eq_mk
    _ = ∫⁻ a, (f' * g') a ∂μ :=
      (lintegral_withDensity_eq_lintegral_mul _ hf.measurable_mk hg.measurable_mk)
    _ = ∫⁻ a, (f' * g) a ∂μ := by
      apply lintegral_congr_ae
      apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
      · have Z := hg.ae_eq_mk
        rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z
        filter_upwards [Z]
        intro x hx
        simp only [g', hx, Pi.mul_apply]
      · have M : MeasurableSet { x : α | f' x ≠ 0 }ᶜ :=
          (hf.measurable_mk (measurableSet_singleton 0).compl).compl
        filter_upwards [ae_restrict_mem M]
        intro x hx
        simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
        simp only [hx, zero_mul, Pi.mul_apply]
    _ = ∫⁻ a : α, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0∞ := AEMeasurable.mk f hf
hg : AEMeasurable g (μ.withDensity f')
this : μ.withDensity f = μ.withDensity f'
g' : α → ℝ≥0∞ := AEMeasurable.mk g hg
g₁ : ∫⁻ (a : α), (f' * g') a ∂μ = ∫⁻ (a : α), (f' * g) a ∂μ
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f' = ∫⁻ (a : α), (f * g) a ∂μ
have g₂ : ∫⁻ (a : α), (f' * g) a ∂μ = ∫⁻ (a : α), (f * g) a ∂μ
Tactic: calc
    ∫⁻ a, g a ∂μ.withDensity f' = ∫⁻ a, g' a ∂μ.withDensity f' := lintegral_congr_ae hg.ae_eq_mk
    _ = ∫⁻ a, (f' * g') a ∂μ :=
      (lintegral_withDensity_eq_lintegral_mul _ hf.measurable_mk hg.measurable_mk)
    _ = ∫⁻ a, (f' * g) a ∂μ := by
      apply lintegral_congr_ae
      apply ae_of_ae_restrict_of_ae_restrict_compl { x | f' x ≠ 0 }
      · have Z := hg.ae_eq_mk
        rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z
        filter_upwards [Z]
        intro x hx
        simp only [g', hx, Pi.mul_apply]
      · have M : MeasurableSet { x : α | f' x ≠ 0 }ᶜ :=
          (hf.measurable_mk (measurableSet_singleton 0).compl).compl
        filter_upwards [ae_restrict_mem M]
        intro x hx
        simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
        simp only [hx, zero_mul, Pi.mul_apply]
    _ = ∫⁻ a : α, (f * g) a ∂μ := by
      apply lintegral_congr_ae
      filter_upwards [hf.ae_eq_mk]
      intro x hx
      simp only [f', hx, Pi.mul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
have rw : AEMeasurable g ((μ.restrict s).withDensity f)
Tactic: rw [restrict_withDensity hs, lintegral_withDensity_eq_lintegral_mul₀' hf.restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
g : α → ℝ≥0∞
hg : AEMeasurable g (μ.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable g ((μ.restrict s).withDensity f)
have rw : AEMeasurable g ((μ.withDensity f).restrict s)
Tactic: rw [← restrict_withDensity hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f ≤ ∫⁻ (a : α), (f * g) a ∂μ
have rw : LE.le (α := ℝ≥0∞) (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f)
  (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ)
Tactic: rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞) (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f)
    (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ)
have refine : ∀ (i : α → ℝ≥0∞) (i_meas : Measurable i) (hi : i ≤ g),
  ∫⁻ (a : α), i a ∂μ.withDensity f ≤
    ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ
Tactic: refine iSup₂_le fun i i_meas => iSup_le fun hi => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
⊢ ∫⁻ (a : α), i a ∂μ.withDensity f ≤
    ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ
have rw : ∫⁻ (a : α), (f * i) a ∂μ ≤ ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ
Tactic: rw [lintegral_withDensity_eq_lintegral_mul _ f_meas i_meas]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
⊢ f * i ≤ f * g
have grw : f * g ≤ f * g
Tactic: grw [hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
have refine : ∫⁻ (a : α), (f * g) a ∂μ ≤ ∫⁻ (a : α), g a ∂μ.withDensity f
Tactic: refine le_antisymm (lintegral_withDensity_le_lintegral_mul μ f_meas g) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), (f * g) a ∂μ ≤ ∫⁻ (a : α), g a ∂μ.withDensity f
have rw : LE.le (α := ℝ≥0∞) (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ)
  (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f)
Tactic: rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → ℝ≥0∞
⊢ LE.le (α := ℝ≥0∞) (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ)
    (⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f)
have refine : ∀ (i : α → ℝ≥0∞) (i_meas : Measurable i) (hi : i ≤ f * g),
  ∫⁻ (a : α), i a ∂μ ≤ ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f
Tactic: refine iSup₂_le fun i i_meas => iSup_le fun hi => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
x : α
⊢ (f x)⁻¹ * i x ≤ g x
have rw : i x / f x ≤ g x
Tactic: rw [mul_comm, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
⊢ ∫⁻ (a : α), i a ∂μ ≤ ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f
have A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
Tactic: have A : (fun x => (f x)⁻¹ * i x) ≤ g := by
    intro x
    dsimp
    rw [mul_comm, ← div_eq_mul_inv]
    exact div_le_of_le_mul' (hi x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∫⁻ (a : α), i a ∂μ ≤ ⨆ (g_1 : α → ℝ≥0∞), ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f
have refine : ∫⁻ (a : α), i a ∂μ ≤
  ⨆ (_ : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g), ∫⁻ (a : α), (fun (x : α) ↦ (f x)⁻¹ * i x) a ∂μ.withDensity f
Tactic: refine le_iSup_of_le (fun x => (f x)⁻¹ * i x) (le_iSup_of_le (f_meas.inv.mul i_meas) ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∫⁻ (a : α), i a ∂μ ≤
    ⨆ (_ : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g), ∫⁻ (a : α), (fun (x : α) ↦ (f x)⁻¹ * i x) a ∂μ.withDensity f
have refine : ∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), (fun (x : α) ↦ (f x)⁻¹ * i x) a ∂μ.withDensity f
Tactic: refine le_iSup_of_le A ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), (fun (x : α) ↦ (f x)⁻¹ * i x) a ∂μ.withDensity f
have rw : ∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) a ∂μ
Tactic: rw [lintegral_withDensity_eq_lintegral_mul _ f_meas (f_meas.inv.mul i_meas)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∫⁻ (a : α), i a ∂μ ≤ ∫⁻ (a : α), HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) a ∂μ
have h : ∀ᵐ (a : α) ∂μ, i a ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) a
Tactic: apply lintegral_mono_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
⊢ ∀ᵐ (a : α) ∂μ, i a ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) a
have h : ∀ (a : α), f a < ∞ → i a ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) a
Tactic: filter_upwards [hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
⊢ i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
have h : ∀ (hx : f x = 0), i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
Tactic: rcases eq_or_ne (f x) 0 with (hx | hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
h : ∀ (hx : f x = 0), i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
⊢ i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
have h₁ : ∀ (hx : f x ≠ 0), i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
Tactic: rcases eq_or_ne (f x) 0 with (hx | hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x = 0
⊢ i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
have this : i x ≤ (f * g) x
Tactic: have := hi x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x = 0
this : i x ≤ (f * g) x
⊢ i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
have this₁ : i x = 0
Tactic: simp only [hx, zero_mul, Pi.mul_apply, nonpos_iff_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.WithDensity (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun (x : α) ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x ≠ 0
⊢ i x ≤ HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
have apply : i x = HMul.hMul (β := α → ℝ≥0∞) f (fun (a : α) ↦ (f a)⁻¹ * i a) x
Tactic: apply le_of_eq _