no goals
ι : Type ?u.6010588
ι' : Type ?u.6010591
α✝ : ι → Type ?u.6010596
inst✝¹ : Fintype ι
m✝ : (i : ι) → OuterMeasure (α✝ i)
α : Type u
m : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ MeasurePreserving ↑MeasurableEquiv.finTwoArrow
simpa only [Matrix.vec_single_eq_const, Matrix.vecCons_const] using
  measurePreserving_finTwoArrow_vec μ μ