awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
u : Set α
hu : MeasurableSet u
huμ : LT.lt (α := ℝ≥0∞) ((μ.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in u ∩ (s ∪ t), f x ∂μ = ∫⁻ (x : α) in u ∩ (s ∪ t), g x ∂μ
have huμ₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ (s ∪ t)) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply hu] at huμ
Cleared hypotheses: huμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ (t : Set α), MeasurableSet t → ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
have refine_1 : ∫⁻ (x : α) in ∅, f x ∂μ = ∫⁻ (x : α) in ∅, g x ∂μ
Tactic: refine MeasurableSpace.induction_on_inter h_eq h_inter ?_ basic ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
refine_1 : ∫⁻ (x : α) in ∅, f x ∂μ = ∫⁻ (x : α) in ∅, g x ∂μ
⊢ ∀ (t : Set α), MeasurableSet t → ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
have refine_2 : ∀ (t : Set α) (htm : MeasurableSet t),
  ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ → ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ
Tactic: refine MeasurableSpace.induction_on_inter h_eq h_inter ?_ basic ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
refine_1 : ∫⁻ (x : α) in ∅, f x ∂μ = ∫⁻ (x : α) in ∅, g x ∂μ
refine_2 :
  ∀ (t : Set α) (htm : MeasurableSet t),
    ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ → ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ
⊢ ∀ (t : Set α), MeasurableSet t → ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
have refine_3 : ∀ (f_1 : ℕ → Set α),
  Pairwise (Function.onFun Disjoint f_1) →
    ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f_1 i)),
      (∀ (i : ℕ), ∫⁻ (x : α) in f_1 i, f x ∂μ = ∫⁻ (x : α) in f_1 i, g x ∂μ) →
        ∫⁻ (x : α) in ⋃ (i : ℕ), f_1 i, f x ∂μ = ∫⁻ (x : α) in ⋃ (i : ℕ), f_1 i, g x ∂μ
