∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)] {a b : ℕ} (h : a = b)
  (μ : (n : ℕ) → MeasureTheory.Measure ((i : ↥(Finset.Iic n)) → X ↑i)), MeasureTheory.Measure.map (cast ⋯) (μ a) = μ b