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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
let ι := Fin (finrank ℝ E)
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this : FiniteDimensional ℝ (ι → ℝ)
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
haveI : FiniteDimensional ℝ (ι → ℝ) := by infer_instance
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this : FiniteDimensional ℝ (ι → ℝ)
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
have : finrank ℝ E = finrank ℝ (ι → ℝ) := by simp
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
have e : E ≃ₗ[ℝ] ι → ℝ := LinearEquiv.ofFinrankEq E (ι → ℝ) this
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
obtain ⟨g, hg⟩ : ∃ g, g = (e : E →ₗ[ℝ] ι → ℝ).comp (f.comp (e.symm : (ι → ℝ) →ₗ[ℝ] E)) := ⟨_, rfl⟩
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
have gdet : LinearMap.det g = LinearMap.det f := by rw [hg]; exact LinearMap.det_conj f e
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det f)⁻¹) • μ
rw [← gdet] at hf ⊢
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
have fg : f = (e.symm : (ι → ℝ) →ₗ[ℝ] E).comp (g.comp (e : E →ₗ[ℝ] ι → ℝ)) := by
  ext x
  simp only [LinearEquiv.coe_coe, Function.comp_apply, LinearMap.coe_comp,
    LinearEquiv.symm_apply_apply, hg]
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
⊢ map (↑(LinearEquiv.symm e) ∘ ↑g ∘ ↑e) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
⊢ map (↑f) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
simp only [fg, LinearEquiv.coe_coe, LinearMap.coe_comp]
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
⊢ map (↑(LinearEquiv.symm e) ∘ ↑g ∘ ↑e) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
⊢ map (↑(LinearEquiv.symm e) ∘ ↑g ∘ ↑e) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
have Ce : Continuous e := (e : E →ₗ[ℝ] ι → ℝ).continuous_of_finiteDimensional
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
⊢ map (↑(LinearEquiv.symm e) ∘ ↑g ∘ ↑e) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
⊢ map (↑(LinearEquiv.symm e) ∘ ↑g ∘ ↑e) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
have Cg : Continuous g := LinearMap.continuous_of_finiteDimensional g
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
⊢ map (↑(LinearEquiv.symm e) ∘ ↑g ∘ ↑e) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
⊢ map (↑(LinearEquiv.symm e) ∘ ↑g ∘ ↑e) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
have Cesymm : Continuous e.symm := (e.symm : (ι → ℝ) →ₗ[ℝ] E).continuous_of_finiteDimensional
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
⊢ map (↑(LinearEquiv.symm e)) (map (↑g) (map (↑e) μ)) = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
⊢ map (↑(LinearEquiv.symm e) ∘ ↑g ∘ ↑e) μ = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
rw [← map_map Cesymm.measurable (Cg.comp Ce).measurable, ← map_map Cg.measurable Ce.measurable]
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
this : IsAddHaarMeasure (map (↑e) μ)
⊢ map (↑(LinearEquiv.symm e)) (map (↑g) (map (↑e) μ)) = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
⊢ map (↑(LinearEquiv.symm e)) (map (↑g) (map (↑e) μ)) = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
haveI : IsAddHaarMeasure (map e μ) := (e : E ≃+ (ι → ℝ)).isAddHaarMeasure_map μ Ce Cesymm
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
this : IsAddHaarMeasure (map (↑e) μ)
ecomp : ↑(LinearEquiv.symm e) ∘ ↑e = id
⊢ map (↑(LinearEquiv.symm e)) (map (↑g) (map (↑e) μ)) = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
this : IsAddHaarMeasure (map (↑e) μ)
⊢ map (↑(LinearEquiv.symm e)) (map (↑g) (map (↑e) μ)) = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
have ecomp : e.symm ∘ e = id := by
  ext x; simp only [id.def, Function.comp_apply, LinearEquiv.symm_apply_apply]
no goals
case intro
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
this : IsAddHaarMeasure (map (↑e) μ)
ecomp : ↑(LinearEquiv.symm e) ∘ ↑e = id
⊢ map (↑(LinearEquiv.symm e)) (map (↑g) (map (↑e) μ)) = ENNReal.ofReal (abs (↑LinearMap.det g)⁻¹) • μ
rw [map_linearMap_add_haar_pi_eq_smul_add_haar hf (map e μ), Measure.map_smul,
  map_map Cesymm.measurable Ce.measurable, ecomp, Measure.map_id]
no goals
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
⊢ FiniteDimensional ℝ (ι → ℝ)
infer_instance
no goals
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this : FiniteDimensional ℝ (ι → ℝ)
⊢ finrank ℝ E = finrank ℝ (ι → ℝ)
simp
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
⊢ ↑LinearMap.det (LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
⊢ ↑LinearMap.det g = ↑LinearMap.det f
rw [hg]
no goals
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
hf : ↑LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
⊢ ↑LinearMap.det (LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))) = ↑LinearMap.det f
exact LinearMap.det_conj f e
case h
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
x : E
⊢ ↑f x = ↑(LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)) x
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
⊢ f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
ext x
no goals
case h
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
x : E
⊢ ↑f x = ↑(LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)) x
simp only [LinearEquiv.coe_coe, Function.comp_apply, LinearMap.coe_comp,
  LinearEquiv.symm_apply_apply, hg]
case h
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
this : IsAddHaarMeasure (map (↑e) μ)
x : E
⊢ (↑(LinearEquiv.symm e) ∘ ↑e) x = id x
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
this : IsAddHaarMeasure (map (↑e) μ)
⊢ ↑(LinearEquiv.symm e) ∘ ↑e = id
ext x
no goals
case h
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.986679
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this✝¹ : FiniteDimensional ℝ (ι → ℝ)
this✝ : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : ↑LinearMap.det g ≠ 0
hg : g = LinearMap.comp (↑e) (LinearMap.comp f ↑(LinearEquiv.symm e))
gdet : ↑LinearMap.det g = ↑LinearMap.det f
fg : f = LinearMap.comp (↑(LinearEquiv.symm e)) (LinearMap.comp g ↑e)
Ce : Continuous ↑e
Cg : Continuous ↑g
Cesymm : Continuous ↑(LinearEquiv.symm e)
this : IsAddHaarMeasure (map (↑e) μ)
x : E
⊢ (↑(LinearEquiv.symm e) ∘ ↑e) x = id x
simp only [id.def, Function.comp_apply, LinearEquiv.symm_apply_apply]