awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : Fintype ι
inst_5 : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
A :
  Eq (α := (a : ι) → F) (⇑b : (a : ι) → F)
    (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))
⊢ Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) :
      ENNReal)
    (1 : ENNReal)
have rw : Eq (α := ENNReal)
  (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
      (parallelepiped (ι := ι) (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))) :
    ENNReal)
  (1 : ENNReal)
Tactic: rw [A, parallelepiped_comp_equiv, AlternatingMap.measure_parallelepiped,
    o.abs_volumeForm_apply_of_orthonormal, ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : Fintype ι
inst_5 : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
A :
  Eq (α := (a : ι) → F) (⇑b : (a : ι) → F)
    (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))
rw :
  Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped (ι := ι)
          (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))) :
      ENNReal)
    (1 : ENNReal)
⊢ Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) :
      ENNReal)
    (1 : ENNReal)
have rw₁ : Eq (α := ENNReal)
  (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
      (parallelepiped (ι := Fin n) (⇑(b.reindex e) : (a : Fin n) → F)) :
    ENNReal)
  (1 : ENNReal)
Tactic: rw [A, parallelepiped_comp_equiv, AlternatingMap.measure_parallelepiped,
    o.abs_volumeForm_apply_of_orthonormal, ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : Fintype ι
inst_5 : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
A :
  Eq (α := (a : ι) → F) (⇑b : (a : ι) → F)
    (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))
rw :
  Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped (ι := ι)
          (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))) :
      ENNReal)
    (1 : ENNReal)
rw₁ :
  Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped (ι := Fin n) (⇑(b.reindex e) : (a : Fin n) → F)) :
      ENNReal)
    (1 : ENNReal)
⊢ Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) :
      ENNReal)
    (1 : ENNReal)
have rw₂ : ENNReal.ofReal |(o.volumeForm : (a : Fin n → F) → ℝ) (⇑(b.reindex e) : (a : Fin n) → F)| = 1
Tactic: rw [A, parallelepiped_comp_equiv, AlternatingMap.measure_parallelepiped,
    o.abs_volumeForm_apply_of_orthonormal, ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : Fintype ι
inst_5 : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
A :
  Eq (α := (a : ι) → F) (⇑b : (a : ι) → F)
    (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))
rw :
  Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped (ι := ι)
          (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))) :
      ENNReal)
    (1 : ENNReal)
rw₁ :
  Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped (ι := Fin n) (⇑(b.reindex e) : (a : Fin n) → F)) :
      ENNReal)
    (1 : ENNReal)
rw₂ : ENNReal.ofReal |(o.volumeForm : (a : Fin n → F) → ℝ) (⇑(b.reindex e) : (a : Fin n) → F)| = 1
⊢ Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) :
      ENNReal)
    (1 : ENNReal)
have rw₃ : ENNReal.ofReal 1 = 1
Tactic: rw [A, parallelepiped_comp_equiv, AlternatingMap.measure_parallelepiped,
    o.abs_volumeForm_apply_of_orthonormal, ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : Fintype ι
inst_5 : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
A :
  Eq (α := (a : ι) → F) (⇑b : (a : ι) → F)
    (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))
rw :
  Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped (ι := ι)
          (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))) :
      ENNReal)
    (1 : ENNReal)
rw₁ :
  Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped (ι := Fin n) (⇑(b.reindex e) : (a : Fin n) → F)) :
      ENNReal)
    (1 : ENNReal)
rw₂ : ENNReal.ofReal |(o.volumeForm : (a : Fin n → F) → ℝ) (⇑(b.reindex e) : (a : Fin n) → F)| = 1
rw₃ : ENNReal.ofReal 1 = 1
⊢ Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) :
      ENNReal)
    (1 : ENNReal)
