-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem Basis.map_addHaar {ι E F : Type*} [Fintype ι] [NormedAddCommGroup E] [NormedAddCommGroup F]
    [NormedSpace ℝ E] [NormedSpace ℝ F] [MeasurableSpace E] [MeasurableSpace F] [BorelSpace E]
    [BorelSpace F] [SecondCountableTopology F] [SigmaCompactSpace F]
    (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) :
    map f b.addHaar = (b.map f.toLinearEquiv).addHaar

Proof state:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
this : (Measure.map (⇑f) b.addHaar).IsAddHaarMeasure
⊢ b.addHaar (⇑f ⁻¹' _root_.parallelepiped (⇑f.toLinearEquiv ∘ ⇑b)) = 1

Tactic:
erw [← image_parallelepiped, f.toEquiv.preimage_image, addHaar_self]

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
⊢ Measure.map (⇑f) b.addHaar = (b.map f.toLinearEquiv).addHaar

Tactic:
have : IsAddHaarMeasure (map f b.addHaar) :=
  AddEquiv.isAddHaarMeasure_map b.addHaar f.toAddEquiv f.continuous f.symm.continuous

Result:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
this : (Measure.map (⇑f) b.addHaar).IsAddHaarMeasure
⊢ Measure.map (⇑f) b.addHaar = (b.map f.toLinearEquiv).addHaar

Proof state:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
this : (Measure.map (⇑f) b.addHaar).IsAddHaarMeasure
⊢ Measure.map (⇑f) b.addHaar = (b.map f.toLinearEquiv).addHaar

Tactic:
rw [eq_comm, Basis.addHaar_eq_iff, Measure.map_apply f.continuous.measurable
  (PositiveCompacts.isCompact _).measurableSet, Basis.coe_parallelepiped, Basis.coe_map]

Result:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace E
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace E
inst✝² : BorelSpace F
inst✝¹ : SecondCountableTopology F
inst✝ : SigmaCompactSpace F
b : Basis ι ℝ E
f : E ≃L[ℝ] F
this : (Measure.map (⇑f) b.addHaar).IsAddHaarMeasure
⊢ b.addHaar (⇑f ⁻¹' _root_.parallelepiped (⇑f.toLinearEquiv ∘ ⇑b)) = 1