Integral is Dimensionally Correct

lemma integral_isDimensionallyCorrect (d : Dimension LTMCTDimensionBase) :    IsDimensionallyCorrect (fun (μ : DimSet (MeasureTheory.Measure M) d)      (f : DimSet (M → G) (dim G * d⁻¹)) ↦ ∫ x, f.1 x ∂μ.1) := by  intro u1 u2  funext ⟨μ, hμ⟩ ⟨f, hf⟩  /- We have to prove that    `scaleUnit u1 (fun μ f ↦ ∫ x, f x ∂μ) u2 ⟨μ, hμ⟩ ⟨f, hf⟩ = ∫ x, f x ∂μ` -/  calc _    /- By definition the LHS is equal to    `scaleUnit u1 u2 (∫ x, (scaleUnit u2 u1 f) x ∂(scaleUnit u2 u1 μ)) `    The statement says, suppose `f` and `μ` are in units `u2`, we change them to units `u1`,    then do the integral, and then we take the result back to `u2`.    If the integral is dimensionally correct, this should be the same as just doing the    original integral in `u2` units i.e. `∫ x, f x ∂μ`. -/    _ = scaleUnit u1 u2 (∫ x, (scaleUnit u2 u1 f) x ∂(scaleUnit u2 u1 μ)) := by      simp    /- Since we have assumed `μ` has dimension `d`, `(scaleUnit u2 μ u1)`      is equal to `(u2.dimScale u1 d) • μ` -/    _ = scaleUnit u1 u2 (u2.dimScale u1 d • ∫ (x : M), scaleUnit u2 u1 f x ∂ μ) := by      rw [hμ, integral_smul_nnreal_measure]    /- Since we assumed `f` has dimension `CarriesDimension.d G * d⁻¹`, `(scaleUnit u2 f u1)`      is equal to `u2.dimScale u1 (CarriesDimension.d G * d⁻¹) • f`. -/    _ = scaleUnit u1 u2 (u2.dimScale u1 d •      u2.dimScale u1 (dim G * d⁻¹) • ∫ (x : M), f x ∂ μ) := by      rw [hf]      congr      erw [MeasureTheory.integral_smul]      rfl    /- What remains is a simple cancellation of the dimensional scales. -/    _ = (u1.dimScale u2 (dim G)) • ((u2.dimScale u1 d) •        u2.dimScale u1 (dim G * d⁻¹) • ∫ (x : M), f x ∂ μ) := by      rw [← HasDim.scaleUnit_apply]    _ = (u1.dimScale u2 (dim G) * (u2.dimScale u1 d) *        u2.dimScale u1 (dim G * d⁻¹)) • ∫ (x : M), f x ∂ μ := by      simp [smul_smul]      ring_nf    _ = ((u1.dimScale u2 (dim G) * u2.dimScale u1 (dim G))        * (u2.dimScale u1 d * u1.dimScale u2 d)) • ∫ (x : M), f x ∂ μ := by      congr 1      conv_lhs => simp only [map_mul]      rw [UnitChoices.dimScale_of_inv_eq_swap]      ring    _ = ∫ (x : M), f x ∂ μ := by simp