awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prod
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))
      ∞
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
⊢ (μ.prod ν).FiniteSpanningSetsIn (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) C D)

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 => ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : ℕ
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∞) <
    ∞
⊢ 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:
rw [prod_prod]

Premises used: MeasureTheory.Measure.prod_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : ℕ
⊢ 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:
mul_lt_top (hμ.finite _) (hν.finite _)

Premises used: ENNReal.mul_lt_top, MeasureTheory.Measure.FiniteSpanningSetsIn.finite
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : ℕ
⊢ 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:
exact mul_lt_top (hμ.finite _) (hν.finite _)

Premises used: ENNReal.mul_lt_top, MeasureTheory.Measure.FiniteSpanningSetsIn.finite
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
refine_2₄ : SProd.sprod (α := Set α) (β := Set β) univ univ = univ
⊢ Eq (α := Set (α × β))
    (⋃ (i : ℕ), (fun (n : ℕ) ↦ hμ.set (C := C) (Nat.unpair n).1 ×ˢ hν.set (C := D) (Nat.unpair n).2) i) univ

Tactic:
simp_rw [iUnion_unpair_prod, hμ.spanning, hν.spanning, univ_prod_univ]

Premises used: Set.iUnion_unpair_prod, Set.univ_prod_univ, MeasureTheory.Measure.FiniteSpanningSetsIn.spanning
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι : Type u_4
m : ι → Measure α
μ : Measure β
inst_2 : SFinite μ
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∞)
⊢ (sum m).prod μ = sum fun (i : ι) ↦ (m i).prod μ

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι : Type u_4
m : ι → Measure α
μ : Measure β
inst_2 : SFinite μ
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:
simp only [prod_apply hs, lintegral_sum_measure, hs, sum_apply]

Premises used: MeasureTheory.Measure.prod_apply, MeasureTheory.Measure.sum_apply, MeasureTheory.lintegral_sum_measure
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)
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∞)
⊢ m.prod (sum m') = sum fun (p : ι') ↦ m.prod (m' p)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
h :
  ∫⁻ (x : α), (sum m' : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m =
    ∑' (i : ι'), ∫⁻ (x : α), (m' i : (a : Set β) → ℝ≥0∞) (Prod.mk x ⁻¹' s) ∂m
⊢ Eq (α := ℝ≥0∞) ((m.prod (sum m') : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
    ((sum fun (p : ι') ↦ m.prod (m' p) : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [prod_apply hs, hs, sum_apply]

Premises used: MeasureTheory.Measure.prod_apply, MeasureTheory.Measure.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : α), MeasurableSet (Prod.mk x ⁻¹' s)

Tactic:
have M : ∀ x, MeasurableSet (Prod.mk x ⁻¹' s) := fun x => measurable_prodMk_left hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)
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
⊢ ∫⁻ (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_rw [Measure.sum_apply _ (M _)]

Premises used: MeasureTheory.Measure.sum_apply
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)
h 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)
⊢ ∫⁻ (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:
rw [lintegral_tsum (fun i ↦ (measurable_measure_prodMk_left hs).aemeasurable)]

Premises used: Measurable.aemeasurable, measurable_measure_prodMk_left, MeasureTheory.lintegral_tsum
-- Module: Mathlib.MeasureTheory.Measure.Prod
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))
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))
⊢ (sum m).prod (sum m') = sum fun (p : ι × ι') ↦ (m p.1).prod (m' p.2)

Tactic:
simp_rw [prod_sum_left, prod_sum_right, sum_sum]

Premises used: MeasureTheory.Measure.sum_sum, MeasureTheory.Measure.prod_sum_right, MeasureTheory.Measure.prod_sum_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 : SigmaFinite μ
x_1 : MeasurableSpace β
ν : Measure β
inst_5 : SigmaFinite ν
⊢ SigmaFinite (μ.prod ν)

Tactic:
(μ.toFiniteSpanningSetsIn.prod ν.toFiniteSpanningSetsIn).sigmaFinite

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.sigmaFinite, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.Measure.FiniteSpanningSetsIn.prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 ν
rw : (sum (sfiniteSeq μ)).prod (sum (sfiniteSeq ν))
| μ.prod ν

Tactic:
rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν]

Premises used: MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 ν
conv_lhs :
  (sum (sfiniteSeq μ)).prod (sum (sfiniteSeq ν)) = sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)
⊢ μ.prod ν = sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)

Tactic:
conv_lhs => rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν]