Tactic: refine MeasurableSpace.induction_on_inter h_eq h_inter ?_ basic ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ
have refine_2 : ∫⁻ (x : α) in t, g x ∂μ ≠ ∞
Tactic: rw [setLIntegral_compl ht, setLIntegral_compl ht, h_eq, h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
refine_2 : ∫⁻ (x : α) in t, g x ∂μ ≠ ∞
⊢ ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ
have refine_2₁ : ∫⁻ (x : α) in t, f x ∂μ ≠ ∞
Tactic: rw [setLIntegral_compl ht, setLIntegral_compl ht, h_eq, h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in t, g x ∂μ ≠ ∞
have refine_2 : ∫⁻ (x : α) in t, g x ∂μ < ∞
Tactic: refine ne_of_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α), g x ∂μ < ∞
have rw : ∫⁻ (x : α), f x ∂μ < ∞
Tactic: rw [← h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in t, g x ∂μ < ∞
have calc : ∫⁻ (x : α), g x ∂μ < ∞
Tactic: calc ∫⁻ x in t, g x ∂μ
      _ ≤ ∫⁻ x, g x ∂μ := setLIntegral_le_lintegral t _
      _ < ∞ := by rw [← h_univ]; exact hf_int.lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in t, f x ∂μ ≠ ∞
have refine_2 : ∫⁻ (x : α) in t, f x ∂μ < ∞
Tactic: refine ne_of_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : ℕ → Set α
htd : Pairwise (Function.onFun Disjoint t)
htm : ∀ (i : ℕ), MeasurableSet (t i)
h : ∀ (i : ℕ), ∫⁻ (x : α) in t i, f x ∂μ = ∫⁻ (x : α) in t i, g x ∂μ
⊢ ∫⁻ (x : α) in ⋃ (i : ℕ), t i, f x ∂μ = ∫⁻ (x : α) in ⋃ (i : ℕ), t i, g x ∂μ
have refine_3 : Eq (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (x : α) in t i, f x ∂μ) (∑' (i : ℕ), ∫⁻ (x : α) in t i, g x ∂μ)
Tactic: simp_rw [lintegral_iUnion htm htd, h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
h_univ : Set.univ ∈ s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
have refine : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
Tactic: refine lintegral_eq_lintegral_of_isPiSystem h_eq h_inter basic ?_ hf_int t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
h_univ : Set.univ ∈ s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
have rw : ∫⁻ (x : α) in Set.univ, f x ∂μ = ∫⁻ (x : α) in Set.univ, g x ∂μ
Tactic: rw [← setLIntegral_univ, ← setLIntegral_univ g]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
⊢ ∫⁻ (x : α × β), g x ∂μ ≠ ∞
have rwa : ∫⁻ (x : α × β) in Set.univ, g x ∂μ ≠ ∞
Tactic: rwa [← setLIntegral_univ, ← Set.univ_prod_univ, ← h .univ .univ, Set.univ_prod_univ,
      setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
rwa : ∫⁻ (x : α × β) in Set.univ, g x ∂μ ≠ ∞
⊢ ∫⁻ (x : α × β), g x ∂μ ≠ ∞
have rwa₁ : ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) Set.univ Set.univ, g x ∂μ ≠ ∞
Tactic: rwa [← setLIntegral_univ, ← Set.univ_prod_univ, ← h .univ .univ, Set.univ_prod_univ,
      setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
rwa : ∫⁻ (x : α × β) in Set.univ, g x ∂μ ≠ ∞
rwa₁ : ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) Set.univ Set.univ, g x ∂μ ≠ ∞
⊢ ∫⁻ (x : α × β), g x ∂μ ≠ ∞
have rwa₂ : ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) Set.univ Set.univ, f x ∂μ ≠ ∞
Tactic: rwa [← setLIntegral_univ, ← Set.univ_prod_univ, ← h .univ .univ, Set.univ_prod_univ,
      setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
rwa : ∫⁻ (x : α × β) in Set.univ, g x ∂μ ≠ ∞
rwa₁ : ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) Set.univ Set.univ, g x ∂μ ≠ ∞
rwa₂ : ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) Set.univ Set.univ, f x ∂μ ≠ ∞
⊢ ∫⁻ (x : α × β), g x ∂μ ≠ ∞
have rwa₃ : ∫⁻ (x : α × β) in Set.univ, f x ∂μ ≠ ∞
Tactic: rwa [← setLIntegral_univ, ← Set.univ_prod_univ, ← h .univ .univ, Set.univ_prod_univ,
      setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
⊢ f =ᶠ[ae μ] g
have hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
Tactic: have hg_int : ∫⁻ x, g x ∂μ ≠ ∞ := by
    rwa [← setLIntegral_univ, ← Set.univ_prod_univ, ← h .univ .univ, Set.univ_prod_univ,
      setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
⊢ f =ᶠ[ae μ] g
have refine : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ∫⁻ (x : α × β) in s, f x ∂μ = ∫⁻ (x : α × β) in s, g x ∂μ
Tactic: refine AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hf_int hg_int fun s hs _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α × β) in s, f x ∂μ = ∫⁻ (x : α × β) in s, g x ∂μ
have refine_1 : Membership.mem (γ := Set (Set (α × β)))
  (Set.image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
  Set.univ
Tactic: refine lintegral_eq_lintegral_of_isPiSystem_of_univ_mem generateFrom_prod.symm isPiSystem_prod
    ?_ ?_ hf_int hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  Membership.mem (γ := Set (Set (α × β)))
    (Set.image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
    Set.univ
⊢ ∫⁻ (x : α × β) in s, f x ∂μ = ∫⁻ (x : α × β) in s, g x ∂μ
have refine_2 : ∀ (t : Set (α × β)),
  Membership.mem (γ := Set (Set (α × β)))
      (Set.image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s}
        {t : Set β | MeasurableSet t})
      t →
    ∫⁻ (x : α × β) in t, f x ∂μ = ∫⁻ (x : α × β) in t, g x ∂μ
Tactic: refine lintegral_eq_lintegral_of_isPiSystem_of_univ_mem generateFrom_prod.symm isPiSystem_prod
    ?_ ?_ hf_int hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
⊢ f =ᶠ[ae μ] g
have refine : ∀ (s : Set α) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
Tactic: refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf hg fun s hs _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
have rw : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (x : α) in s, g x ∂μ
Tactic: rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (x : α) in s, g x ∂μ
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
have rw₁ : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (x : α) in s, g x ∂μ
rw₁ : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
have rw₂ : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
⊢ f =ᶠ[ae μ] g
have refine_1 : ∫⁻ (x : α), g x ∂μ ≠ ∞
Tactic: refine AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hfi ?_ fun s hs _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
refine_1 : ∫⁻ (x : α), g x ∂μ ≠ ∞
⊢ f =ᶠ[ae μ] g
have refine_2 : ∀ (s : Set α) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
Tactic: refine AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hfi ?_ fun s hs _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
⊢ ∫⁻ (x : α), g x ∂μ ≠ ∞
have refine_1 : ∫⁻ (x : α) in Set.univ, g x ∂μ ≠ ∞
Tactic: rwa [← setLIntegral_univ, ← withDensity_apply g MeasurableSet.univ, ← hfg,
        withDensity_apply f MeasurableSet.univ, setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
refine_1 : ∫⁻ (x : α) in Set.univ, g x ∂μ ≠ ∞
⊢ ∫⁻ (x : α), g x ∂μ ≠ ∞
have refine_1₁ : Ne (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [← setLIntegral_univ, ← withDensity_apply g MeasurableSet.univ, ← hfg,
        withDensity_apply f MeasurableSet.univ, setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
refine_1 : ∫⁻ (x : α) in Set.univ, g x ∂μ ≠ ∞
refine_1₁ : Ne (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α), g x ∂μ ≠ ∞
have refine_1₂ : Ne (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [← setLIntegral_univ, ← withDensity_apply g MeasurableSet.univ, ← hfg,
        withDensity_apply f MeasurableSet.univ, setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
refine_1 : ∫⁻ (x : α) in Set.univ, g x ∂μ ≠ ∞
refine_1₁ : Ne (α := ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1₂ : Ne (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α), g x ∂μ ≠ ∞
have refine_1₃ : ∫⁻ (a : α) in Set.univ, f a ∂μ ≠ ∞
Tactic: rwa [← setLIntegral_univ, ← withDensity_apply g MeasurableSet.univ, ← hfg,
        withDensity_apply f MeasurableSet.univ, setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
have refine_2 : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (x : α) in s, g x ∂μ
Tactic: rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (x : α) in s, g x ∂μ
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
have refine_2₁ : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfLIntegral (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
hfg : μ.withDensity f = μ.withDensity g
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : (μ.withDensity f : (a : Set α) → ℝ≥0∞) s = ∫⁻ (x : α) in s, g x ∂μ
refine_2₁ :
  Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
have refine_2₂ : Eq (α := ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ.withDensity f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← withDensity_apply f hs, ← withDensity_apply g hs, ← hfg]