awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
refine_1 :
  MeasurePreserving (α := (i : Fin (finrank ℝ U)) → ℝ) (β := U)
    (⇑(MeasurableEquiv.toEquiv
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))) :
      (a : (i : Fin (finrank ℝ U)) → ℝ) → U)
    (Measure.pi (α := fun (i : Fin (finrank ℝ U)) ↦ ℝ) fun (i : Fin (finrank ℝ U)) ↦ volume) volume
refine_2 :
  MeasurePreserving (α := (i' : Fin (finrank ℝ V)) → ℝ) (β := V)
    (⇑(MeasurableEquiv.toEquiv
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))))) :
      (a : (i' : Fin (finrank ℝ V)) → ℝ) → V)
    (Measure.pi (α := fun (i' : Fin (finrank ℝ V)) ↦ ℝ) fun (i : Fin (finrank ℝ V)) ↦ volume) volume
⊢ MeasurePreserving (α := ((i : Fin (finrank ℝ U)) → ℝ) × ((i' : Fin (finrank ℝ V)) → ℝ)) (β := U × V)
    (⇑(MeasurableEquiv.prodCongr
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))))) :
      (a : ((i : Fin (finrank ℝ U)) → ℝ) × ((i' : Fin (finrank ℝ V)) → ℝ)) → U × V)
    (Measure.prod (Measure.pi (α := fun (i : Fin (finrank ℝ U)) ↦ ℝ) fun (i : Fin (finrank ℝ U)) ↦ volume)
      (Measure.pi (α := fun (i' : Fin (finrank ℝ V)) ↦ ℝ) fun (i : Fin (finrank ℝ V)) ↦ volume))
    (volume : Measure (U × V))

Tactic:
refine MeasurePreserving.prod ?_ ?_

Premises used: MeasureTheory.MeasurePreserving.prod
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := (i : Fin (finrank ℝ U)) → ℝ) (β := U)
    (⇑(MeasurableEquiv.toEquiv
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))) :
      (a : (i : Fin (finrank ℝ U)) → ℝ) → U)
    (Measure.pi (α := fun (i : Fin (finrank ℝ U)) ↦ ℝ) fun (i : Fin (finrank ℝ U)) ↦ volume) volume

Tactic:
(EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm.trans ?_

Premises used: WithLp.equiv, MeasureTheory.MeasurePreserving.symm, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, Equiv.symm, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
refine_1 :
  MeasurePreserving (α := WithLp 2 (Fin (finrank ℝ U) → ℝ)) (β := U)
    (⇑(LinearIsometryEquiv.toMeasurableEquiv
          (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))) :
      (a : WithLp 2 (Fin (finrank ℝ U) → ℝ)) → U)
    volume volume
⊢ MeasurePreserving (α := (i : Fin (finrank ℝ U)) → ℝ) (β := U)
    (⇑(MeasurableEquiv.toEquiv
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))))) :
      (a : (i : Fin (finrank ℝ U)) → ℝ) → U)
    (Measure.pi (α := fun (i : Fin (finrank ℝ U)) ↦ ℝ) fun (i : Fin (finrank ℝ U)) ↦ volume) volume

Tactic:
refine (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm.trans ?_

Premises used: MeasureTheory.MeasurePreserving.symm, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := WithLp 2 (Fin (finrank ℝ U) → ℝ)) (β := U)
    (⇑(LinearIsometryEquiv.toMeasurableEquiv
          (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))) :
      (a : WithLp 2 (Fin (finrank ℝ U) → ℝ)) → U)
    volume volume

Tactic:
(LinearIsometryEquiv.measurePreserving _)

Premises used: LinearIsometryEquiv.measurePreserving
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := WithLp 2 (Fin (finrank ℝ U) → ℝ)) (β := U)
    (⇑(LinearIsometryEquiv.toMeasurableEquiv
          (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ U)))) :
      (a : WithLp 2 (Fin (finrank ℝ U) → ℝ)) → U)
    volume volume

Tactic:
exact (LinearIsometryEquiv.measurePreserving _)

Premises used: LinearIsometryEquiv.measurePreserving
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := (i' : Fin (finrank ℝ V)) → ℝ) (β := V)
    (⇑(MeasurableEquiv.toEquiv
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))))) :
      (a : (i' : Fin (finrank ℝ V)) → ℝ) → V)
    (Measure.pi (α := fun (i' : Fin (finrank ℝ V)) ↦ ℝ) fun (i : Fin (finrank ℝ V)) ↦ volume) volume

Tactic:
(EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm.trans ?_

Premises used: WithLp.equiv, MeasureTheory.MeasurePreserving.symm, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, Equiv.symm, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
refine_2 :
  MeasurePreserving (α := WithLp 2 (Fin (finrank ℝ V) → ℝ)) (β := V)
    (⇑(LinearIsometryEquiv.toMeasurableEquiv
          (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))) :
      (a : WithLp 2 (Fin (finrank ℝ V) → ℝ)) → V)
    volume volume
⊢ MeasurePreserving (α := (i' : Fin (finrank ℝ V)) → ℝ) (β := V)
    (⇑(MeasurableEquiv.toEquiv
          (MeasurableEquiv.trans (MeasurableEquiv.toLp 2 ((i' : Fin (finrank ℝ V)) → ℝ))
            (LinearIsometryEquiv.toMeasurableEquiv
              (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))))) :
      (a : (i' : Fin (finrank ℝ V)) → ℝ) → V)
    (Measure.pi (α := fun (i' : Fin (finrank ℝ V)) ↦ ℝ) fun (i : Fin (finrank ℝ V)) ↦ volume) volume

Tactic:
refine (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm.trans ?_

Premises used: MeasureTheory.MeasurePreserving.symm, EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp, MeasureTheory.MeasurePreserving.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := WithLp 2 (Fin (finrank ℝ V) → ℝ)) (β := V)
    (⇑(LinearIsometryEquiv.toMeasurableEquiv
          (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))) :
      (a : WithLp 2 (Fin (finrank ℝ V) → ℝ)) → V)
    volume volume

Tactic:
(LinearIsometryEquiv.measurePreserving _)

Premises used: LinearIsometryEquiv.measurePreserving
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := WithLp 2 (Fin (finrank ℝ V) → ℝ)) (β := V)
    (⇑(LinearIsometryEquiv.toMeasurableEquiv
          (LinearIsometryEquiv.symm (OrthonormalBasis.repr (stdOrthonormalBasis ℝ V)))) :
      (a : WithLp 2 (Fin (finrank ℝ V) → ℝ)) → V)
    volume volume

Tactic:
exact (LinearIsometryEquiv.measurePreserving _)

Premises used: LinearIsometryEquiv.measurePreserving
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := WithLp 2 (U × V)) ofLp (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))

Tactic:
volume_preserving_symm_measurableEquiv_toLp_prod U V

Premises used: WithLp.volume_preserving_symm_measurableEquiv_toLp_prod
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
U : Type u_4
V : Type u_5
inst : NormedAddCommGroup U
inst_1 : InnerProductSpace ℝ U
inst_2 : MeasurableSpace U
inst_3 : BorelSpace U
inst_4 : FiniteDimensional ℝ U
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : MeasurableSpace V
inst_8 : BorelSpace V
inst_9 : FiniteDimensional ℝ V
⊢ MeasurePreserving (α := U × V) (β := WithLp 2 (U × V)) (toLp 2) (volume : Measure (U × V))
    (volume : Measure (WithLp 2 (U × V)))

Tactic:
(volume_preserving_symm_measurableEquiv_toLp_prod U V).symm

Premises used: MeasureTheory.MeasurePreserving.symm, WithLp.volume_preserving_symm_measurableEquiv_toLp_prod
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
rw : ∀ (v_1 : E), ∃ (r : ℝ), r • ‖v‖⁻¹ • v = v_1
⊢ Eq (α := Submodule ℝ E) (ℝ ∙ ‖v‖⁻¹ • v) ⊤

Tactic:
rw [Submodule.span_singleton_eq_top_iff]

Premises used: Submodule.span_singleton_eq_top_iff
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
apply : ‖v‖⁻¹ • v ≠ 0
⊢ ∀ (v_1 : E), ∃ (r : ℝ), r • ‖v‖⁻¹ • v = v_1

Tactic:
apply exists_smul_eq_of_finrank_eq_one h

Premises used: exists_smul_eq_of_finrank_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
⊢ ‖v‖⁻¹ • v ≠ 0

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
⊢ Eq (α := Submodule ℝ E) (ℝ ∙ ‖v‖⁻¹ • v) ⊤

Tactic:
have hv' : Submodule.span ℝ {‖v‖⁻¹ • v} = ⊤ := by
      rw [Submodule.span_singleton_eq_top_iff]
      apply exists_smul_eq_of_finrank_eq_one h
      simpa
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : Eq (α := Submodule ℝ E) (ℝ ∙ ‖v‖⁻¹ • v) ⊤
⊢ ‖‖v‖⁻¹ • v‖ = 1

Tactic:
simp [norm_smul, hv]

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : Eq (α := Submodule ℝ E) (ℝ ∙ ‖v‖⁻¹ • v) ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  LinearIsometryEquiv.trans (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯)
    (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
⊢ Measurable.{0, u_2} (β := E) fun (x : ℝ) ↦ x • v

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : Eq (α := Submodule ℝ E) (ℝ ∙ ‖v‖⁻¹ • v) ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  LinearIsometryEquiv.trans (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯)
    (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ ‖v‖⁻¹ • x

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : Eq (α := Submodule ℝ E) (ℝ ∙ ‖v‖⁻¹ • v) ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  LinearIsometryEquiv.trans (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯)
    (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
rw : Eq.{u_2 + 1} (α := Measure E) volume (map (α := ℝ) ((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) volume)
⊢ Eq.{u_2 + 1} (α := Measure E) volume (map (fun (x : ℝ) ↦ x • v) (map (fun (x : ℝ) ↦ ‖v‖⁻¹ • x) volume))

Tactic:
rw [map_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : Eq (α := Submodule ℝ E) (ℝ ∙ ‖v‖⁻¹ • v) ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  LinearIsometryEquiv.trans (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯)
    (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
⊢ Eq (α := Measure E) (volume : Measure E) (map (α := ℝ) (⇑f : (a : ℝ) → E) volume)

Tactic:
f.measurePreserving.map_eq.symm

Premises used: LinearIsometryEquiv.measurePreserving, MeasureTheory.MeasurePreserving.map_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : Eq (α := Submodule ℝ E) (ℝ ∙ ‖v‖⁻¹ • v) ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  LinearIsometryEquiv.trans (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯)
    (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
h₁ : Eq (α := ℝ → E) ((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) (⇑f : (a : ℝ) → E)
⊢ Eq.{u_2 + 1} (α := Measure E) volume (map (α := ℝ) ((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) volume)

Tactic:
convert! f.measurePreserving.map_eq.symm

Premises used: LinearIsometryEquiv.measurePreserving, MeasureTheory.MeasurePreserving.map_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : Eq (α := Submodule ℝ E) (ℝ ∙ ‖v‖⁻¹ • v) ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  LinearIsometryEquiv.trans (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯)
    (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
h₁ : ∀ (x : ℝ), Eq (α := E) (((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) x : E) ((f : (a : ℝ) → E) x : E)
⊢ Eq (α := ℝ → E) ((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) (⇑f : (a : ℝ) → E)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : Eq (α := Submodule ℝ E) (ℝ ∙ ‖v‖⁻¹ • v) ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  LinearIsometryEquiv.trans (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯)
    (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
x : ℝ
⊢ Eq (α := E) (((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) x : E) ((f : (a : ℝ) → E) x : E)

Tactic:
simp [f, mul_comm, smul_smul]

Premises used: smul_smul, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
⊢ ‖v‖⁻¹ ≠ 0

Tactic:
simpa using hv
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
rw :
  map (fun (x : ℝ) ↦ x • v) (HSMul.hSMul (β := Measure ℝ) (ENNReal.ofReal |(‖v‖⁻¹ ^ finrank ℝ ℝ)⁻¹|) volume) =
    HSMul.hSMul (β := Measure E) ‖v‖ₑ (map (fun (x : ℝ) ↦ x • v) volume)
⊢ map (fun (x : ℝ) ↦ x • v) (map (fun (x : ℝ) ↦ ‖v‖⁻¹ • x) volume) =
    HSMul.hSMul (β := Measure E) ‖v‖ₑ (map (fun (x : ℝ) ↦ x • v) volume)

Tactic:
rw [map_addHaar_smul _ (by simpa using hv)]

Premises used: MeasureTheory.Measure.map_addHaar_smul
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
⊢ map (fun (x : ℝ) ↦ x • v) (HSMul.hSMul (β := Measure ℝ) (ENNReal.ofReal |(‖v‖⁻¹ ^ finrank ℝ ℝ)⁻¹|) volume) =
    HSMul.hSMul (β := Measure E) ‖v‖ₑ (map (fun (x : ℝ) ↦ x • v) volume)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
φ : G ≃ₜ* G
⊢ 0 < mulEquivHaarChar φ

Tactic:
haarScalarFactor_pos_of_isHaarMeasure _ _

Premises used: MeasureTheory.Measure.haarScalarFactor_pos_of_isHaarMeasure, MeasureTheory.mulEquivHaarChar
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
⊢ haar = haarScalarFactor haar μ • μ

Tactic:
have smul := isMulLeftInvariant_eq_smul_of_regular haar μ
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
smul : haar = haarScalarFactor haar μ • μ
enter : haar
| haarScalarFactor (G := G) haar (map (α := G) (⇑φ : (a : G) → G) haar) = μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)

Tactic:
enter [1, 1]
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
smul : haar = haarScalarFactor haar μ • μ
rw : haarScalarFactor haar μ • μ
| haar

Tactic:
rw [smul]
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
smul : haar = haarScalarFactor haar μ • μ
enter : haarScalarFactor haar μ • μ
| haarScalarFactor (G := G) haar (map (α := G) (⇑φ : (a : G) → G) haar) = μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)

Tactic:
enter [1, 1]
    rw [smul]
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
smul : haar = haarScalarFactor haar μ • μ
conv :
  (haarScalarFactor haar μ • μ).haarScalarFactor (map (α := G) (⇑φ : (a : G) → G) haar) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
⊢ haarScalarFactor (G := G) haar (map (α := G) (⇑φ : (a : G) → G) haar) = μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)

Tactic:
conv =>
    enter [1, 1]
    rw [smul]
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
smul : haar = haarScalarFactor haar μ • μ
enter : haar
| (haarScalarFactor haar μ • μ).haarScalarFactor (map (α := G) (⇑φ : (a : G) → G) haar) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)

Tactic:
enter [1, 2, 2]
-- Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : MeasurableSpace G
inst_3 : BorelSpace G
inst_4 : IsTopologicalGroup G
inst_5 : LocallyCompactSpace G
μ : Measure G
inst_6 : μ.IsHaarMeasure
inst_7 : μ.Regular
φ : G ≃ₜ* G
smul : haar = haarScalarFactor haar μ • μ
enter : haarScalarFactor haar μ • μ
| (haarScalarFactor haar μ • μ).haarScalarFactor (map (α := G) (⇑φ : (a : G) → G) haar) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)

Tactic:
enter [1, 2, 2]
    rw [smul]