have rw₄ : Eq (α := ENNReal) 1 1
Tactic: rw [A, parallelepiped_comp_equiv, AlternatingMap.measure_parallelepiped,
    o.abs_volumeForm_apply_of_orthonormal, ENNReal.ofReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
⊢ Eq (α := Measure F) (o.volumeForm.measure : Measure F) (volume : Measure F)
have A : Eq (α := ENNReal)
  (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
      (↑(Basis.parallelepiped (ι := Fin (finrank ℝ F)) (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) : Set F) :
    ENNReal)
  (1 : ENNReal)
Tactic: have A : o.volumeForm.measure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1 :=
    Orientation.measure_orthonormalBasis o (stdOrthonormalBasis ℝ F)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A :
  Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (↑(Basis.parallelepiped (ι := Fin (finrank ℝ F)) (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) :
          Set F) :
      ENNReal)
    (1 : ENNReal)
⊢ Eq (α := Measure F) (o.volumeForm.measure : Measure F) (volume : Measure F)
have rw : Eq (α := Measure F)
  (addHaarMeasure (Basis.parallelepiped (ι := Fin (finrank ℝ F)) (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) :
    Measure F)
  (volume : Measure F)
Tactic: rw [addHaarMeasure_unique o.volumeForm.measure
    (stdOrthonormalBasis ℝ F).toBasis.parallelepiped, A, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (hypothesis)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : Fintype ι
inst_5 : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
⊢ Eq (α := ENNReal)
    (((volume : Measure F) : (a : Set F) → ENNReal) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) : ENNReal)
    (1 : ENNReal)
have this : Fact (finrank ℝ F = finrank ℝ F)
Tactic: haveI : Fact (finrank ℝ F = finrank ℝ F) := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : Fintype ι
inst_5 : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := Basis.orientation (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))
⊢ Eq (α := ENNReal)
    (((volume : Measure F) : (a : Set F) → ENNReal) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) : ENNReal)
    (1 : ENNReal)
have rw : Eq (α := ENNReal)
  (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
      (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) :
    ENNReal)
  (1 : ENNReal)
Tactic: rw [← o.measure_eq_volume]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_4
F : Type u_5
inst : Fintype ι
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ F
inst_3 : FiniteDimensional ℝ F
inst_4 : MeasurableSpace F
inst_5 : BorelSpace F
b : OrthonormalBasis ι ℝ F
⊢ Eq (α := Measure F) (b.toBasis.addHaar : Measure F) (volume : Measure F)
have rw : Eq (α := ENNReal) (((volume : Measure F) : (a : Set F) → ENNReal) (↑b.toBasis.parallelepiped : Set F) : ENNReal)
  (1 : ENNReal)
Tactic: rw [Basis.addHaar_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : Fintype ι
inst_5 : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
⊢ MeasurePreserving.{u_3, u_1} (α := F) (β := EuclideanSpace ℝ ι) (⇑b.measurableEquiv : (a : F) → EuclideanSpace ℝ ι)
    volume volume
have h : MeasureSpace.toMeasurableSpace = inst_2 →
  Eq.{u_3 + 1} (α := autoParam (Measure F) MeasurePreserving._auto_1) volume
    (map.{u_1, u_3} (α := EuclideanSpace ℝ ι) (⇑(MeasurableEquiv.symm b.measurableEquiv) : (a : EuclideanSpace ℝ ι) → F)
      (volume : Measure (EuclideanSpace ℝ ι)))
Tactic: convert! (b.measurableEquiv.symm.measurable.measurePreserving _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : Fintype ι
inst_5 : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
e_3 : MeasureSpace.toMeasurableSpace = inst_2
⊢ Eq.{u_3 + 1} (α := autoParam (Measure F) MeasurePreserving._auto_1) volume
    (map.{u_1, u_3} (α := EuclideanSpace ℝ ι) (⇑(MeasurableEquiv.symm b.measurableEquiv) : (a : EuclideanSpace ℝ ι) → F)
      (volume : Measure (EuclideanSpace ℝ ι)))
have h : Eq.{u_3 + 1} (α := autoParam (Measure F) MeasurePreserving._auto_1) volume
  (map (⇑(MeasurableEquiv.symm b.measurableEquiv) : (a : EuclideanSpace ℝ ι) → F)
    (Basis.addHaar (OrthonormalBasis.toBasis (EuclideanSpace.basisFun ι ℝ))))
Tactic: rw [← (EuclideanSpace.basisFun ι ℝ).addHaar_eq_volume]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : MeasurableSpace F
inst_3 : BorelSpace F
inst_4 : Fintype ι
inst_5 : FiniteDimensional ℝ F
b : OrthonormalBasis ι ℝ F
e_3 : MeasureSpace.toMeasurableSpace = inst_2
⊢ Eq.{u_3 + 1} (α := autoParam (Measure F) MeasurePreserving._auto_1) volume
    (map (⇑(MeasurableEquiv.symm b.measurableEquiv) : (a : EuclideanSpace ℝ ι) → F)
      (Basis.addHaar (OrthonormalBasis.toBasis (EuclideanSpace.basisFun ι ℝ))))
have h : Eq (α := autoParam (Measure F) MeasurePreserving._auto_1) volume
  (Basis.map (OrthonormalBasis.toBasis (EuclideanSpace.basisFun ι ℝ))
      (↑(↑b.repr.symm : EuclideanSpace ℝ ι ≃L[ℝ] F) : EuclideanSpace ℝ ι ≃ₗ[ℝ] F)).addHaar
Tactic: erw [MeasurableEquiv.coe_toEquiv_symm, Basis.map_addHaar _ b.repr.symm.toContinuousLinearEquiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_4
inst : Fintype ι
⊢ MeasurePreserving.{u_4, u_4} (α := WithLp 2 (ι → ℝ)) (β := ι → ℝ)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (ι → ℝ))) : (a : WithLp 2 (ι → ℝ)) → ι → ℝ)
    (volume : Measure (WithLp 2 (ι → ℝ))) (volume : Measure (ι → ℝ))
have suffices : Eq.{u_4 + 1} (α := Measure (WithLp 2 (ι → ℝ))) volume
  (map (α := ι → ℝ) (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)) : (a : ι → ℝ) → WithLp 2 (ι → ℝ)) volume)
