awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), s n) x
have L1 : ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x
Tactic: have L1 : ∀ᶠ n in atTop, g x + u n ≤ f x := by
      have : Tendsto (fun n => g x + u n) atTop (𝓝 (g x + (0 : ℝ≥0))) :=
        tendsto_const_nhds.add (ENNReal.tendsto_coe.2 u_lim)
      simp only [ENNReal.coe_zero, add_zero] at this
      exact this.eventually_le_const hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
L1 : ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), s n) x
have L2 : ∀ᶠ (n : ℕ) in atTop, g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)
Tactic: have L2 : ∀ᶠ n : ℕ in (atTop : Filter ℕ), g x ≤ (n : ℝ≥0) :=
      have : Tendsto (fun n : ℕ => ((n : ℝ≥0) : ℝ≥0∞)) atTop (𝓝 ∞) := by
        simp only [ENNReal.coe_natCast]
        exact ENNReal.tendsto_nat_nhds_top
      this.eventually_const_le (hx.trans_le le_top)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : g x < f x
L1 : ∀ᶠ (n : ℕ) in atTop, g x + (↑(u n) : ℝ≥0∞) ≤ f x
L2 : ∀ᶠ (n : ℕ) in atTop, g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)
⊢ Membership.mem (γ := Set α) (⋃ (n : ℕ), s n) x
have apply : ∃ (i : ℕ), x ∈ s i
Tactic: apply Set.mem_iUnion.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f ≤ᶠ[ae μ] g
have B : Subset.{u_1} (α := Set α) {x : α | f x ≤ g x}ᶜ (⋃ (n : ℕ), s n)
Tactic: have B : {x | f x ≤ g x}ᶜ ⊆ ⋃ n, s n := by
    intro x hx
    simp only [Set.mem_compl_iff, Set.mem_setOf, not_le] at hx
    have L1 : ∀ᶠ n in atTop, g x + u n ≤ f x := by
      have : Tendsto (fun n => g x + u n) atTop (𝓝 (g x + (0 : ℝ≥0))) :=
        tendsto_const_nhds.add (ENNReal.tendsto_coe.2 u_lim)
      simp only [ENNReal.coe_zero, add_zero] at this
      exact this.eventually_le_const hx
    have L2 : ∀ᶠ n : ℕ in (atTop : Filter ℕ), g x ≤ (n : ℝ≥0) :=
      have : Tendsto (fun n : ℕ => ((n : ℝ≥0) : ℝ≥0∞)) atTop (𝓝 ∞) := by
        simp only [ENNReal.coe_natCast]
        exact ENNReal.tendsto_nat_nhds_top
      this.eventually_const_le (hx.trans_le le_top)
    apply Set.mem_iUnion.2
    exact ((L1.and L2).and (eventually_mem_spanningSets μ x)).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
B : Subset.{u_1} (α := Set α) {x : α | f x ≤ g x}ᶜ (⋃ (n : ℕ), s n)
⊢ f ≤ᶠ[ae μ] g
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ f x ≤ g x) x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine le_antisymm ?_ bot_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
A :
  ∀ (ε N : ℝ≥0) (p : ℕ),
    0 < ε →
      Eq (α := ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) ({x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p) : ℝ≥0∞)
        (0 : ℝ≥0∞)
u : ℕ → ℝ≥0
left : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
s : (n : ℕ) → Set α :=
  fun (n : ℕ) ↦ {x : α | g x + (↑(u n) : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑(↑n : ℝ≥0) : ℝ≥0∞)} ∩ spanningSets μ n
μs : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
B : Subset.{u_1} (α := Set α) {x : α | f x ≤ g x}ᶜ (⋃ (n : ℕ), s n)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ f x ≤ g x) x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have μ₁ : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s n)) 0
Tactic: calc
    μ {x : α | (fun x : α => f x ≤ g x) x}ᶜ ≤ μ (⋃ n, s n) := measure_mono B
    _ ≤ ∑' n, μ (s n) := measure_iUnion_le _
    _ = 0 := by simp only [μs, tsum_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
⊢ f =ᶠ[ae μ] g
have A : f ≤ᶠ[ae μ] g
Tactic: have A : f ≤ᵐ[μ] g :=
    ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hf fun s hs h's => le_of_eq (h s hs h's)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
A : f ≤ᶠ[ae μ] g
⊢ f =ᶠ[ae μ] g
have B : g ≤ᶠ[ae μ] f
Tactic: have B : g ≤ᵐ[μ] f :=
    ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hg fun s hs h's => ge_of_eq (h s hs h's)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
A : f ≤ᶠ[ae μ] g
B : g ≤ᶠ[ae μ] f
⊢ f =ᶠ[ae μ] g
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≤ f x) x} x →
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = g x) x} x}
          x}
    a
Tactic: filter_upwards [A, B] with x using le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
A : f ≤ᶠ[ae μ] g
B : g ≤ᶠ[ae μ] f
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≤ f x) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x = g x) x} x}
            x}
      a
⊢ f =ᶠ[ae μ] g
have h₂ : ∀ (a : α), f a ≤ g a → g a ≤ f a → f a = g a
Tactic: filter_upwards [A, B] with x using le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
⊢ f =ᶠ[ae μ] g
have hf' : AEFinStronglyMeasurable f μ
Tactic: have hf' : AEFinStronglyMeasurable f μ :=
    ENNReal.aefinStronglyMeasurable_of_aemeasurable hfi hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
