awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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 →ₗ[ℝ] ι → ℝ)
⊢ map (⇑f : (a : E) → E) μ = ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have simp : map
    (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
      (Function.comp (β := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (⇑e : (a : E) → ι → ℝ)))
    μ =
  ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
Tactic: simp only [fg, LinearEquiv.coe_coe, LinearMap.coe_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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 →ₗ[ℝ] ι → ℝ)
⊢ map
      (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
        (Function.comp (β := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (⇑e : (a : E) → ι → ℝ)))
      μ =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have Ce : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (⇑e : (a : E) → ι → ℝ)
Tactic: have Ce : Continuous e := (e : E →ₗ[ℝ] ι → ℝ).continuous_of_finiteDimensional
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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) → ι → ℝ)
⊢ map
      (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
        (Function.comp (β := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (⇑e : (a : E) → ι → ℝ)))
      μ =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have Cg : Continuous (X := ι → ℝ) (Y := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ)
Tactic: have Cg : Continuous g := LinearMap.continuous_of_finiteDimensional g
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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 : ι → ℝ) → ι → ℝ)
⊢ map
      (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
        (Function.comp (β := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (⇑e : (a : E) → ι → ℝ)))
      μ =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have Cesymm : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e.symm : (a : ι → ℝ) → E)
Tactic: have Cesymm : Continuous e.symm := (e.symm : (ι → ℝ) →ₗ[ℝ] E).continuous_of_finiteDimensional
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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)
⊢ map
      (Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
        (Function.comp (β := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (⇑e : (a : E) → ι → ℝ)))
      μ =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have rw : map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
    (map (α := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (map (⇑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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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)
⊢ map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
      (map (α := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have this₁ : IsAddHaarMeasure (G := ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)
Tactic: haveI : IsAddHaarMeasure (map e μ) := (e : E ≃+ (ι → ℝ)).isAddHaarMeasure_map μ Ce Cesymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
have h : ∀ (x : E), Function.comp (β := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E) (⇑e : (a : E) → ι → ℝ) x = id x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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) → ι → ℝ) μ)
⊢ map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
      (map (α := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have ecomp : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
⊢ map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
      (map (α := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have 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)⁻¹| • μ
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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)⁻¹| • μ
⊢ map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
      (map (α := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have 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)⁻¹| • μ
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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)⁻¹| • μ
⊢ map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
      (map (α := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have 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)⁻¹| • μ
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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)⁻¹| • μ
⊢ map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
      (map (α := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have rw₃ : HSMul.hSMul (β := Measure E) (ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹|) (map id μ) =
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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)⁻¹| • μ
⊢ map (α := ι → ℝ) (⇑e.symm : (a : ι → ℝ) → E)
      (map (α := ι → ℝ) (⇑g : (a : ι → ℝ) → ι → ℝ) (map (⇑e : (a : E) → ι → ℝ) μ)) =
    ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ
have rw₄ : ENNReal.ofReal |((LinearMap.det : (a : (ι → ℝ) →ₗ[ℝ] ι → ℝ) → ℝ) g)⁻¹| • μ =
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (goal)
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
⊢ ((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∞)
have 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∞)
Tactic: rw [map_linearMap_addHaar_eq_smul_addHaar μ hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar (hypothesis)
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 : 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∞)
have A : 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