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 α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
⊢ Eq (α := Measure (α × β × γ))
    (sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
    (sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)))

Tactic:
have : sum (fun (p : ℕ × ℕ × ℕ) ↦
        (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
      = sum (fun (p : (ℕ × ℕ) × ℕ) ↦
        (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))) := by
    ext s hs
    rw [sum_apply _ hs, sum_apply _ hs, ← (Equiv.prodAssoc _ _ _).tsum_eq]
    simp only [Equiv.prodAssoc_apply]
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
this :
  Eq (α := Measure (α × β × γ))
    (sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
    (sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)))
rw :
  Eq (α := Measure (α × β × γ))
    (sum fun (i : (ℕ × ℕ) × ℕ) ↦
      map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
        (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)))
    (sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)))
⊢ map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)

Tactic:
rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, ← sum_sfiniteSeq τ, prod_sum, prod_sum,
    map_sum MeasurableEquiv.prodAssoc.measurable.aemeasurable, prod_sum, prod_sum, this]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.map_sum, MeasureTheory.sum_sfiniteSeq, MeasurableEquiv.prodAssoc, MeasureTheory.Measure.prod_sum, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
this :
  Eq (α := Measure (α × β × γ))
    (sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
    (sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)))
e_f :
  Eq (α := (ℕ × ℕ) × ℕ → Measure (α × β × γ))
    (fun (i : (ℕ × ℕ) × ℕ) ↦
      map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
        (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)))
    fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))
⊢ Eq (α := Measure (α × β × γ))
    (sum fun (i : (ℕ × ℕ) × ℕ) ↦
      map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
        (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)))
    (sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)))

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
this :
  Eq (α := Measure (α × β × γ))
    (sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
    (sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)))
e_f :
  ∀ (i : (ℕ × ℕ) × ℕ),
    map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
        (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)) =
      (sfiniteSeq μ i.1.1).prod ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2))
⊢ Eq (α := (ℕ × ℕ) × ℕ → Measure (α × β × γ))
    (fun (i : (ℕ × ℕ) × ℕ) ↦
      map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
        (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)))
    fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))

Tactic:
ext1 i
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
this :
  Eq (α := Measure (α × β × γ))
    (sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
    (sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)))
i : (ℕ × ℕ) × ℕ
⊢ map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
      (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)) =
    (sfiniteSeq μ i.1.1).prod ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2))

Tactic:
(prod_eq_generateFrom generateFrom_measurableSet generateFrom_prod
    isPiSystem_measurableSet isPiSystem_prod ((sfiniteSeq μ i.1.1)).toFiniteSpanningSetsIn
    ((sfiniteSeq ν i.1.2).toFiniteSpanningSetsIn.prod (sfiniteSeq τ i.2).toFiniteSpanningSetsIn)
      ?_).symm

Premises used: MeasureTheory.Measure.prod_eq_generateFrom, isPiSystem_prod, MeasurableSpace.isPiSystem_measurableSet, MeasurableSpace.generateFrom_measurableSet, generateFrom_prod, Prod.fst, MeasureTheory.Measure.toFiniteSpanningSetsIn, Eq.symm, Prod.snd, MeasureTheory.Measure.FiniteSpanningSetsIn.prod, MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
this :
  Eq (α := Measure (α × β × γ))
    (sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
    (sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)))
i : (ℕ × ℕ) × ℕ
e_f :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s →
      ∀ (t : Set (β × γ)),
        Membership.mem (γ := Set (Set (β × γ)))
            (image2 (fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) {s : Set β | MeasurableSet s}
              {t : Set γ | MeasurableSet t})
            t →
          (map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
                  (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)) :
                (a : Set (α × β × γ)) → ℝ≥0∞)
              (s ×ˢ t) =
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
              (((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2) : (a : Set (β × γ)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
      (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)) =
    (sfiniteSeq μ i.1.1).prod ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2))

