case inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f ≠ 0
⊢ ↑↑μ (↑f '' s) = ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s

case inr
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f = 0
⊢ ↑↑μ (↑f '' s) = ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
⊢ ↑↑μ (↑f '' s) = ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s
rcases ne_or_eq (LinearMap.det f) 0 with (hf | hf)
case inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f ≠ 0
g : E ≃L[ℝ] E := LinearEquiv.toContinuousLinearEquiv (LinearMap.equivOfDetNeZero f hf)
⊢ ↑↑μ (↑f '' s) = ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s
case inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f ≠ 0
⊢ ↑↑μ (↑f '' s) = ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s
let g := (f.equivOfDetNeZero hf).toContinuousLinearEquiv
case inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f ≠ 0
g : E ≃L[ℝ] E := LinearEquiv.toContinuousLinearEquiv (LinearMap.equivOfDetNeZero f hf)
⊢ ↑↑μ (↑g '' s) = ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s
case inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f ≠ 0
g : E ≃L[ℝ] E := LinearEquiv.toContinuousLinearEquiv (LinearMap.equivOfDetNeZero f hf)
⊢ ↑↑μ (↑f '' s) = ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s
change μ (g '' s) = _
case inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f ≠ 0
g : E ≃L[ℝ] E := LinearEquiv.toContinuousLinearEquiv (LinearMap.equivOfDetNeZero f hf)
⊢ ENNReal.ofReal (abs (↑LinearMap.det ↑↑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.symm g)))) * ↑↑μ s =
    ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s
case inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f ≠ 0
g : E ≃L[ℝ] E := LinearEquiv.toContinuousLinearEquiv (LinearMap.equivOfDetNeZero f hf)
⊢ ↑↑μ (↑g '' s) = ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s
rw [ContinuousLinearEquiv.image_eq_preimage g s, add_haar_preimage_continuousLinearEquiv]
no goals
case inl
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f ≠ 0
g : E ≃L[ℝ] E := LinearEquiv.toContinuousLinearEquiv (LinearMap.equivOfDetNeZero f hf)
⊢ ENNReal.ofReal (abs (↑LinearMap.det ↑↑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.symm g)))) * ↑↑μ s =
    ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s
congr
case inr
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f = 0
⊢ ↑↑μ ((fun a => ↑f a) '' s) = 0
case inr
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f = 0
⊢ ↑↑μ (↑f '' s) = ENNReal.ofReal (abs (↑LinearMap.det f)) * ↑↑μ s
simp only [hf, zero_mul, ENNReal.ofReal_zero, abs_zero]
case inr
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f = 0
this : ↑↑μ ↑(LinearMap.range f) = 0
⊢ ↑↑μ ((fun a => ↑f a) '' s) = 0
case inr
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f = 0
⊢ ↑↑μ ((fun a => ↑f a) '' s) = 0
have : μ (LinearMap.range f) = 0 :=
  add_haar_submodule μ _ (LinearMap.range_lt_top_of_det_eq_zero hf).ne
no goals
case inr
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
μ : Measure E
inst✝³ : IsAddHaarMeasure μ
F : Type ?u.1724957
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
s : Set E
hf : ↑LinearMap.det f = 0
this : ↑↑μ ↑(LinearMap.range f) = 0
⊢ ↑↑μ ((fun a => ↑f a) '' s) = 0
exact le_antisymm (le_trans (measure_mono (image_subset_range _ _)) this.le) (zero_le _)