Tactic: suffices volume = map (MeasurableEquiv.toLp 2 (ι → ℝ)) volume by
    convert! ((MeasurableEquiv.toLp 2 (ι → ℝ)).measurable.measurePreserving _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_4
inst : Fintype ι
⊢ Eq.{u_4 + 1} (α := Measure (WithLp 2 (ι → ℝ))) volume
    (map (α := ι → ℝ) (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)) : (a : ι → ℝ) → WithLp 2 (ι → ℝ)) volume)
have rw : Eq.{u_4 + 1} (α := Measure (WithLp 2 (ι → ℝ))) volume
  (Basis.addHaar (ι := ι)
    (Basis.map (Pi.basisFun ℝ ι)
      (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv 2 ℝ fun (a : ι) ↦ ℝ)) :
        (ι → ℝ) ≃ₗ[ℝ] WithLp 2 (ι → ℝ))))
Tactic: rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar_def,
    MeasurableEquiv.coe_toLp, ← PiLp.coe_symm_continuousLinearEquiv 2 ℝ, Basis.map_addHaar]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : IsEmpty ι
⊢ Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) volume (dirac 0)
have rw : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (map (toLp 2) (volume : Measure (ι → ℝ))) (dirac 0)
Tactic: rw [← (PiLp.volume_preserving_toLp ι).map_eq, volume_pi_eq_dirac 0, map_dirac, toLp_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : IsEmpty ι
rw : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (map (toLp 2) (volume : Measure (ι → ℝ))) (dirac 0)
⊢ Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) volume (dirac 0)
have rw₁ : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (map (toLp 2) (dirac 0)) (dirac 0)
Tactic: rw [← (PiLp.volume_preserving_toLp ι).map_eq, volume_pi_eq_dirac 0, map_dirac, toLp_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : IsEmpty ι
rw : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (map (toLp 2) (volume : Measure (ι → ℝ))) (dirac 0)
rw₁ : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (map (toLp 2) (dirac 0)) (dirac 0)
⊢ Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) volume (dirac 0)
have rw₂ : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (dirac (toLp 2 0)) (dirac 0)
Tactic: rw [← (PiLp.volume_preserving_toLp ι).map_eq, volume_pi_eq_dirac 0, map_dirac, toLp_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
ι : Type u_4
inst : Fintype ι
inst_1 : IsEmpty ι
rw : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (map (toLp 2) (volume : Measure (ι → ℝ))) (dirac 0)
rw₁ : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (map (toLp 2) (dirac 0)) (dirac 0)
rw₂ : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (dirac (toLp 2 0)) (dirac 0)
⊢ Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) volume (dirac 0)
have rw₃ : Eq.{u_4 + 1} (α := Measure (EuclideanSpace ℝ ι)) (dirac 0) (dirac 0)
Tactic: rw [← (PiLp.volume_preserving_toLp ι).map_eq, volume_pi_eq_dirac 0, map_dirac, toLp_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : FiniteDimensional ℝ E
inst_9 : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
⊢ MeasurePreserving.{u_2, u_3} (α := E) (β := F) (⇑f : (a : E) → F) (volume : Measure E) (volume : Measure F)
have refine : Eq.{u_3 + 1} (α := Measure F) (map.{u_2, u_3} (α := E) (⇑f : (a : E) → F) (volume : Measure E) : Measure F)
  (volume : Measure F)
Tactic: refine ⟨f.continuous.measurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : FiniteDimensional ℝ E
inst_9 : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
⊢ Eq.{u_3 + 1} (α := Measure F) (map.{u_2, u_3} (α := E) (⇑f : (a : E) → F) (volume : Measure E) : Measure F)
    (volume : Measure F)
have rcases : ∀ (w : Finset E) (b : OrthonormalBasis ↥w ℝ E)
  (_hw : Eq (α := (a : ↥w) → E) (⇑b : (a : ↥w) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ w))),
  Eq.{u_3 + 1} (α := Measure F) (map.{u_2, u_3} (α := E) (⇑f : (a : E) → F) (volume : Measure E) : Measure F)
    (volume : Measure F)