Tactic:
refine (prod_eq_generateFrom generateFrom_measurableSet generateFrom_prod
    isPiSystem_measurableSet isPiSystem_prod ((sfiniteSeq μ i.1.1)).toFiniteSpanningSetsIn
    ((sfiniteSeq ν i.1.2).toFiniteSpanningSetsIn.prod (sfiniteSeq τ i.2).toFiniteSpanningSetsIn)
      ?_).symm

Premises used: MeasureTheory.Measure.prod_eq_generateFrom, isPiSystem_prod, MeasurableSpace.isPiSystem_measurableSet, MeasurableSpace.generateFrom_measurableSet, generateFrom_prod, Prod.fst, MeasureTheory.Measure.toFiniteSpanningSetsIn, Eq.symm, Prod.snd, MeasureTheory.Measure.FiniteSpanningSetsIn.prod, MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
this :
  Eq (α := Measure (α × β × γ))
    (sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)))
    (sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)))
i : (ℕ × ℕ) × ℕ
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | MeasurableSet s} s
t : Set β
ht : Membership.mem (γ := Set (Set β)) {s : Set β | MeasurableSet s} t
u : Set γ
hu : Membership.mem (γ := Set (Set γ)) {t : Set γ | MeasurableSet t} u
e_f :
  ∀ (hs : MeasurableSet s) (t : Set β) (ht : MeasurableSet t) (u : Set γ) (hu : MeasurableSet u),
    (map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
            (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)) :
          (a : Set (α × β × γ)) → ℝ≥0∞)
        (SProd.sprod (β := Set (β × γ)) s ((fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) t u)) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2) : (a : Set (β × γ)) → ℝ≥0∞)
            ((fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) t u) :
          ℝ≥0∞)
⊢ (map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
          (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)) :
        (a : Set (α × β × γ)) → ℝ≥0∞)
      (SProd.sprod (β := Set (β × γ)) s ((fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) t u)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2) : (a : Set (β × γ)) → ℝ≥0∞)
          ((fun (x1 : Set β) (x2 : Set γ) ↦ x1 ×ˢ x2) t u) :
        ℝ≥0∞)

Tactic:
rw [mem_setOf_eq] at hs ht hu

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
rw :
  Eq (α := Measure (α × β)) (sum fun (p : ℕ × ℕ) ↦ ((sfiniteSeq μ p.1).restrict s).prod ((sfiniteSeq ν p.2).restrict t))
    (sum fun (i : ℕ × ℕ) ↦ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t))
⊢ (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)

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

Premises used: MeasureTheory.Measure.restrict_sum_of_countable, MeasureTheory.sum_sfiniteSeq, MeasureTheory.Measure.prod_sum
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
e_f :
  Eq (α := ℕ × ℕ → Measure (α × β))
    (fun (p : ℕ × ℕ) ↦ ((sfiniteSeq μ p.1).restrict s).prod ((sfiniteSeq ν p.2).restrict t)) fun (i : ℕ × ℕ) ↦
    ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)
⊢ Eq (α := Measure (α × β)) (sum fun (p : ℕ × ℕ) ↦ ((sfiniteSeq μ p.1).restrict s).prod ((sfiniteSeq ν p.2).restrict t))
    (sum fun (i : ℕ × ℕ) ↦ ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t))

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
e_f :
  ∀ (i : ℕ × ℕ),
    ((sfiniteSeq μ i.1).restrict s).prod ((sfiniteSeq ν i.2).restrict t) =
      ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)
⊢ Eq (α := ℕ × ℕ → Measure (α × β))
    (fun (p : ℕ × ℕ) ↦ ((sfiniteSeq μ p.1).restrict s).prod ((sfiniteSeq ν p.2).restrict t)) fun (i : ℕ × ℕ) ↦
    ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)

Tactic:
ext1 i
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
i : ℕ × ℕ
⊢ ((sfiniteSeq μ i.1).restrict s).prod ((sfiniteSeq ν i.2).restrict t) =
    ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)

