-- 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 : 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∞)
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∞)
e_f₅ :
  (((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₆ :
  HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq μ i.1.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        ((sfiniteSeq ν i.1.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞))
      ((sfiniteSeq τ i.2 : (a : Set γ) → ℝ≥0∞) u : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i.1.1 : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((sfiniteSeq ν i.1.2 : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
        ((sfiniteSeq τ i.2 : (a : Set γ) → ℝ≥0∞) 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:
simp_rw [map_apply (MeasurableEquiv.measurable _) (hs.prod (ht.prod hu)),
    MeasurableEquiv.prodAssoc, MeasurableEquiv.coe_mk, Equiv.prod_assoc_preimage, prod_prod,
    mul_assoc]

Premises used: MeasureTheory.Measure.map_apply, mul_assoc, MeasurableEquiv.coe_mk, MeasurableSet.prod, MeasureTheory.Measure.prod_prod, MeasurableEquiv.prodAssoc, Equiv.prod_assoc_preimage, MeasurableEquiv.measurable