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 ν
inst_3 : SFinite μ
this :
  Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
i : ℕ × ℕ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have e_f : ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1) : (a : Set (α × β)) → ℝ≥0∞) (Prod.swap ⁻¹' s ×ˢ t) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [map_apply measurable_swap (hs.prod ht), preimage_swap_prod, prod_prod, mul_comm]
-- 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 μ
this :
  Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
i : ℕ × ℕ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1) : (a : Set (α × β)) → ℝ≥0∞) (Prod.swap ⁻¹' s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have e_f₁ : ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1) : (a : Set (α × β)) → ℝ≥0∞) (t ×ˢ s) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [map_apply measurable_swap (hs.prod ht), preimage_swap_prod, prod_prod, mul_comm]
-- 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 μ
this :
  Eq (α := Measure (β × α)) (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2)))
    (sum fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)))
i : ℕ × ℕ
s : Set β
t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
e_f :
  ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1) : (a : Set (α × β)) → ℝ≥0∞) (Prod.swap ⁻¹' s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
e_f₁ :
  ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1) : (a : Set (α × β)) → ℝ≥0∞) (t ×ˢ s) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1)) : (a : Set (β × α)) → ℝ≥0∞) (s ×ˢ t) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have e_f₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1 : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((sfiniteSeq μ i.2 : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp_rw [map_apply measurable_swap (hs.prod ht), preimage_swap_prod, prod_prod, mul_comm]
-- 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 (α × β)
hs : MeasurableSet s
⊢ (μ.prod ν : (a : Set (α × β)) → ℝ≥0∞) s = ∫⁻ (y : β), (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s) ∂ν
have rw : ∫⁻ (x : β), (μ : (a : Set α) → ℝ≥0∞) (Prod.mk x ⁻¹' Prod.swap ⁻¹' s) ∂ν =
  ∫⁻ (y : β), (μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (x, y)) ⁻¹' s) ∂ν
Tactic: rw [← prod_swap, map_apply measurable_swap hs, prod_apply (measurable_swap hs)]
-- 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 μ
p : α → β → Prop
h : MeasurableSet (α := α × β) {x : α × β | p x.1 x.2}
⊢ (∀ᵐ (x : α × β) ∂μ.prod ν, p x.1 x.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1
have rw : (∀ᵐ (x : β × α) ∂ν.prod μ, p x.swap.1 x.swap.2) ↔ ∀ᵐ (x : β × α) ∂ν.prod μ, p x.2 x.1
Tactic: rw [← prod_swap, ae_map_iff (by fun_prop) h]
-- 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 β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet s μ
have refine : NullMeasurableSet (t ×ˢ s) (ν.prod μ)
Tactic: refine .right_of_prod ?_ 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 β
h : NullMeasurableSet (s ×ˢ t) (μ.prod ν)
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (t ×ˢ s) (ν.prod μ)
have rw : NullMeasurableSet (Prod.swap ⁻¹' s ×ˢ t) (ν.prod μ)
Tactic: rw [← preimage_swap_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 β
inst_2 : SFinite ν
inst_3 : SFinite μ
s : Set α
t : Set β
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have inl : ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases eq_or_ne (μ s) 0 with hs | hs
-- 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 β
inl :
  ∀ (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
      NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
          Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : ∀ (hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases eq_or_ne (μ s) 0 with hs | hs
-- 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 β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : ∀ (ht : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases eq_or_ne (ν t) 0 with ht | 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 β
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
inr :
  ∀ (ht : Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
    NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
      NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
          Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
have inr₁ : ∀ (ht : Ne (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  NullMeasurableSet (s ×ˢ t) (μ.prod ν) ↔
    NullMeasurableSet s μ ∧ NullMeasurableSet t ν ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
        Eq (α := ℝ≥0∞) ((ν : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases eq_or_ne (ν t) 0 with ht | ht
-- 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 τ
⊢ 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)))
have h : ∀ (s : Set (α × β × γ)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)) :
          (a : Set (α × β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)) :
          (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
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((sum fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2)) :
          (a : Set (α × β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((sum fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2)) :
          (a : Set (α × β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  (∑' (c : (ℕ × ℕ) × ℕ),
    ((sfiniteSeq μ ((Equiv.prodAssoc ℕ ℕ ℕ : (a : (ℕ × ℕ) × ℕ) → ℕ × ℕ × ℕ) c).1).prod
          ((sfiniteSeq ν ((Equiv.prodAssoc ℕ ℕ ℕ : (a : (ℕ × ℕ) × ℕ) → ℕ × ℕ × ℕ) c).2.1).prod
            (sfiniteSeq τ ((Equiv.prodAssoc ℕ ℕ ℕ : (a : (ℕ × ℕ) × ℕ) → ℕ × ℕ × ℕ) c).2.2)) :
        (a : Set (α × β × γ)) → ℝ≥0∞)
      s)
  (∑' (i : (ℕ × ℕ) × ℕ),
    ((sfiniteSeq μ i.1.1).prod ((sfiniteSeq ν i.1.2).prod (sfiniteSeq τ i.2)) : (a : Set (α × β × γ)) → ℝ≥0∞) s)
Tactic: rw [sum_apply _ hs, sum_apply _ hs, ← (Equiv.prodAssoc _ _ _).tsum_eq]
-- 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 α
ν : Measure β
τ : Measure γ
inst_3 : SFinite ν
inst_4 : SFinite μ
inst_5 : SFinite τ
⊢ map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)
have 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)))
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]
-- 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)))
⊢ map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ((μ.prod ν).prod τ) = μ.prod (ν.prod τ)
have 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)))
Tactic: rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, ← sum_sfiniteSeq τ, prod_sum, prod_sum,
    map_sum MeasurableEquiv.prodAssoc.measurable.aemeasurable, prod_sum, prod_sum, this]
-- 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)))
⊢ 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)))
have 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))
Tactic: congr
-- 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)))
⊢ 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))
have 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))
Tactic: ext1 i
-- 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 : (ℕ × ℕ) × ℕ
⊢ 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))
have 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∞)
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
-- 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 : 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
⊢ (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 : ∀ (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∞)
Tactic: rw [mem_setOf_eq] at hs ht hu
Cleared hypotheses: hs, t, ht, u, hu
-- 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∞)
⊢ (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∞)
    ((⇑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∞)
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]