awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
⊢ NullMeasurableSet t ν
have obtain : ∀ (x : α) (hxs : x ∈ s) (hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u), NullMeasurableSet t ν
Tactic: obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, (Prod.mk x ⁻¹' (s ×ˢ t)) =ᵐ[ν] (Prod.mk x ⁻¹' u) :=
    ((frequently_ae_iff.2 hs).and_eventually (ae_ae_eq_curry_of_prod hu)).exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u
⊢ NullMeasurableSet t ν
have refine : t =ᶠ[ae ν] Prod.mk x ⁻¹' u
Tactic: refine ⟨Prod.mk x ⁻¹' u, measurable_prodMk_left hum, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
s : Set α
t : Set β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : Set (α × β)
hum : MeasurableSet u
hu : s ×ˢ t =ᶠ[ae (μ.prod ν)] u
x : α
hxs : x ∈ s
hx : Prod.mk x ⁻¹' s ×ˢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u
⊢ t =ᶠ[ae ν] Prod.mk x ⁻¹' u
have rwa : ∀ (hx : t =ᶠ[ae ν] Prod.mk x ⁻¹' u), t =ᶠ[ae ν] Prod.mk x ⁻¹' u
Tactic: rwa [mk_preimage_prod_right hxs] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
⊢ (μ.prod ν).FiniteSpanningSetsIn (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
have this : SigmaFinite ν
Tactic: haveI := hν.sigmaFinite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
this : SigmaFinite ν
⊢ (μ.prod ν).FiniteSpanningSetsIn (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
have refine_1 : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞)
      ((fun (n : ℕ) ↦ hμ.set (C := C) (Nat.unpair n).1 ×ˢ hν.set (C := D) (Nat.unpair n).2) n))
    ∞
Tactic: refine
    ⟨fun n => hμ.set n.unpair.1 ×ˢ hν.set n.unpair.2, fun n =>
      mem_image2_of_mem (hμ.set_mem _) (hν.set_mem _), fun n => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
this : SigmaFinite ν
refine_1 :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞)
        ((fun (n : ℕ) ↦ hμ.set (C := C) (Nat.unpair n).1 ×ˢ hν.set (C := D) (Nat.unpair n).2) n))
      ∞
⊢ (μ.prod ν).FiniteSpanningSetsIn (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)
have refine_2 : Eq (α := Set (α × β))
  (⋃ (i : ℕ), (fun (n : ℕ) ↦ hμ.set (C := C) (Nat.unpair n).1 ×ˢ hν.set (C := D) (Nat.unpair n).2) i) univ
Tactic: refine
    ⟨fun n => hμ.set n.unpair.1 ×ˢ hν.set n.unpair.2, fun n =>
      mem_image2_of_mem (hμ.set_mem _) (hν.set_mem _), fun n => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
this : SigmaFinite ν
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞)
      ((fun (n : ℕ) ↦ hμ.set (C := C) (Nat.unpair n).1 ×ˢ hν.set (C := D) (Nat.unpair n).2) n))
    ∞
have refine_1 : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (hμ.set (C := C) (Nat.unpair n).1) : ℝ≥0∞)
    ((ν : (a : Set β) → ℝ≥0∞) (hν.set (C := D) (Nat.unpair n).2) : ℝ≥0∞) <
  ∞
