awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
fg : f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : E) → ι → ℝ)
Cg : Continuous (X := ι → ℝ) (Y := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ)
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e.symm : (a : ι → ℝ) → E)
rw :
  map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
      (map (α := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
⊢ map
      (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
        (Function.comp (β := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (⇑e : (a : E) → ι → ℝ)))
      μ =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ

Tactic:
rw [← map_map Cesymm.measurable (Cg.comp Ce).measurable, ← map_map Cg.measurable Ce.measurable]

Premises used: Continuous.comp, Continuous.measurable, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
fg : f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : E) → ι → ℝ)
Cg : Continuous (X := ι → ℝ) (Y := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ)
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e.symm : (a : ι → ℝ) → E)
⊢ IsAddHaarMeasure (G := ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)

Tactic:
haveI : IsAddHaarMeasure (map e μ) := (e : E ≃+ (ι → ℝ)).isAddHaarMeasure_map μ Ce Cesymm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this_2 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
fg : f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : E) → ι → ℝ)
Cg : Continuous (X := ι → ℝ) (Y := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ)
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e.symm : (a : ι → ℝ) → E)
this : IsAddHaarMeasure (G := ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)
h : ∀ (x : E), Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) (⇑e : (a : E) → ι → ℝ) x = id x
⊢ Eq (α := E → E) (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) (⇑e : (a : E) → ι → ℝ)) id

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this_2 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
fg : f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : E) → ι → ℝ)
Cg : Continuous (X := ι → ℝ) (Y := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ)
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e.symm : (a : ι → ℝ) → E)
this : IsAddHaarMeasure (G := ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)
x : E
⊢ Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) (⇑e : (a : E) → ι → ℝ) x = id x

Tactic:
simp only [id, Function.comp_apply, LinearEquiv.symm_apply_apply]

Premises used: LinearEquiv.symm_apply_apply, id, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this_2 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
fg : f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : E) → ι → ℝ)
Cg : Continuous (X := ι → ℝ) (Y := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ)
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e.symm : (a : ι → ℝ) → E)
this : IsAddHaarMeasure (G := ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)
⊢ Eq (α := E → E) (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) (⇑e : (a : E) → ι → ℝ)) id

Tactic:
have ecomp : e.symm ∘ e = id := by
    ext x; simp only [id, Function.comp_apply, LinearEquiv.symm_apply_apply]
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
ι : Type := Fin (finrank ℝ E)
this_1 : FiniteDimensional ℝ (ι → ℝ)
this_2 : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : Ne (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) (0 : ℝ)
hg : g = (↑e : E →ₗ[ℝ] ι → ℝ) ∘ₗ f ∘ₗ (↑e.symm : (ι → ℝ) →ₗ[ℝ] E)
gdet : Eq (α := ℝ) ((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ)
fg : f = (↑e.symm : (ι → ℝ) →ₗ[ℝ] E) ∘ₗ g ∘ₗ (↑e : E →ₗ[ℝ] ι → ℝ)
Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : E) → ι → ℝ)
Cg : Continuous (X := ι → ℝ) (Y := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ)
Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e.symm : (a : ι → ℝ) → E)
this : IsAddHaarMeasure (G := ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)
ecomp : Eq (α := E → E) (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) (⇑e : (a : E) → ι → ℝ)) id
rw :
  map (⇑e.symm : (a : ι → ℝ) → E)
      (HSMul.hSMul (β := Measure (ι → ℝ)) (ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹|)
        (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
rw₁ :
  HSMul.hSMul (β := Measure E) (ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹|)
      (map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
rw₂ :
  HSMul.hSMul (β := Measure E) (ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹|)
      (map (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) (⇑e : (a : E) → ι → ℝ)) μ) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
rw₃ :
  HSMul.hSMul (β := Measure E) (ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹|) (map id μ) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
rw₄ rw₅ :
  ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
⊢ map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
      (map (α := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ

Tactic:
rw [map_linearMap_addHaar_pi_eq_smul_addHaar hf (map e μ), Measure.map_smul,
    map_map Cesymm.measurable Ce.measurable, ecomp, Measure.map_id]

Premises used: MeasureTheory.Measure.map_id, MeasureTheory.Measure.map_linearMap_addHaar_pi_eq_smul_addHaar, MeasureTheory.Measure.map, Continuous.measurable, MeasureTheory.Measure.map_smul, MeasureTheory.Measure.map_map, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
s : Set E
rw :
  (ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ((map (⇑f : (a : E) → E) μ : Measure E) : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]

Premises used: MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
s : Set E
⊢ (ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ : (a : Set E) → ℝ≥0∞) s =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →L[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E) : ℝ) (0 : ℝ)
s : Set E
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) ⁻¹' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E))⁻¹|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
addHaar_preimage_linearMap μ hf s

Premises used: MeasureTheory.Measure.addHaar_preimage_linearMap
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
⊢ Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E) : ℝ) (0 : ℝ)

Tactic:
have A : LinearMap.det (f : E →ₗ[ℝ] E) ≠ 0 := (LinearEquiv.isUnit_det' f).ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
A : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E) : ℝ) (0 : ℝ)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑(↑f : E →ₗ[ℝ] E) : (a : E) → E) ⁻¹' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E))⁻¹|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
addHaar_preimage_linearMap μ A s