Premises used: MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 ν
⊢ (sum (sfiniteSeq μ)).prod (sum (sfiniteSeq ν)) = sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)

Tactic:
apply prod_sum

Premises used: MeasureTheory.Measure.prod_sum
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)

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
-- Module: Mathlib.MeasureTheory.Measure.Prod
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)
rw :
  SFinite (α := α × β) (m0 := Prod.instMeasurableSpace)
    (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2))
⊢ SFinite (μ.prod ν)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 (α := α × β) (m0 := Prod.instMeasurableSpace)
    (sum fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ μ' : Measure α_1
ν ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν
α : Type u_4
β : Type u_5
inst_4 : MeasureSpace α
inst_5 : SigmaFinite.{u_4} (α := α) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_6 : MeasureSpace β
inst_7 : SigmaFinite.{u_5} (α := β) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ SigmaFinite (α := α × β) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
prod.instSigmaFinite

Premises used: MeasureTheory.Measure.prod.instSigmaFinite
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
inst : MeasurableSpace α_1
inst_1 : MeasurableSpace β_1
inst_2 : MeasurableSpace γ
μ μ' : Measure α_1
ν ν' : Measure β_1
τ : Measure γ
inst_3 : SFinite ν
α : Type u_4
β : Type u_5
inst_4 : MeasureSpace α
inst_5 : SFinite.{u_4} (α := α) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_6 : MeasureSpace β
inst_7 : SFinite.{u_5} (α := β) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ SFinite (α := α × β) (m0 := MeasureSpace.toMeasurableSpace) volume

Tactic:
prod.instSFinite

Premises used: MeasureTheory.Measure.prod.instSFinite
-- Module: Mathlib.MeasureTheory.Measure.Prod
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 ν = μν

Tactic:
(h3C.prod h3D).ext
      (generateFrom_eq_prod hC hD h3C.isCountablySpanning h3D.isCountablySpanning).symm
      (h2C.prod h2D) ?_

Premises used: IsPiSystem.prod, generateFrom_eq_prod, Eq.symm, MeasureTheory.Measure.FiniteSpanningSetsIn.prod, MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning, MeasureTheory.Measure.FiniteSpanningSetsIn.ext
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
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∞)
⊢ μ.prod ν = μν

Tactic:
refine
    (h3C.prod h3D).ext
      (generateFrom_eq_prod hC hD h3C.isCountablySpanning h3D.isCountablySpanning).symm
      (h2C.prod h2D) ?_

Premises used: IsPiSystem.prod, generateFrom_eq_prod, Eq.symm, MeasureTheory.Measure.FiniteSpanningSetsIn.prod, MeasureTheory.Measure.FiniteSpanningSetsIn.isCountablySpanning, MeasureTheory.Measure.FiniteSpanningSetsIn.ext
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
⊢ SigmaFinite ν

Tactic:
haveI := h3D.sigmaFinite
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
rw₁ 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∞)
⊢ 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))

Tactic:
rw [h₁ s hs t ht, prod_prod]

Premises used: MeasureTheory.Measure.prod_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SigmaFinite μ
ν : Measure β
inst_3 : SigmaFinite ν
μν : Measure (α × β)
h :
  ∀ (s : Set α) (t : Set β),
    MeasurableSet s →
      MeasurableSet t →
        (μν : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ μ.prod ν = μν

Tactic:
prod_eq_generateFrom generateFrom_measurableSet generateFrom_measurableSet
    isPiSystem_measurableSet isPiSystem_measurableSet μ.toFiniteSpanningSetsIn
    ν.toFiniteSpanningSetsIn fun s hs t ht => h s t hs ht

Premises used: MeasureTheory.Measure.prod_eq_generateFrom, MeasurableSpace.isPiSystem_measurableSet, MeasurableSpace.generateFrom_measurableSet, MeasureTheory.Measure.toFiniteSpanningSetsIn
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
h₁ :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
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
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
    ((ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [← univ_prod_univ]

Premises used: Set.univ_prod_univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
    ((ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)

Tactic:
h .univ .univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)
    ((ν : (a : Set (α × β)) → ℝ≥0∞) (SProd.sprod (α := Set α) (β := Set β) univ univ) : ℝ≥0∞)

Tactic:
exact h .univ .univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)

Tactic:
have h_univ : μ univ = ν univ := by
    rw [← univ_prod_univ]
    exact h .univ .univ
-- Module: Mathlib.MeasureTheory.Measure.Prod
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set (α × β)) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [← h_univ]