-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Pi (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : Fintype ι
inst_1 : RCLike 𝕜
E : ι → Type u_3
f : (i : ι) → E i → 𝕜
mE : (i : ι) → MeasurableSpace (E i)
μ : (i : ι) → Measure (E i)
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
e : Fin (card ι) ≃ ι := Equiv.symm (equivFin ι)
simp_rw :
  Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
      (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
        μ ((e : (a : Fin (card ι)) → ι) i'))
      fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
      ∏ i : Fin (card ι),
        f ((e : (a : Fin (card ι)) → ι) i)
          ((MeasurableEquiv.piCongrLeft E e :
              (a : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) → (a : ι) → E a)
            x ((e : (a : Fin (card ι)) → ι) i)))
    (∏ i : Fin (card ι),
      ∫ (x : E ((e : (a : Fin (card ι)) → ι) i)),
        f ((e : (a : Fin (card ι)) → ι) i) x ∂μ ((e : (a : Fin (card ι)) → ι) i))
simp_rw₁ :
  Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
      (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
        μ ((e : (a : Fin (card ι)) → ι) i'))
      fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
      ∏ x_1 : Fin (card ι),
        f ((e : (a : Fin (card ι)) → ι) x_1)
          ((Equiv.piCongrLeft E e : (a : (a : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) a)) → (b : ι) → E b) x
            ((e : (a : Fin (card ι)) → ι) x_1)))
    (∏ i : Fin (card ι),
      ∫ (x : E ((e : (a : Fin (card ι)) → ι) i)),
        f ((e : (a : Fin (card ι)) → ι) i) x ∂μ ((e : (a : Fin (card ι)) → ι) i))
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
      (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
        μ ((e : (a : Fin (card ι)) → ι) i'))
      fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
      ∏ i : ι,
        f i
          ((MeasurableEquiv.piCongrLeft E e :
              (a : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) → (a : ι) → E a)
            x i))
    (∏ i : ι, ∫ (x : E i), f i x ∂μ i)
have simp_rw₂ : Eq.{u_1 + 1} (α := 𝕜)
  (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)))
    (Measure.pi (α := fun (b : Fin (card ι)) ↦ E ((e : (a : Fin (card ι)) → ι) b)) fun (i' : Fin (card ι)) ↦
      μ ((e : (a : Fin (card ι)) → ι) i'))
    fun (x : (b : Fin (card ι)) → E ((e : (a : Fin (card ι)) → ι) b)) ↦
    ∏ x_1 : Fin (card ι), f ((e : (a : Fin (card ι)) → ι) x_1) (x x_1))
  (∏ i : Fin (card ι),
    ∫ (x : E ((e : (a : Fin (card ι)) → ι) i)),
      f ((e : (a : Fin (card ι)) → ι) i) x ∂μ ((e : (a : Fin (card ι)) → ι) i))
Tactic: simp_rw [← e.prod_comp, MeasurableEquiv.coe_piCongrLeft, Equiv.piCongrLeft_apply_apply,
    MeasureTheory.integral_fin_nat_prod_eq_prod]