Premises used: MeasureTheory.Measure.addHaar_preimage_linearMap
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
A : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E) : ℝ) (0 : ℝ)
h :
  Eq (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f.symm : E →ₗ[ℝ] E) : ℝ)
    (((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E))⁻¹ : ℝ)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) ⁻¹' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f.symm : E →ₗ[ℝ] E)|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
convert! addHaar_preimage_linearMap μ A s

Premises used: MeasureTheory.Measure.addHaar_preimage_linearMap
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E ≃ₗ[ℝ] E
s : Set E
A : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E) : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f.symm : E →ₗ[ℝ] E) : ℝ)
    (((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E))⁻¹ : ℝ)

Tactic:
simp only [LinearEquiv.det_coe_symm]

Premises used: LinearEquiv.det_coe_symm
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E ≃L[ℝ] E
s : Set E
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) ⁻¹' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑(↑f.symm : E ≃ₗ[ℝ] E) : E →ₗ[ℝ] E)|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
addHaar_preimage_linearEquiv μ _ s

Premises used: MeasureTheory.Measure.addHaar_preimage_linearEquiv
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
s : Set E
inl :
  ∀ (hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)),
    (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|)
        ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
inr :
  ∀ (hf : Eq (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)),
    (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
      HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|)
        ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases ne_or_eq (LinearMap.det f) 0 with (hf | hf)

Premises used: ne_or_eq, LinearMap.det, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
s : Set E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
g : E ≃L[ℝ] E := (f.equivOfDetNeZero hf).toContinuousLinearEquiv
inl :
  (μ : (a : Set E) → ℝ≥0∞) ((⇑g : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
change μ (g '' s) = _

Premises used: Set.image, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
s : Set E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
g : E ≃L[ℝ] E := (f.equivOfDetNeZero hf).toContinuousLinearEquiv
inl :
  HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑(↑g.symm.symm : E ≃ₗ[ℝ] E) : E →ₗ[ℝ] E)|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑g : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [ContinuousLinearEquiv.image_eq_preimage_symm g s, addHaar_preimage_continuousLinearEquiv]

Premises used: ContinuousLinearEquiv.image_eq_preimage_symm, MeasureTheory.Measure.addHaar_preimage_continuousLinearEquiv
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
s : Set E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
g : E ≃L[ℝ] E := (f.equivOfDetNeZero hf).toContinuousLinearEquiv
⊢ HMul.hMul (β := ℝ≥0∞)
      (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑(↑g.symm.symm : E ≃ₗ[ℝ] E) : E →ₗ[ℝ] E)|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
s : Set E
hf : Eq (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f|) ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simpa [hf] using (measure_mono (image_subset_range _ _)).trans_eq <|
      addHaar_submodule μ _ (LinearMap.range_lt_top_of_det_eq_zero hf).ne

Premises used: LE.le.trans_eq, Set.image_subset_range, MeasureTheory.Measure.addHaar_submodule, MeasureTheory.measure_mono, LT.lt.ne, LinearMap.range_lt_top_of_det_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →L[ℝ] E
s : Set E
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑f : E →ₗ[ℝ] E)|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
addHaar_image_linearMap μ _ s

Premises used: MeasureTheory.Measure.addHaar_image_linearMap
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E ≃L[ℝ] E
s : Set E
⊢ (μ : (a : Set E) → ℝ≥0∞) ((⇑f : (a : E) → E) '' s) =
    HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal |(LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑(↑f : E ≃ₗ[ℝ] E) : E →ₗ[ℝ] E)|)
      ((μ : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
μ.addHaar_image_linearMap (f : E →ₗ[ℝ] E) s

Premises used: ContinuousLinearEquiv.toLinearEquiv, MeasureTheory.Measure.addHaar_image_linearMap, LinearEquiv.toLinearMap
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
⊢ QuasiMeasurePreserving (⇑f : (a : E) → E) μ μ

Tactic:
⟨f.continuous_of_finiteDimensional.measurable, ?_⟩

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.mk, LinearMap.continuous_of_finiteDimensional, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
refine : map (⇑f : (a : E) → E) μ ≪ μ
⊢ QuasiMeasurePreserving (⇑f : (a : E) → E) μ μ

Tactic:
refine ⟨f.continuous_of_finiteDimensional.measurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
rw : ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ ≪ μ
⊢ map (⇑f : (a : E) → E) μ ≪ μ

Tactic:
rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]

Premises used: MeasureTheory.Measure.map_linearMap_addHaar_eq_smul_addHaar
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
⊢ ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ ≪ μ

Tactic:
smul_absolutelyContinuous

Premises used: MeasureTheory.Measure.smul_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : Ne (α := ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f : ℝ) (0 : ℝ)
⊢ ENNReal.ofReal |((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) f)⁻¹| • μ ≪ μ

Tactic:
exact smul_absolutelyContinuous

Premises used: MeasureTheory.Measure.smul_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
f : E →L[ℝ] E
hf : f.det ≠ 0
⊢ QuasiMeasurePreserving (⇑f : (a : E) → E) μ μ

Tactic:
LinearMap.quasiMeasurePreserving μ (f : E →ₗ[ℝ] E) hf

Premises used: ContinuousLinearMap.toLinearMap, MeasureTheory.Measure.LinearMap.quasiMeasurePreserving