awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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)) (β := U × V)
    (⇑(volumePreservingSymmMeasurableEquivToLpProdAux U V) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))
have refine : MeasurePreserving (α := WithLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)) (β := U × V)
  (⇑(MeasurableEquiv.trans
        (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)))
        (MeasurableEquiv.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ 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 : WithLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)) → U × V)
  volume (volume : Measure (U × V))
Tactic: refine (LinearIsometryEquiv.measurePreserving _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)) (β := U × V)
    (⇑(MeasurableEquiv.trans
          (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)))
          (MeasurableEquiv.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ 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 : WithLp 2 ((i : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V)) → ℝ)) → U × V)
    volume (volume : Measure (U × V))
have refine : MeasurePreserving (α := Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) (β := U × V)
  (⇑(MeasurableEquiv.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ 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 : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) → U × V)
  volume (volume : Measure (U × V))
Tactic: refine (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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 (α := Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) (β := U × V)
    (⇑(MeasurableEquiv.trans (MeasurableEquiv.sumPiEquivProdPi fun (x : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ 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 : Fin (finrank ℝ U) ⊕ Fin (finrank ℝ V) → ℝ) → U × V)
    volume (volume : Measure (U × V))
have refine : 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_sumPiEquivProdPi _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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)) → ℝ) × ((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))
have 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
Tactic: refine MeasurePreserving.prod ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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
⊢ 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))
have 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
Tactic: refine MeasurePreserving.prod ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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
have 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
Tactic: refine (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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
have 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
Tactic: refine (EuclideanSpace.volume_preserving_symm_measurableEquiv_toLp _).symm.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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) ⊤
have rw : ∀ (v_1 : E), ∃ (r : ℝ), r • ‖v‖⁻¹ • v = v_1
Tactic: rw [Submodule.span_singleton_eq_top_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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_1 : E), ∃ (r : ℝ), r • ‖v‖⁻¹ • v = v_1
have apply : ‖v‖⁻¹ • v ≠ 0
Tactic: apply exists_smul_eq_of_finrank_eq_one h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (hypothesis)
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.{u_2 + 1} (α := Measure E) volume (map (fun (x : ℝ) ↦ x • v) (map (fun (x : ℝ) ↦ ‖v‖⁻¹ • x) volume))
have hv' : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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.{u_2 + 1} (α := Measure E) volume (map (fun (x : ℝ) ↦ x • v) (map (fun (x : ℝ) ↦ ‖v‖⁻¹ • x) volume))
have rw : Eq.{u_2 + 1} (α := Measure E) volume (map (α := ℝ) ((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) volume)
Tactic: rw [map_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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.{u_2 + 1} (α := Measure E) volume (map (α := ℝ) ((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) volume)
have h₁ : Eq (α := ℝ → E) ((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) (⇑f : (a : ℝ) → E)
Tactic: convert! f.measurePreserving.map_eq.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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 (α := ℝ → E) ((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) (⇑f : (a : ℝ) → E)
have h₁ : ∀ (x : ℝ), Eq (α := E) (((fun (x : ℝ) ↦ x • v) ∘ fun (x : ℝ) ↦ ‖v‖⁻¹ • x) x : E) ((f : (a : ℝ) → E) x : E)
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
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) (map (fun (x : ℝ) ↦ ‖v‖⁻¹ • x) volume) =
    HSMul.hSMul (β := Measure E) ‖v‖ₑ (map (fun (x : ℝ) ↦ x • v) volume)
have 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)
Tactic: rw [map_addHaar_smul _ (by simpa using hv)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (hypothesis)
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
⊢ mulEquivHaarChar φ = μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
have smul : haar = haarScalarFactor haar μ • μ
Tactic: have smul := isMulLeftInvariant_eq_smul_of_regular haar μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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 μ • μ
| haar
have rw : haarScalarFactor haar μ • μ
Tactic: rw [smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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 μ • μ
| haarScalarFactor (G := G) haar (map (α := G) (⇑φ : (a : G) → G) haar) = μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
have enter : haarScalarFactor haar μ • μ
Tactic: enter [1, 1]
    rw [smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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 μ • μ
⊢ haarScalarFactor (G := G) haar (map (α := G) (⇑φ : (a : G) → G) haar) = μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
have conv : (haarScalarFactor haar μ • μ).haarScalarFactor (map (α := G) (⇑φ : (a : G) → G) haar) =
  μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
Tactic: conv =>
    enter [1, 1]
    rw [smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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 μ • μ
| (haarScalarFactor haar μ • μ).haarScalarFactor (map (α := G) (⇑φ : (a : G) → G) haar) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
have enter : haarScalarFactor haar μ • μ
Tactic: enter [1, 2, 2]
    rw [smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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 μ • μ
⊢ (haarScalarFactor haar μ • μ).haarScalarFactor (map (α := G) (⇑φ : (a : G) → G) haar) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
have conv : (haarScalarFactor haar μ • μ).haarScalarFactor (map (⇑φ : (a : G) → G) (haarScalarFactor haar μ • μ)) =
  μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
Tactic: conv =>
    enter [1, 2, 2]
    rw [smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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 μ • μ
⊢ (haarScalarFactor haar μ • μ).haarScalarFactor (map (⇑φ : (a : G) → G) (haarScalarFactor haar μ • μ)) =
    μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
have simp_rw : (haarScalarFactor haar μ • μ).haarScalarFactor
    (HSMul.hSMul (β := Measure G) (haarScalarFactor haar μ) (map (⇑φ : (a : G) → G) μ)) =
  μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)
Tactic: simp_rw [MeasureTheory.Measure.map_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
⊢ HSMul.hSMul (β := Measure G) (mulEquivHaarChar φ) (map (⇑φ : (a : G) → G) μ) = μ
have rw : HSMul.hSMul (β := Measure G) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) (map (⇑φ : (a : G) → G) μ) = μ
Tactic: rw [mulEquivHaarChar_eq μ φ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (hypothesis)
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
⊢ HSMul.hSMul (β := Measure G) (μ.haarScalarFactor (map (⇑φ : (a : G) → G) μ)) (map (⇑φ : (a : G) → G) μ) = μ
have this : Regular (α := G) (map (⇑φ : (a : G) → G) μ)
Tactic: have : Regular (map φ μ) := Regular.map φ.toHomeomorph
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
⊢ mulEquivHaarChar φ • μ = comap (⇑φ : (a : G) → G) μ
have rw : mulEquivHaarChar φ • μ = map (⇑φ.symm : (a : G) → G) μ
Tactic: rw [show ⇑φ = ⇑e from rfl, ← e.map_symm, show ⇑e.symm = ⇑φ.symm from rfl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (hypothesis)
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
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
⊢ mulEquivHaarChar φ • μ = map (⇑φ.symm : (a : G) → G) μ
have this : Regular (α := G) (map (⇑φ.symm : (a : G) → G) μ)
Tactic: have : (map (φ.symm) μ).Regular := Regular.map φ.symm.toHomeomorph
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar (goal)
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
e : G ≃ᵐ G := φ.toHomeomorph.toMeasurableEquiv
this : Regular (α := G) (map (⇑φ.symm : (a : G) → G) μ)
⊢ mulEquivHaarChar φ • μ = map (⇑φ.symm : (a : G) → G) μ
have rw : mulEquivHaarChar φ • μ =
  HSMul.hSMul (β := Measure G) (mulEquivHaarChar φ)
    (map (Function.comp (β := G) (⇑φ : (a : G) → G) (⇑φ.symm : (a : G) → G)) μ)
Tactic: rw [← mulEquivHaarChar_smul_map (map φ.symm μ) φ, map_map]