⊢ f =ᶠ[ae μ] g
have hg' : AEFinStronglyMeasurable g μ
Tactic: have hg' : AEFinStronglyMeasurable g μ :=
    ENNReal.aefinStronglyMeasurable_of_aemeasurable hgi hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
⊢ f =ᶠ[ae μ] g
have refine : ∀ᵐ (x : α) ∂μ.restrict (s ∪ t)ᶜ, f x = g x
Tactic: refine ae_of_ae_restrict_of_ae_restrict_compl _ this ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
⊢ ∀ᵐ (x : α) ∂μ.restrict (s ∪ t)ᶜ, f x = g x
have simp : ∀ᵐ (x : α) ∂μ.restrict (sᶜ ∩ tᶜ), f x = g x
Tactic: simp only [Set.compl_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
⊢ ∀ᵐ (x : α) ∂μ.restrict (sᶜ ∩ tᶜ), f x = g x
have h1 : f =ᶠ[ae (μ.restrict sᶜ)] 0
Tactic: have h1 : f =ᵐ[μ.restrict sᶜ] 0 := hf'.ae_eq_zero_compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ ∀ᵐ (x : α) ∂μ.restrict (sᶜ ∩ tᶜ), f x = g x
have h2 : g =ᶠ[ae (μ.restrict tᶜ)] 0
Tactic: have h2 : g =ᵐ[μ.restrict tᶜ] 0 := hg'.ae_eq_zero_compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : f =ᶠ[ae (μ.restrict sᶜ)] 0
h2 : g =ᶠ[ae (μ.restrict tᶜ)] 0
⊢ ∀ᵐ (x : α) ∂μ.restrict (sᶜ ∩ tᶜ), f x = g x
have rw : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x
Tactic: rw [ae_restrict_iff' (hf'.measurableSet.compl.inter hg'.measurableSet.compl)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : f =ᶠ[ae (μ.restrict sᶜ)] 0
h2 : g =ᶠ[ae (μ.restrict tᶜ)] 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x
have h1₁ : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
Tactic: rw [EventuallyEq, ae_restrict_iff' hf'.measurableSet.compl] at h1
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : g =ᶠ[ae (μ.restrict tᶜ)] 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x
have h2₁ : ∀ᵐ (x : α) ∂μ, x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
Tactic: rw [EventuallyEq, ae_restrict_iff' hg'.measurableSet.compl] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : ∀ᵐ (x : α) ∂μ, x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x
have h : ∀ (x : α) (h1 : x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x) (h2 : x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x)
  (hx : x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ), f x = g x
Tactic: filter_upwards [h1, h2] with x h1 h2 hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1_1 : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2_1 : ∀ᵐ (x : α) ∂μ, x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
x : α
h1 : x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
hx : x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ
⊢ f x = g x
have h : 0 x = g x
Tactic: rw [h1 (Set.inter_subset_left hx), h2 (Set.inter_subset_right hx)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1_1 : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2_1 : ∀ᵐ (x : α) ∂μ, x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
x : α
h1 : x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
hx : x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ
h : 0 x = g x
⊢ f x = g x
have h₁ : Eq (α := ℝ≥0∞) (0 x) (0 x)
Tactic: rw [h1 (Set.inter_subset_left hx), h2 (Set.inter_subset_right hx)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
⊢ f =ᶠ[ae μ] g
have suffices : f =ᶠ[ae (μ.restrict (s ∪ t))] g
Tactic: suffices f =ᵐ[μ.restrict (s ∪ t)] g by
    refine ae_of_ae_restrict_of_ae_restrict_compl _ this ?_
    simp only [Set.compl_union]
    have h1 : f =ᵐ[μ.restrict sᶜ] 0 := hf'.ae_eq_zero_compl
    have h2 : g =ᵐ[μ.restrict tᶜ] 0 := hg'.ae_eq_zero_compl
    rw [ae_restrict_iff' (hf'.measurableSet.compl.inter hg'.measurableSet.compl)]
    rw [EventuallyEq, ae_restrict_iff' hf'.measurableSet.compl] at h1
    rw [EventuallyEq, ae_restrict_iff' hg'.measurableSet.compl] at h2
    filter_upwards [h1, h2] with x h1 h2 hx
    rw [h1 (Set.inter_subset_left hx), h2 (Set.inter_subset_right hx)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
⊢ f =ᶠ[ae (μ.restrict (s ∪ t))] g
have refine : ∀ (u : Set α) (hu : MeasurableSet u)
  (huμ : LT.lt (α := ℝ≥0∞) ((μ.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ∫⁻ (x : α) in u, f x ∂μ.restrict (s ∪ t) = ∫⁻ (x : α) in u, g x ∂μ.restrict (s ∪ t)
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf.restrict hg.restrict
    fun u hu huμ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hgi : ∫⁻ (x : α), g x ∂μ ≠ ∞
hfg :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
u : Set α
hu : MeasurableSet u
huμ : LT.lt (α := ℝ≥0∞) ((μ.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in u, f x ∂μ.restrict (s ∪ t) = ∫⁻ (x : α) in u, g x ∂μ.restrict (s ∪ t)
have rw : ∫⁻ (x : α) in u ∩ (s ∪ t), f x ∂μ = ∫⁻ (x : α) in u ∩ (s ∪ t), g x ∂μ
Tactic: rw [Measure.restrict_restrict hu]