awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ g ≤ f,
    Measurable g ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
have obtain : ∀ (g : α →ₛ ℝ≥0∞) (hgf : (⇑g : (a : α) → ℝ≥0∞) ≤ f) (hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ),
  ∃ g ≤ f,
    Measurable g ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
Tactic: obtain ⟨g, hgf, hgε⟩ : ∃ (g : α →ₛ ℝ≥0∞) (_ : g ≤ f), ∫⁻ a, f a ∂μ - ε < g.lintegral μ := by
      simpa only [← lt_iSup_iff, ← lintegral_def] using ENNReal.sub_lt_self hf hf₀ hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α →ₛ ℝ≥0∞
hgf : (⇑g : (a : α) → ℝ≥0∞) ≤ f
hgε : ∫⁻ (a : α), f a ∂μ - ε < g.lintegral μ
⊢ ∃ g ≤ f,
    Measurable g ∧
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
        ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
have refine : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support (M := ℝ≥0∞) (⇑g : (a : α) → ℝ≥0∞)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨g, hgf, g.measurable, ?_, by rwa [g.lintegral_eq_lintegral]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
have neg : ∀ (g : α → ℝ≥0∞) (hgf : g ≤ f) (hg_meas : Measurable g)
  (hgsupp : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ),
  ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
Tactic: obtain ⟨g, hgf, hg_meas, hgsupp, hgε⟩ :
      ∃ g ≤ f, Measurable g ∧ μ (support g) < ∞ ∧ ∫⁻ a, f a ∂μ - ε < ∫⁻ a, g a ∂μ := by
    obtain ⟨g, hgf, hgε⟩ : ∃ (g : α →ₛ ℝ≥0∞) (_ : g ≤ f), ∫⁻ a, f a ∂μ - ε < g.lintegral μ := by
      simpa only [← lt_iSup_iff, ← lintegral_def] using ENNReal.sub_lt_self hf hf₀ hε
    refine ⟨g, hgf, g.measurable, ?_, by rwa [g.lintegral_eq_lintegral]⟩
    exact SimpleFunc.FinMeasSupp.of_lintegral_ne_top <| ne_top_of_le_ne_top hf <|
      g.lintegral_eq_lintegral μ ▸ lintegral_mono hgf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
hf₀ : ¬∫⁻ (a : α), f a ∂μ = 0
g : α → ℝ≥0∞
hgf : g ≤ f
hg_meas : Measurable g
hgsupp : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (support g) : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : ∫⁻ (a : α), f a ∂μ - ε < ∫⁻ (a : α), g a ∂μ
⊢ ∃ (s : Set α),
    MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧ ∫⁻ (a : α) in sᶜ, f a ∂μ < ε
have neg : ∫⁻ (a : α) in (support g)ᶜ, f a ∂μ < ε
Tactic: refine ⟨_, measurableSet_support hg_meas, hgsupp, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ ∃ (g : α → ℝ≥0∞),
    Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
have obtain : ∀ (g : α → ℝ≥0∞) (hmg : Measurable g) (hgf : g ≤ f) (hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ),
  ∃ (g : α → ℝ≥0∞),
    Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
Tactic: obtain ⟨g, hmg, hgf, hifg⟩ := exists_measurable_le_lintegral_eq (μ := μ) f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∃ (g : α → ℝ≥0∞),
    Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
have right : ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
Tactic: use g, hmg, hgf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
have right : ∀ (s : Set α) (hms : MeasurableSet s), ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
Tactic: refine fun s hms ↦ le_antisymm ?_ (lintegral_mono hgf)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have right : ∫⁻ (a : α), g a ∂μ - ∫⁻ (x : α) in sᶜ, f x ∂μ ≤ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α) in sᶜ, g x ∂μ
Tactic: rw [← compl_compl s, setLIntegral_compl hms.compl, setLIntegral_compl hms.compl, hifg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
right : ∫⁻ (a : α), g a ∂μ - ∫⁻ (x : α) in sᶜ, f x ∂μ ≤ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α) in sᶜ, g x ∂μ
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have right₁ : ∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ∞
Tactic: rw [← compl_compl s, setLIntegral_compl hms.compl, setLIntegral_compl hms.compl, hifg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
right : ∫⁻ (a : α), g a ∂μ - ∫⁻ (x : α) in sᶜ, f x ∂μ ≤ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α) in sᶜ, g x ∂μ
right₁ : ∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ∞
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α) in s, g a ∂μ
have right₂ : ∫⁻ (x : α) in sᶜ, f x ∂μ ≠ ∞
Tactic: rw [← compl_compl s, setLIntegral_compl hms.compl, setLIntegral_compl hms.compl, hifg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (a : α), g a ∂μ - ∫⁻ (x : α) in sᶜ, f x ∂μ ≤ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α) in sᶜ, g x ∂μ
have right : ∀ (x : α), g x ≤ f x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Sub (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (a : α), f a ∂μ ≠ ∞
g : α → ℝ≥0∞
hmg : Measurable g
hgf : g ≤ f
hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
s : Set α
hms : MeasurableSet s
⊢ ∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ∞
have right : ∀ (hf : ∫⁻ (a : α), g a ∂μ ≠ ∞) (hmg : Measurable g) (hgf : g ≤ f) (hifg : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ)
  (s : Set α) (hms : MeasurableSet s), ∫⁻ (x : α) in sᶜ, g x ∂μ ≠ ∞
Tactic: rw [hifg] at hf
Cleared hypotheses: hf, hmg, hgf, hifg, s, hms
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have mp : AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) →
  AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g : α → E
