awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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∞)
⊢ 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
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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

Tactic:
le_antisymm ?_ bot_le

Premises used: Set.Mem, Filter.Eventually, setOf, le_antisymm, Filter.EventuallyLE, bot_le
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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)
refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ f x ≤ g x) x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f ≤ᶠ[ae μ] g

Tactic:
refine le_antisymm ?_ bot_le

Premises used: le_antisymm, bot_le
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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∞)
    ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n) : ℝ≥0∞)

Tactic:
measure_mono B

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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∞) (⋃ (n : ℕ), s n) : ℝ≥0∞)
    (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞)

Tactic:
measure_iUnion_le _

Premises used: MeasureTheory.measure_iUnion_le
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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)
⊢ Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s n)) 0

Tactic:
simp only [μs, tsum_zero]

Premises used: tsum_zero
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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)
μ₁ : Eq (α := ℝ≥0∞) (∑' (n : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s n)) 0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ f x ≤ g x) x}ᶜ : ℝ≥0∞) (0 : ℝ≥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]

Premises used: Compl.compl, setOf, LE.le, MeasureTheory.measure_iUnion_le, MeasureTheory.measure_mono, DFunLike.coe, Set.iUnion
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : Measurable 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 ∂μ
⊢ f ≤ᶠ[ae μ] g

Tactic:
ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hf.aemeasurable h

Premises used: Measurable.aemeasurable, MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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

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)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
⊢ 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)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
x : α
⊢ f x ≤ g x → g x ≤ f x → f x = g x

Tactic:
le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
h₂ h₃ : ∀ (x : α), f x ≤ g x → g x ≤ f x → f x = g x
⊢ f =ᶠ[ae μ] g

Tactic:
filter_upwards [A, B] with x using le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable 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

Tactic:
ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf.aemeasurable hg.aemeasurable h

Premises used: Measurable.aemeasurable, MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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 ∂μ
⊢ AEFinStronglyMeasurable f μ

Tactic:
have hf' : AEFinStronglyMeasurable f μ :=
    ENNReal.aefinStronglyMeasurable_of_aemeasurable hfi hf
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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 μ
⊢ AEFinStronglyMeasurable g μ

Tactic:
have hg' : AEFinStronglyMeasurable g μ :=
    ENNReal.aefinStronglyMeasurable_of_aemeasurable hgi hg
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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

Tactic:
ae_of_ae_restrict_of_ae_restrict_compl _ this ?_

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
refine : ∀ᵐ (x : α) ∂μ.restrict (s ∪ t)ᶜ, f x = g x
⊢ f =ᶠ[ae μ] g

Tactic:
refine ae_of_ae_restrict_of_ae_restrict_compl _ this ?_

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
simp : ∀ᵐ (x : α) ∂μ.restrict (sᶜ ∩ tᶜ), f x = g x
⊢ ∀ᵐ (x : α) ∂μ.restrict (s ∪ t)ᶜ, f x = g x

Tactic:
simp only [Set.compl_union]

Premises used: Set.compl_union
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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 (μ.restrict sᶜ)] 0

Tactic:
have h1 : f =ᵐ[μ.restrict sᶜ] 0 := hf'.ae_eq_zero_compl
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
⊢ g =ᶠ[ae (μ.restrict tᶜ)] 0

Tactic:
have h2 : g =ᵐ[μ.restrict tᶜ] 0 := hg'.ae_eq_zero_compl
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
rw : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x
⊢ ∀ᵐ (x : α) ∂μ.restrict (sᶜ ∩ tᶜ), f x = g x

Tactic:
rw [ae_restrict_iff' (hf'.measurableSet.compl.inter hg'.measurableSet.compl)]

Premises used: MeasureTheory.AEFinStronglyMeasurable.measurableSet, MeasurableSet.compl, MeasureTheory.ae_restrict_iff', MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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ᶜ → f x = 0 x

Tactic:
rw [EventuallyEq, ae_restrict_iff' hf'.measurableSet.compl] at h1

Premises used: MeasureTheory.AEFinStronglyMeasurable.measurableSet, Filter.EventuallyEq, MeasurableSet.compl, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
h1₁ : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
⊢ g =ᶠ[ae (μ.restrict tᶜ)] 0

Tactic:
rw [EventuallyEq, ae_restrict_iff' hf'.measurableSet.compl] at h1

Premises used: MeasureTheory.AEFinStronglyMeasurable.measurableSet, Filter.EventuallyEq, MeasurableSet.compl, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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 ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x

Tactic:
rw [EventuallyEq, ae_restrict_iff' hg'.measurableSet.compl] at h2

Premises used: MeasureTheory.AEFinStronglyMeasurable.measurableSet, Filter.EventuallyEq, MeasurableSet.compl, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
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
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x

Tactic:
filter_upwards [h1, h2] with x h1 h2 hx
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
h₁ h₂ : Eq (α := ℝ≥0∞) (0 x) (0 x)
⊢ f x = g x

Tactic:
rw [h1 (Set.inter_subset_left hx), h2 (Set.inter_subset_right hx)]

Premises used: Set.inter_subset_left, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
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
suffices : f =ᶠ[ae (μ.restrict (s ∪ t))] g
⊢ f =ᶠ[ae μ] 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)]