-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Pi (goal)
Goal:
ι : Type u_1
ι' : Type u_2
inst : Fintype ι
inst_1 : Fintype ι'
X : ι ⊕ ι' → Type u_4
m : (i : ι ⊕ ι') → MeasurableSpace (X i)
μ : (i : ι ⊕ ι') → Measure (X i)
inst_2 : ∀ (i : ι ⊕ ι'), SigmaFinite (μ i)
s : (i : ι ⊕ ι') → Set (X i)
h : ∀ (i : ι ⊕ ι'), MeasurableSet (s i)
simp_rw :
  Eq (α := ℝ≥0∞)
    ((Measure.prod (Measure.pi (α := fun (i : ι) ↦ X (Sum.inl i)) fun (i : ι) ↦ μ (Sum.inl i))
            (Measure.pi (α := fun (i' : ι') ↦ X (Sum.inr i')) fun (i : ι') ↦ μ (Sum.inr i)) :
          (a : Set (((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))) → ℝ≥0∞)
        ((⇑(MeasurableEquiv.symm (MeasurableEquiv.sumPiEquivProdPi X)) :
            (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i) ⁻¹'
          Set.pi (α := X) univ s) :
      ℝ≥0∞)
    (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₁ :
  Eq (α := ℝ≥0∞)
    ((Measure.prod (Measure.pi (α := fun (i : ι) ↦ X (Sum.inl i)) fun (i : ι) ↦ μ (Sum.inl i))
            (Measure.pi (α := fun (i' : ι') ↦ X (Sum.inr i')) fun (i : ι') ↦ μ (Sum.inr i)) :
          (a : Set (((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))) → ℝ≥0∞)
        ((⇑(Equiv.sumPiEquivProdPi X).symm :
            (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i) ⁻¹'
          Set.pi (α := X) univ s) :
      ℝ≥0∞)
    (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₂ :
  Eq (α := ℝ≥0∞)
    ((Measure.prod (Measure.pi (α := fun (i : ι) ↦ X (Sum.inl i)) fun (i : ι) ↦ μ (Sum.inl i))
            (Measure.pi (α := fun (i' : ι') ↦ X (Sum.inr i')) fun (i : ι') ↦ μ (Sum.inr i)) :
          (a : Set (((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))) → ℝ≥0∞)
        (SProd.sprod (α := Set ((i : ι) → X (Sum.inl i))) (β := Set ((i : ι') → X (Sum.inr i)))
          (Set.pi (α := fun (i : ι) ↦ X (Sum.inl i)) univ fun (i : ι) ↦ s (Sum.inl i))
          (Set.pi (α := fun (i : ι') ↦ X (Sum.inr i)) univ fun (i : ι') ↦ s (Sum.inr i))) :
      ℝ≥0∞)
    (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
simp_rw₃ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((Measure.pi (α := fun (i : ι) ↦ X (Sum.inl i)) fun (i : ι) ↦ μ (Sum.inl i) :
            (a : Set ((i : ι) → X (Sum.inl i))) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι) ↦ X (Sum.inl i)) univ fun (i : ι) ↦ s (Sum.inl i)) :
        ℝ≥0∞)
      ((Measure.pi (α := fun (i' : ι') ↦ X (Sum.inr i')) fun (i : ι') ↦ μ (Sum.inr i) :
            (a : Set ((i' : ι') → X (Sum.inr i'))) → ℝ≥0∞)
          (Set.pi (α := fun (i : ι') ↦ X (Sum.inr i)) univ fun (i : ι') ↦ s (Sum.inr i)) :
        ℝ≥0∞) =
    ∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)
⊢ Eq (α := ℝ≥0∞)
    ((Measure.map (α := ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i')))
            (⇑(MeasurableEquiv.symm (MeasurableEquiv.sumPiEquivProdPi X)) :
              (a : ((i : ι) → X (Sum.inl i)) × ((i' : ι') → X (Sum.inr i'))) → (i : ι ⊕ ι') → X i)
            (Measure.prod (Measure.pi (α := fun (i : ι) ↦ X (Sum.inl i)) fun (i : ι) ↦ μ (Sum.inl i))
              (Measure.pi (α := fun (i' : ι') ↦ X (Sum.inr i')) fun (i : ι') ↦ μ (Sum.inr i))) :
          (a : Set ((i : ι ⊕ ι') → X i)) → ℝ≥0∞)
        (Set.pi (α := X) univ s) :
      ℝ≥0∞)
    (∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have simp_rw₄ : HMul.hMul (α := ℝ≥0∞)
    (∏ i : ι, ((μ (Sum.inl i) : Measure (X (Sum.inl i))) : (a : Set (X (Sum.inl i))) → ℝ≥0∞) (s (Sum.inl i)))
    (∏ i : ι', ((μ (Sum.inr i) : Measure (X (Sum.inr i))) : (a : Set (X (Sum.inr i))) → ℝ≥0∞) (s (Sum.inr i))) =
  ∏ i : ι ⊕ ι', (μ i : (a : Set (X i)) → ℝ≥0∞) (s i)
Tactic: simp_rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_sumPiEquivProdPi_symm,
      Equiv.sumPiEquivProdPi_symm_preimage_univ_pi, Measure.prod_prod, Measure.pi_pi,
      Fintype.prod_sum_type]