Tactic: rw [prod_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
this : SigmaFinite ν
refine_2 refine_2₁ :
  Eq (α := Set (α × β)) (⋃ (i : ℕ), hμ.set (C := C) (Nat.unpair i).1 ×ˢ hν.set (C := D) (Nat.unpair i).2) univ
⊢ Eq (α := Set (α × β))
    (⋃ (i : ℕ), (fun (n : ℕ) ↦ hμ.set (C := C) (Nat.unpair n).1 ×ˢ hν.set (C := D) (Nat.unpair n).2) i) univ
have refine_2₂ : SProd.sprod (α := Set α) (β := Set β) (⋃ (n : ℕ), hμ.set (C := C) n) (⋃ (n : ℕ), hν.set (C := D) n) = univ
Tactic: simp_rw [iUnion_unpair_prod, hμ.spanning, hν.spanning, univ_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
this : SigmaFinite ν
refine_2 refine_2₁ :
  Eq (α := Set (α × β)) (⋃ (i : ℕ), hμ.set (C := C) (Nat.unpair i).1 ×ˢ hν.set (C := D) (Nat.unpair i).2) univ
refine_2₂ : SProd.sprod (α := Set α) (β := Set β) (⋃ (n : ℕ), hμ.set (C := C) n) (⋃ (n : ℕ), hν.set (C := D) n) = univ
⊢ Eq (α := Set (α × β))
    (⋃ (i : ℕ), (fun (n : ℕ) ↦ hμ.set (C := C) (Nat.unpair n).1 ×ˢ hν.set (C := D) (Nat.unpair n).2) i) univ
have refine_2₃ : SProd.sprod (α := Set α) (β := Set β) univ (⋃ (n : ℕ), hν.set (C := D) n) = univ
Tactic: simp_rw [iUnion_unpair_prod, hμ.spanning, hν.spanning, univ_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ μ' : Measure α
ν_1 ν' : Measure β
τ : Measure γ
inst_3 : SFinite ν_1
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hμ : μ.FiniteSpanningSetsIn C
hν : ν.FiniteSpanningSetsIn D
this : SigmaFinite ν
refine_2 refine_2₁ :
  Eq (α := Set (α × β)) (⋃ (i : ℕ), hμ.set (C := C) (Nat.unpair i).1 ×ˢ hν.set (C := D) (Nat.unpair i).2) univ
refine_2₂ : SProd.sprod (α := Set α) (β := Set β) (⋃ (n : ℕ), hμ.set (C := C) n) (⋃ (n : ℕ), hν.set (C := D) n) = univ
refine_2₃ : SProd.sprod (α := Set α) (β := Set β) univ (⋃ (n : ℕ), hν.set (C := D) n) = univ
⊢ Eq (α := Set (α × β))
    (⋃ (i : ℕ), (fun (n : ℕ) ↦ hμ.set (C := C) (Nat.unpair n).1 ×ˢ hν.set (C := D) (Nat.unpair n).2) i) univ
have refine_2₄ : SProd.sprod (α := Set α) (β := Set β) univ univ = univ
Tactic: simp_rw [iUnion_unpair_prod, hμ.spanning, hν.spanning, univ_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι : Type u_4
m : ι → Measure α
μ : Measure β
inst_2 : SFinite μ
⊢ (sum m).prod μ = sum fun (i : ι) ↦ (m i).prod μ
have h : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((sum m).prod μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((sum fun (i : ι) ↦ (m i).prod μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι' : Type u_4
inst_2 : Countable ι'
m : Measure α
m' : ι' → Measure β
inst_3 : ∀ (n : ι'), SFinite (m' n)
⊢ m.prod (sum m') = sum fun (p : ι') ↦ m.prod (m' p)
have h : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((m.prod (sum m') : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((sum fun (p : ι') ↦ m.prod (m' p) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι' : Type u_4
inst_2 : Countable ι'
m : Measure α
m' : ι' → Measure β
inst_3 : ∀ (n : ι'), SFinite (m' n)
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((m.prod (sum m') : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((sum fun (p : ι') ↦ m.prod (m' p) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h : ∫⁻ (x : α), (sum m' : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m =
  ∑' (i : ι'), ∫⁻ (x : α), (m' i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m
Tactic: simp only [prod_apply hs, hs, sum_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι' : Type u_4
inst_2 : Countable ι'
m : Measure α
m' : ι' → Measure β
inst_3 : ∀ (n : ι'), SFinite (m' n)
s : Set (α × β)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (sum m' : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m =
    ∑' (i : ι'), ∫⁻ (x : α), (m' i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m
have M : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
Tactic: have M : ∀ x, MeasurableSet (Prod.mk x ⁻¹' s) := fun x => measurable_prodMk_left hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι' : Type u_4
inst_2 : Countable ι'
m : Measure α
m' : ι' → Measure β
inst_3 : ∀ (n : ι'), SFinite (m' n)
s : Set (α × β)
hs : MeasurableSet s
M : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ ∫⁻ (x : α), (sum m' : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m =
    ∑' (i : ι'), ∫⁻ (x : α), (m' i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m
have h : ∫⁻ (x : α), ∑' (i : ι'), (m' i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m =
  ∑' (i : ι'), ∫⁻ (x : α), (m' i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m
Tactic: simp_rw [Measure.sum_apply _ (M _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι' : Type u_4
inst_2 : Countable ι'
m : Measure α
m' : ι' → Measure β
inst_3 : ∀ (n : ι'), SFinite (m' n)
s : Set (α × β)
hs : MeasurableSet s
M : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ ∫⁻ (x : α), ∑' (i : ι'), (m' i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m =
    ∑' (i : ι'), ∫⁻ (x : α), (m' i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m
have h : Eq (α := ℝ≥0∞) (∑' (i : ι'), ∫⁻ (a : α), (m' i : (a : Set β) → ℝ≥0∞) (Prod.mk a ⁻¹' s) ∂m)
  (∑' (i : ι'), ∫⁻ (x : α), (m' i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m)
Tactic: rw [lintegral_tsum (fun i ↦ (measurable_measure_prodMk_left hs).aemeasurable)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι : Type u_4
ι' : Type u_5
inst_2 : Countable ι'
m : ι → Measure α
m' : ι' → Measure β
inst_3 : ∀ (n : ι'), SFinite (m' n)
⊢ (sum m).prod (sum m') = sum fun (p : ι × ι') ↦ (m p.1).prod (m' p.2)
have simp_rw : Eq (α := Measure (α × β)) (sum fun (i : ι) ↦ (m i).prod (sum m')) (sum fun (p : ι × ι') ↦ (m p.1).prod (m' p.2))
Tactic: simp_rw [prod_sum_left, prod_sum_right, sum_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι : Type u_4
ι' : Type u_5
inst_2 : Countable ι'
m : ι → Measure α
m' : ι' → Measure β
inst_3 : ∀ (n : ι'), SFinite (m' n)
simp_rw :
  Eq (α := Measure (α × β)) (sum fun (i : ι) ↦ (m i).prod (sum m')) (sum fun (p : ι × ι') ↦ (m p.1).prod (m' p.2))
⊢ (sum m).prod (sum m') = sum fun (p : ι × ι') ↦ (m p.1).prod (m' p.2)
have simp_rw₁ : Eq (α := Measure (α × β)) (sum fun (i : ι) ↦ sum fun (p : ι') ↦ (m i).prod (m' p))
  (sum fun (p : ι × ι') ↦ (m p.1).prod (m' p.2))
Tactic: simp_rw [prod_sum_left, prod_sum_right, sum_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
x : MeasurableSpace α
μ : Measure α
inst_4 : SFinite μ
x_1 : MeasurableSpace β
ν : Measure β
inst_5 : SFinite ν
| μ.prod ν
have rw : (sum (sfiniteSeq μ)).prod (sum (sfiniteSeq ν))
Tactic: rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
x : MeasurableSpace α
μ : Measure α
inst_4 : SFinite μ
x_1 : MeasurableSpace β
ν : Measure β
inst_5 : SFinite ν
⊢ μ.prod ν = sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)
have conv_lhs : (sum (sfiniteSeq μ)).prod (sum (sfiniteSeq ν)) = sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)
Tactic: conv_lhs => rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
x : MeasurableSpace α
μ : Measure α
inst_4 : SFinite μ
x_1 : MeasurableSpace β
ν : Measure β
inst_5 : SFinite ν
⊢ SFinite (μ.prod ν)
have this : μ.prod ν = sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)
Tactic: have : μ.prod ν =
      Measure.sum (fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)) := by
    conv_lhs => rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν]
    apply prod_sum
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ_1 μ' : Measure α_1
ν_1 ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν_1
α : Type u_4
β : Type u_5
x : MeasurableSpace α
μ : Measure α
inst_4 : SFinite μ
x_1 : MeasurableSpace β
ν : Measure β
inst_5 : SFinite ν
this : μ.prod ν = sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)
⊢ SFinite (μ.prod ν)
have rw : SFinite (α := α × β) (m0 := Prod.instMeasurableSpace) (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst
hD : generateFrom D = inst_1
h2C : IsPiSystem C
h2D : IsPiSystem D
h3C : μ.FiniteSpanningSetsIn C
h3D : ν.FiniteSpanningSetsIn D
μν : Measure (α × β)
h₁ :
  ∀ s ∈ C,
    ∀ t ∈ D,
      (μν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ μ.prod ν = μν
have hC₁ : ∀ (s : Set (α × β)),
  Membership.mem (γ := Set (Set (α × β))) (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D) s →
    Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((μν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine
    (h3C.prod h3D).ext
      (generateFrom_eq_prod hC hD h3C.isCountablySpanning h3D.isCountablySpanning).symm
      (h2C.prod h2D) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst
hD : generateFrom D = inst_1
h2C : IsPiSystem C
h2D : IsPiSystem D
h3C : μ.FiniteSpanningSetsIn C
h3D : ν.FiniteSpanningSetsIn D
μν : Measure (α × β)
h₁ :
  ∀ s ∈ C,
    ∀ t ∈ D,
      (μν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t))
    ((μν : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t))
have this : SigmaFinite ν
Tactic: haveI := h3D.sigmaFinite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst
hD : generateFrom D = inst_1
h2C : IsPiSystem C
h2D : IsPiSystem D
h3C : μ.FiniteSpanningSetsIn C
h3D : ν.FiniteSpanningSetsIn D
μν : Measure (α × β)
h₁ :
  ∀ s ∈ C,
    ∀ t ∈ D,
      (μν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
this : SigmaFinite ν
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t))
    ((μν : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t))
have rw : (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [h₁ s hs t ht, prod_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
C : Set (Set α)
D : Set (Set β)
hC : generateFrom C = inst
hD : generateFrom D = inst_1
h2C : IsPiSystem C
h2D : IsPiSystem D
h3C : μ.FiniteSpanningSetsIn C
h3D : ν.FiniteSpanningSetsIn D
μν : Measure (α × β)
h₁ :
  ∀ s ∈ C,
    ∀ t ∈ D,
      (μν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
this : SigmaFinite ν
rw :
  (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t))
    ((μν : (a : Set (α × β)) → ℝ≥0∞) ((fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) s t))
have rw₁ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [h₁ s hs t ht, prod_prod]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β},
    MeasurableSet s →
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
⊢ μ = ν
have h₁ : ∀ (s : Set (α × β)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β},
    MeasurableSet s →
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
  ((ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
Tactic: rw [← univ_prod_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β},
    MeasurableSet s →
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
s : Set (α × β)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: have h_univ : μ univ = ν univ := by
    rw [← univ_prod_univ]
    exact h .univ .univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β},
    MeasurableSet s →
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
s : Set (α × β)
hs : MeasurableSet s
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have this : IsFiniteMeasure ν
Tactic: have : IsFiniteMeasure ν := ⟨by simp [← h_univ]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure (α × β)
inst : IsFiniteMeasure μ
h :
  ∀ {s : Set α} {t : Set β},
    MeasurableSet s →
      MeasurableSet t →
        Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) : ℝ≥0∞)
s : Set (α × β)
hs : MeasurableSet s
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)
this : IsFiniteMeasure ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∀ (t : Set (α × β))
  (ht :
    Membership.mem (γ := Set (Set (α × β)))
      (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
      t),
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: refine MeasurableSpace.induction_on_inter generateFrom_prod.symm isPiSystem_prod (by simp)
    ?_ ?_ ?_ s hs