awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
ν : 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 : MeasurableSet s
t : Set β
ht : MeasurableSet t
u : Set γ
hu : MeasurableSet u
e_f e_f₁ :
  (map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
          (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)) :
        (a : Set (α × β × γ)) → ℝ≥0∞)
      (s ×ˢ 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∞) (t ×ˢ u) : ℝ≥0∞)
e_f₂ :
  (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2) : (a : Set ((α × β) × γ)) → ℝ≥0∞)
      ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ 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∞) (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∞)
have e_f₃ : (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2) : (a : Set ((α × β) × γ)) → ℝ≥0∞)
    ((⇑{ toEquiv := Equiv.prodAssoc α β γ, measurable_toFun := sorry, measurable_invFun := sorry } :
        (a : (α × β) × γ) → α × β × γ) ⁻¹'
      s ×ˢ 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∞) (t ×ˢ u) : ℝ≥0∞)
Tactic: simp_rw [map_apply (MeasurableEquiv.measurable _) (hs.prod (ht.prod hu)),
    MeasurableEquiv.prodAssoc, MeasurableEquiv.coe_mk, Equiv.prod_assoc_preimage, prod_prod,
    mul_assoc]
-- 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 α
ν : 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 : MeasurableSet s
t : Set β
ht : MeasurableSet t
u : Set γ
hu : MeasurableSet u
e_f e_f₁ :
  (map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ)
          (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2)) :
        (a : Set (α × β × γ)) → ℝ≥0∞)
      (s ×ˢ 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∞) (t ×ˢ u) : ℝ≥0∞)
e_f₂ :
  (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2) : (a : Set ((α × β) × γ)) → ℝ≥0∞)
      ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ 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∞) (t ×ˢ u) : ℝ≥0∞)
e_f₃ :
  (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2) : (a : Set ((α × β) × γ)) → ℝ≥0∞)
      ((⇑{ toEquiv := Equiv.prodAssoc α β γ, measurable_toFun := ⋯, measurable_invFun := ⋯ } :
          (a : (α × β) × γ) → α × β × γ) ⁻¹'
        s ×ˢ 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∞) (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∞)
have e_f₄ : (((sfiniteSeq μ i.1.1).prod (sfiniteSeq ν i.1.2)).prod (sfiniteSeq τ i.2) : (a : Set ((α × β) × γ)) → ℝ≥0∞)
    ((⇑(Equiv.prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ 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∞) (t ×ˢ u) : ℝ≥0∞)
Tactic: simp_rw [map_apply (MeasurableEquiv.measurable _) (hs.prod (ht.prod hu)),
    MeasurableEquiv.prodAssoc, MeasurableEquiv.coe_mk, Equiv.prod_assoc_preimage, prod_prod,
    mul_assoc]
-- 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 ν
inst_3 : SFinite μ
s : Set α
t : Set β
⊢ (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
have 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))
Tactic: rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, restrict_sum_of_countable, restrict_sum_of_countable,
    prod_sum, prod_sum, restrict_sum_of_countable]
-- 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 ν
inst_3 : SFinite μ
s : Set α
t : Set β
⊢ 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))
have 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)
Tactic: congr 1
-- 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 ν
inst_3 : SFinite μ
s : Set α
t : Set β
⊢ 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)
have e_f : ∀ (i : ℕ × ℕ),
  ((sfiniteSeq μ i.1).restrict s).prod ((sfiniteSeq ν i.2).restrict t) =
    ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)).restrict (s ×ˢ t)
Tactic: ext1 i
-- 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 ν
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)
have 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∞)
Tactic: refine prod_eq fun s' t' hs' ht' => ?_
-- 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 ν
inst_3 : SFinite μ
s : Set α
t : Set β
i : ℕ × ℕ
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∞)
have 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∞)
Tactic: rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
    restrict_apply ht']
-- 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 ν
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∞)
⊢ (((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∞)
have 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∞)
Tactic: rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
    restrict_apply ht']
-- 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 ν
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∞)
⊢ (((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∞)
have 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∞)
Tactic: rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
    restrict_apply ht']
-- 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 ν
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∞)
⊢ (((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∞)
have 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∞)
Tactic: rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
    restrict_apply ht']
-- 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 ν
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∞)
⊢ (((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∞)
have 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∞)
Tactic: rw [restrict_apply (hs'.prod ht'), prod_inter_prod, prod_prod, restrict_apply hs',
    restrict_apply ht']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
⊢ (μ.restrict s).prod ν = (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ)
have this : ν = ν.restrict univ
Tactic: have : ν = ν.restrict Set.univ := Measure.restrict_univ.symm
-- 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 ν
inst_3 : SFinite μ
s : Set α
this : ν = ν.restrict univ
⊢ (μ.restrict s).prod ν = (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ)
have rw : (μ.restrict s).prod (ν.restrict univ) = (μ.prod (ν.restrict univ)).restrict (SProd.sprod (β := Set β) s univ)
Tactic: rw [this, Measure.prod_restrict, ← 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 β
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)
⊢ (μ.restrict s).prod ν = (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ)
have rw₁ : (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ) =
  (μ.prod (ν.restrict univ)).restrict (SProd.sprod (β := Set β) s univ)
Tactic: rw [this, Measure.prod_restrict, ← 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 β
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)
⊢ (μ.restrict s).prod ν = (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ)
have rw₂ : (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ) = (μ.prod ν).restrict (SProd.sprod (β := Set β) s univ)
Tactic: rw [this, Measure.prod_restrict, ← this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
y : β
⊢ Eq (α := Measure (α × β)) (μ.prod (dirac y)) (map (fun (x : α) ↦ (x, y)) μ)
have rw : Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
  (sum fun (i : ℕ) ↦ map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
Tactic: rw [← sum_sfiniteSeq μ, prod_sum_left, map_sum measurable_prodMk_right.aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
y : β
⊢ Eq (α := Measure (α × β)) (sum fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y))
    (sum fun (i : ℕ) ↦ map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
have e_f : Eq (α := ℕ → Measure (α × β)) (fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y)) fun (i : ℕ) ↦
  map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
inst_2 : SFinite μ
y : β
⊢ Eq (α := ℕ → Measure (α × β)) (fun (i : ℕ) ↦ (sfiniteSeq μ i).prod (dirac y)) fun (i : ℕ) ↦
    map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i)
have e_f : ∀ (i : ℕ), Eq (α := Measure (α × β)) ((sfiniteSeq μ i).prod (dirac y)) (map (fun (x : α) ↦ (x, y)) (sfiniteSeq μ i))
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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))
have 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∞)
Tactic: refine prod_eq fun s t hs ht => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ (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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ (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∞)
have 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∞)
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]