Tactic: rcases exists_orthonormalBasis ℝ E with ⟨w, b, _hw⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : MeasurableSpace F
inst_7 : BorelSpace F
inst_8 : FiniteDimensional ℝ E
inst_9 : FiniteDimensional ℝ F
f : E ≃ₗᵢ[ℝ] F
w : Finset E
b : OrthonormalBasis ↥w ℝ E
_hw : Eq (α := (a : ↥w) → E) (⇑b : (a : ↥w) → E) (Subtype.val (p := fun (x : E) ↦ x ∈ w))
⊢ Eq.{u_3 + 1} (α := Measure F) (map.{u_2, u_3} (α := E) (⇑f : (a : E) → F) (volume : Measure E) : Measure F)
    (volume : Measure F)
have erw : Eq (α := Measure F) (b.toBasis.map (↑(↑f : E ≃L[ℝ] F) : E ≃ₗ[ℝ] F)).addHaar (b.map f).toBasis.addHaar
Tactic: erw [← OrthonormalBasis.addHaar_eq_volume b, ← OrthonormalBasis.addHaar_eq_volume (b.map f),
    Basis.map_addHaar _ f.toContinuousLinearEquiv]
-- 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
this :
  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))
⊢ MeasurePreserving (α := WithLp 2 (U × V)) (β := U × V)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V))) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))
have h : Eq (α := WithLp 2 (U × V) ≃ᵐ U × V) (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)))
  (volumePreservingSymmMeasurableEquivToLpProdAux U V)
Tactic: convert! this
-- 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
this :
  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))
⊢ Eq (α := WithLp 2 (U × V) ≃ᵐ U × V) (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)))
    (volumePreservingSymmMeasurableEquivToLpProdAux U V)
have h : ∀ (uv : WithLp 2 (U × V)),
  Eq.{u_4 + 1} (α := U) ((MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)) : (a : WithLp 2 (U × V)) → U × V) uv).1
    ((volumePreservingSymmMeasurableEquivToLpProdAux U V : (a : WithLp 2 (U × V)) → U × V) uv).1
Tactic: ext uv
-- 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
this :
  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))
h :
  ∀ (uv : WithLp 2 (U × V)),
    Eq.{u_4 + 1} (α := U)
      ((MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)) : (a : WithLp 2 (U × V)) → U × V) uv).1
      ((volumePreservingSymmMeasurableEquivToLpProdAux U V : (a : WithLp 2 (U × V)) → U × V) uv).1
⊢ Eq (α := WithLp 2 (U × V) ≃ᵐ U × V) (MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)))
    (volumePreservingSymmMeasurableEquivToLpProdAux U V)
have h₁ : ∀ (uv : WithLp 2 (U × V)),
  Eq.{u_5 + 1} (α := V) ((MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V)) : (a : WithLp 2 (U × V)) → U × V) uv).2
    ((volumePreservingSymmMeasurableEquivToLpProdAux U V : (a : WithLp 2 (U × V)) → U × V) uv).2
Tactic: ext uv
-- 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)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (U × V))) : (a : WithLp 2 (U × V)) → U × V)
    (volume : Measure (WithLp 2 (U × V))) (volume : Measure (U × V))
have suffices : 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))
Tactic: suffices MeasurePreserving (volumePreservingSymmMeasurableEquivToLpProdAux U V) by
    convert! this
    ext uv
    <;> simp [volumePreservingSymmMeasurableEquivToLpProdAux, MeasurableEquiv.coe_sumPiEquivProdPi,
      LinearEquiv.prodCongr_symm, MeasurableEquiv.prodCongr]