Tactic:
prod_eq fun s' t' hs' ht' => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
i : ℕ × ℕ
e_f :
  ∀ (s' : Set α) (t' : Set β) (hs' : MeasurableSet s') (ht' : MeasurableSet t'),
    (((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t) : (a : Set (α × β)) → ℝ≥0∞) (s' ×ˢ t') =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((sfiniteSeq μ i.1).restrict s : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
        (((sfiniteSeq ν i.2).restrict t : (a : Set β) → ℝ≥0∞) t' : ℝ≥0∞)
⊢ ((sfiniteSeq μ i.1).restrict s).prod ((sfiniteSeq ν i.2).restrict t) =
    ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)

Tactic:
refine prod_eq fun s' t' hs' ht' => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
i : ℕ × ℕ
s' : Set α
t' : Set β
hs' : MeasurableSet s'
ht' : MeasurableSet t'
e_f :
  ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) : (a : Set (α × β)) → ℝ≥0∞) (s' ×ˢ t' ∩ s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((sfiniteSeq μ i.1).restrict s : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
      (((sfiniteSeq ν i.2).restrict t : (a : Set β) → ℝ≥0∞) t' : ℝ≥0∞)
e_f₁ :
  ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2) : (a : Set (α × β)) → ℝ≥0∞) ((s' ∩ s) ×ˢ (t' ∩ t)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((sfiniteSeq μ i.1).restrict s : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
      (((sfiniteSeq ν i.2).restrict t : (a : Set β) → ℝ≥0∞) t' : ℝ≥0∞)
e_f₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) (s' ∩ s) : ℝ≥0∞)
      ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) (t' ∩ t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((sfiniteSeq μ i.1).restrict s : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
      (((sfiniteSeq ν i.2).restrict t : (a : Set β) → ℝ≥0∞) t' : ℝ≥0∞)
e_f₃ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) (s' ∩ s) : ℝ≥0∞)
      ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) (t' ∩ t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) (s' ∩ s) : ℝ≥0∞)
      (((sfiniteSeq ν i.2).restrict t : (a : Set β) → ℝ≥0∞) t' : ℝ≥0∞)
e_f₄ e_f₅ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) (s' ∩ s) : ℝ≥0∞)
      ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) (t' ∩ t) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1 : (a : Set α) → ℝ≥0∞) (s' ∩ s) : ℝ≥0∞)
      ((sfiniteSeq ν i.2 : (a : Set β) → ℝ≥0∞) (t' ∩ t) : ℝ≥0∞)
⊢ (((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t) : (a : Set (α × β)) → ℝ≥0∞) (s' ×ˢ t') =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((sfiniteSeq μ i.1).restrict s : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)
      (((sfiniteSeq ν i.2).restrict t : (a : Set β) → ℝ≥0∞) t' : ℝ≥0∞)

Tactic:
rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
    restrict_apply ht']

Premises used: MeasureTheory.Measure.restrict_apply, MeasurableSet.prod, MeasureTheory.Measure.prod_prod, Set.prod_inter_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
⊢ ν = ν.restrict univ

Tactic:
have : ν = ν.restrict Set.univ := Measure.restrict_univ.symm
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
this : ν = ν.restrict univ
rw : (μ.restrict s).prod (ν.restrict univ) = (μ.prod (ν.restrict univ)).restrict (SProd.sprod (β := Set β) s univ)
rw₁ :
  (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ) =
    (μ.prod (ν.restrict univ)).restrict (SProd.sprod (β := Set β) s univ)
rw₂ rw₃ : (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ) = (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ)
⊢ (μ.restrict s).prod ν = (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ)

Tactic:
rw [this, Measure.prod_restrict, ← this]

Premises used: MeasureTheory.Measure.prod_restrict
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
y : β
rw :
  Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (sum fun (i : ℕ) ↦ map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
⊢ Eq (α := Measure (α × β)) (μ.prod (dirac y)) (map (fun (x : α) ↦ (x, y)) μ)

Tactic:
rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prodMk_right.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.map_sum, measurable_prodMk_right, MeasureTheory.sum_sfiniteSeq, MeasureTheory.Measure.prod_sum_left
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
y : β
e_f :
  Eq (α := ℕ → Measure (α × β)) (fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y)) fun (i : ℕ) ↦
    map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i)
⊢ Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (sum fun (i : ℕ) ↦ map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
y : β
e_f :
  ∀ (i : ℕ), Eq (α := Measure (α × β)) ((sfiniteSeq μ i).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
⊢ Eq (α := ℕ → Measure (α × β)) (fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y)) fun (i : ℕ) ↦
    map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i)

Tactic:
ext1 i
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
y : β
i : ℕ
⊢ Eq (α := Measure (α × β)) ((sfiniteSeq μ i).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))

Tactic:
prod_eq fun s t hs ht => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
y : β
i : ℕ
e_f :
  ∀ (s : Set α) (t : Set β) (hs : MeasurableSet s) (ht : MeasurableSet t),
    (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := Measure (α × β)) ((sfiniteSeq μ i).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))

Tactic:
refine prod_eq fun s t hs ht => ?_

Premises used: MeasureTheory.Measure.prod_eq
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
y : β
i : ℕ
s : Set α
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₁ :
  (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) (if y ∈ t then s else ∅) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₂ :
  t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
e_f₃ :
  t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (t.indicator 1 y : ℝ≥0∞)
e_f₄ :
  Eq (α := ℝ≥0∞) (t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y)
    (t.indicator
      (fun (j : β) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 j : ℝ≥0∞)) y)
e_f₅ :
  Eq (α := ℝ≥0∞) (t.indicator (fun (x : β) ↦ (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) y)
    (t.indicator
      (fun (j : β) ↦ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)) y)
⊢ (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, mul_one]

Premises used: MeasureTheory.Measure.map_apply, Pi.one_apply, MeasureTheory.Measure.dirac_apply', measurable_prodMk_right, MeasurableSet.prod, MeasureTheory.measure_if, mul_one, Set.indicator_mul_right, DFunLike.coe, Set.mk_preimage_prod_left_eq_if, MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
y : β
rw : Eq (α := Measure (α × β)) ((sum (sfiniteSeq μ)).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
rw₁ :
  Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (map (fun (x : α) ↦ (x, y)) (sum (sfiniteSeq μ)))
rw₂ rw₃ rw₄ :
  Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (sum fun (i : ℕ) ↦ map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
e_f :
  Eq (α := ℕ → Measure (α × β)) (fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y)) fun (i : ℕ) ↦
    map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i)
e_f₁ :
  ∀ (i : ℕ), Eq (α := Measure (α × β)) ((sfiniteSeq μ i).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
e_f₂ :
  ∀ (i : ℕ) (s : Set α) (t : Set β) (hs : MeasurableSet s) (ht : MeasurableSet t),
    (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i) : (a : Set (α × β)) → ℝ≥0∞) (s ×ˢ t) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (((dirac y : Measure β) : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := Measure (α × β)) (μ.prod (dirac y)) (map (fun (x : α) ↦ (x, y)) μ)

Tactic:
classical
  rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prodMk_right.aemeasurable]
  congr
  ext1 i
  refine prod_eq fun s t hs ht => ?_
  simp_rw [map_apply measurable_prodMk_right (hs.prod ht), mk_preimage_prod_left_eq_if, measure_if,
    dirac_apply' _ ht, ← indicator_mul_right _ fun _ => sfiniteSeq μ i s, Pi.one_apply, mul_one]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.prod_eq, Pi.one_apply, MeasureTheory.Measure.map_sum, measurable_prodMk_right, MeasureTheory.sum_sfiniteSeq, MeasureTheory.measure_if, MeasureTheory.Measure.prod_sum_left, mul_one, Set.mk_preimage_prod_left_eq_if
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : SFinite ν
x : α
rw :
  Eq (α := Measure (α × β)) (sum fun (p : ℕ) ↦ Measure.prod (dirac x) (sfiniteSeq ν p))
    (sum fun (i : ℕ) ↦ map (Prod.mk x) (sfiniteSeq ν i))
⊢ Eq (α := Measure (α × β)) (Measure.prod (dirac x) ν) (map (Prod.mk x) ν)

Tactic:
rw [← sum_sfiniteSeq ν, prod_sum_right, map_sum measurable_prodMk_left.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.map_sum, MeasureTheory.sum_sfiniteSeq, MeasureTheory.Measure.prod_sum_right, measurable_prodMk_left