Matrix Transvection Struct measure Preserving

lemma Matrix.TransvectionStruct.measurePreserving [SecondCountableTopology F]    (t : Matrix.TransvectionStruct ι F) :    MeasurePreserving (⇑(Matrix.toLin' t.toMatrix)) addHaar addHaar := by  -- Step 1: replace `addHaar` by the product Haar measure `μ`.  --         By uniqueness of Haar measures, they differ by a scalar, and  --         measure-preservation is unaffected by scaling.  let μ := Measure.pi fun _ : ι => (addHaar : Measure F)  suffices MeasurePreserving (⇑(toLin' t.toMatrix)) μ μ by    rw [isAddLeftInvariant_eq_smul_of_regular addHaar μ]    apply MeasurePreserving.smul_measure this  -- Step 2: prove invariance for the product Haar `μ`.  --         This is the analogue of `Real.volume_preserving_transvectionStruct`.  have hc: Continuous (toLin' t.toMatrix) := LinearMap.continuous_on_pi (toLin' t.toMatrix)  have hm: Measurable (toLin' t.toMatrix) := hc.measurable  refine ⟨hm, ?_⟩  -- Step 3: reduce to checking the map preserves measure of rectangles.  refine (pi_eq fun s hs ↦ ?_).symm  have h2s : MeasurableSet (Set.univ.pi s) := MeasurableSet.univ_pi hs  simp_rw [← pi_pi, ← lintegral_indicator_one h2s]  rw [lintegral_map (measurable_one.indicator h2s) hm]   -- Step 4: reduce further to the one-dimensional marginal on coordinate i.  refine lintegral_eq_of_lmarginal_eq {t.i}    ((measurable_one.indicator h2s).comp hm)    (measurable_one.indicator h2s) ?_  simp_rw [lmarginal_singleton]  ext x  -- Step 5: explicit computation for a transvection.  -- On the j-th coordinate, the transvection acts as a translation,  -- and Haar measure is invariant under translations.  cases t with  | mk i j hij c =>    simp [transvection, single_mulVec, hij.symm, ← Function.update_add,          lintegral_add_right_eq_self            (fun xᵢ ↦ Set.indicator (Set.univ.pi s) 1 (Function.update x i xᵢ))]