-- Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
theorem measurePreserving (f : E ≃ₗᵢ[ℝ] F) :
    MeasurePreserving f

Proof state:
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
⊢ map (⇑f) volume = volume

Tactic:
rcases exists_orthonormalBasis ℝ E with ⟨w, b, _hw⟩

Result:
case intro.intro
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis { x // x ∈ w } ℝ E
_hw : ⇑b = Subtype.val
⊢ map (⇑f) volume = volume

Proof state:
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
⊢ MeasurePreserving (⇑f) volume volume

Tactic:
refine ⟨f.continuous.measurable, ?_⟩

Result:
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
⊢ map (⇑f) volume = volume

Proof state:
case intro.intro
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis { x // x ∈ w } ℝ E
_hw : ⇑b = Subtype.val
⊢ (b.toBasis.map f.toContinuousLinearEquiv.toLinearEquiv).addHaar = (b.map f).toBasis.addHaar

Tactic:
congr

Result:
no goals

Proof state:
case intro.intro
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis { x // x ∈ w } ℝ E
_hw : ⇑b = Subtype.val
⊢ map (⇑f) volume = volume

Tactic:
erw [← OrthonormalBasis.addHaar_eq_volume b, ← OrthonormalBasis.addHaar_eq_volume (b.map f),
  Basis.map_addHaar _ f.toContinuousLinearEquiv]

Result:
case intro.intro
E : Type u_2
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : InnerProductSpace ℝ F
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis { x // x ∈ w } ℝ E
_hw : ⇑b = Subtype.val
⊢ (b.toBasis.map f.toContinuousLinearEquiv.toLinearEquiv).addHaar = (b.map f).toBasis.addHaar