mp :
  AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) →
    AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) ↔
    AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have mpr : AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ →
  AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
⊢ AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
Tactic: have A : MeasurableSet { x : α | f x ≠ 0 } := (hf (measurableSet_singleton 0)).compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ AEMeasurable.{u_1, u_2} (β := E) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) μ
have mp : EventuallyEq.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) fun (x : α) ↦ (↑(f x) : ℝ) • g' x
Tactic: refine ⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.smul g'meas, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) fun (x : α) ↦ (↑(f x) : ℝ) • g' x
have mp : ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
  Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
Tactic: apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ { x | f x ≠ 0 }
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
mp :
  ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
    Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ (↑(f x) : ℝ) • g x) fun (x : α) ↦ (↑(f x) : ℝ) • g' x
have mp₁ : ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}ᶜ,
  Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
Tactic: apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ { x | f x ≠ 0 }
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
    Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
have hg'₁ : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
Tactic: rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'
Cleared hypotheses: hg', A
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0},
    Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
have mp : ∀ᵐ (x : α) ∂μ,
  Membership.mem (γ := Set α) {x : α | f x ≠ 0} x →
    Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
Tactic: rw [ae_restrict_iff' A]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ,
    Membership.mem (γ := Set α) {x : α | f x ≠ 0} x →
      Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
have h : ∀ (a : α), ((↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a) → f a ≠ 0 → (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a
Tactic: filter_upwards [hg']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a ≠ 0
⊢ (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a
have this : (↑(f a) : ℝ≥0∞) ≠ 0
Tactic: have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h'a
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = g' x
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
a : α
ha : (↑(f a) : ℝ≥0∞) ≠ 0 → g a = g' a
h'a : f a ≠ 0
this : (↑(f a) : ℝ≥0∞) ≠ 0
⊢ (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a
have h : (↑(f a) : ℝ) • g' a = (↑(f a) : ℝ) • g' a
Tactic: rw [ha this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x : α | f x ≠ 0}ᶜ,
    Eq.{u_2 + 1} (α := E) ((fun (x : α) ↦ (↑(f x) : ℝ) • g x) x) ((fun (x : α) ↦ (↑(f x) : ℝ) • g' x) x)
have h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | f x ≠ 0}ᶜ a → (↑(f a) : ℝ) • g a = (↑(f a) : ℝ) • g' a
Tactic: filter_upwards [ae_restrict_mem A.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] g'
A : MeasurableSet.{u_1} (α := α) {x : α | f x ≠ 0}
x : α
hx : Membership.mem (γ := Set α) {x : α | f x ≠ 0}ᶜ x
⊢ (↑(f x) : ℝ) • g x = (↑(f x) : ℝ) • 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.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
⊢ AEMeasurable g (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))
have mpr : g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f x) : ℝ)⁻¹ • g' x
Tactic: refine ⟨fun x => (f x : ℝ)⁻¹ • g' x, hf.coe_nnreal_real.inv.smul g'meas, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
⊢ g =ᶠ[ae (μ.withDensity fun (x : α) ↦ (↑(f x) : ℝ≥0∞))] fun (x : α) ↦ (↑(f x) : ℝ)⁻¹ • g' x
have mpr : ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f x) : ℝ)⁻¹ • g' x
Tactic: rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
⊢ ∀ᵐ (x : α) ∂μ, (↑(f x) : ℝ≥0∞) ≠ 0 → g x = (↑(f x) : ℝ)⁻¹ • g' x
have h : ∀ (a : α), (↑(f a) : ℝ) • g a = g' a → (↑(f a) : ℝ≥0∞) ≠ 0 → g a = (↑(f a) : ℝ)⁻¹ • g' a
Tactic: filter_upwards [hg']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
x : α
hx : (↑(f x) : ℝ) • g x = g' x
h'x : (↑(f x) : ℝ≥0∞) ≠ 0
⊢ g x = (↑(f x) : ℝ)⁻¹ • g' x
have h : (↑(f x) : ℝ) ≠ 0
Tactic: rw [← hx, smul_smul, inv_mul_cancel₀, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.LebesgueNormedSpace (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : Measurable g'
hg' : (fun (x : α) ↦ (↑(f x) : ℝ) • g x) =ᶠ[ae μ] g'
x : α
hx : (↑(f x) : ℝ) • g x = g' x
h'x : (↑(f x) : ℝ≥0∞) ≠ 0
⊢ (↑(f x) : ℝ) ≠ 0
have h'x₁ : ¬f x = 0
Tactic: simp only [Ne, ENNReal.coe_eq_zero] at h'x
Cleared hypotheses: h'x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
⊢ lmarginal (X := X) μ ∅ f = f
have h : ∀ (x : (i : δ) → X i), lmarginal (X := X) μ ∅ f x = f x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
⊢ lmarginal (X := X) μ ∅ f x = f x
have h : (∫⁻ (y : (i : ↥∅) → X (↑i : δ)),
    f (updateFinset (π := X) x ∅ y) ∂Measure.dirac fun (a : ↥∅) ↦ isEmptyElim (p := fun (x : ↥∅) ↦ X (↑x : δ)) a) =
  f x
Tactic: simp_rw [lmarginal, Measure.pi_of_empty fun i : (∅ : Finset δ) => μ i]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
⊢ (∫⁻ (y : (i : ↥∅) → X (↑i : δ)),
      f (updateFinset (π := X) x ∅ y) ∂Measure.dirac fun (a : ↥∅) ↦ isEmptyElim (p := fun (x : ↥∅) ↦ X (↑x : δ)) a) =
    f x
have h : Measurable (β := ℝ≥0∞) fun (a : (i : ↥∅) → X (↑i : δ)) ↦ f (updateFinset (π := X) x ∅ a)
Tactic: apply lintegral_dirac'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s : Finset δ
x y : (i : δ) → X i
f : ((i : δ) → X i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
⊢ lmarginal (X := X) μ s f x = lmarginal (X := X) μ s f y
have dsimp : (∫⁻ (y : (i : ↥s) → X (↑i : δ)),
    f fun (i : δ) ↦
      if hi : i ∈ s then y (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi)
      else x i ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)) =
  ∫⁻ (y_1 : (i : ↥s) → X (↑i : δ)),
    f fun (i : δ) ↦
      if hi : i ∈ s then y_1 (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi)
      else y i ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)
Tactic: dsimp [lmarginal, updateFinset_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
s : Finset δ
x y : (i : δ) → X i
f : ((i : δ) → X i) → ℝ≥0∞
h : ∀ i ∉ s, x i = y i
⊢ (∫⁻ (y : (i : ↥s) → X (↑i : δ)),
      f fun (i : δ) ↦
        if hi : i ∈ s then y (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi)
        else x i ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)) =
    ∫⁻ (y_1 : (i : ↥s) → X (↑i : δ)),
      f fun (i : δ) ↦
        if hi : i ∈ s then y_1 (Subtype.mk (p := fun (x : δ) ↦ x ∈ s) i hi)
        else y i ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : δ)) fun (i : ↥s) ↦ μ (↑i : δ)
have e_f : ∀ (x_1 : (i : ↥s) → X (↑i : δ)), ∀ x_2 ∉ s, x x_2 = y x_2
Tactic: rcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Marginal (goal)
Goal:
δ : Type u_1
X : δ → Type u_3
inst : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst_1 : DecidableEq δ
f : ((i : δ) → X i) → ℝ≥0∞
i : δ
α : Type u_1 := ↥{i}
e : X (↑default : δ) ≃ᵐ ((i_1 : α) → X (↑i_1 : δ)) :=
  MeasurableEquiv.symm (MeasurableEquiv.piUnique fun (j : α) ↦ X (↑j : δ))
⊢ lmarginal (X := X) μ {i} f = fun (x : (a : δ) → X a) ↦ ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
have h : ∀ (x : (i : δ) → X i), lmarginal (X := X) μ {i} f x = ∫⁻ (xᵢ : X i), f (update (β := X) x i xᵢ) ∂μ i
Tactic: ext1 x