awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
f : E ≃ₗᵢ[ℝ] F
⊢ Eq (α := F ≃ᵐ E) f.symm.toMeasurableEquiv (MeasurableEquiv.symm f.toMeasurableEquiv)

Tactic:
rfl

Premises used: MeasurableEquiv.symm, Homeomorph.toMeasurableEquiv, LinearIsometryEquiv.toMeasurableEquiv, LinearEquiv.toEquiv, Equiv.symm, rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
f : E ≃ₗᵢ[ℝ] F
⊢ Eq (α := (a : F) → E) (⇑(MeasurableEquiv.symm f.toMeasurableEquiv) : (a : F) → E) (⇑f.symm : (a : F) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
refine : Fintype.card ι = n
⊢ ι ≃ Fin n

Tactic:
refine Fintype.equivFinOfCardEq ?_

Premises used: Fintype.equivFinOfCardEq
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
rw : Fintype.card ι = finrank ℝ F
rw₁ rw₂ : Fintype.card ι = Fintype.card ι
⊢ Fintype.card ι = n

Tactic:
rw [← _i.out, finrank_eq_card_basis b.toBasis]

Premises used: Module.finrank_eq_card_basis, Fact.out, OrthonormalBasis.toBasis
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
have :
  ∀ (e : ι ≃ Fin n),
    Eq (α := ENNReal)
      (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
          (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → 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)

Tactic:
have e : ι ≃ Fin n := by
    refine Fintype.equivFinOfCardEq ?_
    rw [← _i.out, finrank_eq_card_basis b.toBasis]
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
h :
  ∀ (x : ι),
    Eq (α := F) ((b : (a : ι) → F) x : F)
      (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n) x : F)
⊢ Eq (α := (a : ι) → F) (⇑b : (a : ι) → F)
    (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
x : ι
⊢ Eq (α := F) ((b : (a : ι) → F) x : F)
    (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n) x : F)

Tactic:
simp only [OrthonormalBasis.coe_reindex, Function.comp_apply, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, OrthonormalBasis.coe_reindex, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
⊢ Eq (α := (a : ι) → F) (⇑b : (a : ι) → F)
    (Function.comp (β := Fin n) (⇑(b.reindex e) : (a : Fin n) → F) (⇑e : (a : ι) → Fin n))

Tactic:
have A : ⇑b = b.reindex e ∘ e := by
    ext x
    simp only [OrthonormalBasis.coe_reindex, Function.comp_apply, Equiv.symm_apply_apply]
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
rw₄ rw₅ : Eq (α := ENNReal) 1 1
⊢ Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) :
      ENNReal)
    (1 : ENNReal)

Tactic:
rw [A, parallelepiped_comp_equiv, AlternatingMap.measure_parallelepiped,
    o.abs_volumeForm_apply_of_orthonormal, ENNReal.ofReal_one]

Premises used: Orientation.abs_volumeForm_apply_of_orthonormal, ENNReal.ofReal_one, parallelepiped_comp_equiv, AlternatingMap.measure_parallelepiped
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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 (α := 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)
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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)
rw :
  Eq (α := Measure F)
    (addHaarMeasure
        (Basis.parallelepiped (ι := Fin (finrank ℝ F)) (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) :
      Measure F)
    (volume : Measure F)
⊢ Eq (α := Measure F) (o.volumeForm.measure : Measure F) (volume : Measure F)

Tactic:
rw [addHaarMeasure_unique o.volumeForm.measure
    (stdOrthonormalBasis ℝ F).toBasis.parallelepiped, A, one_smul]

Premises used: Real, MeasureTheory.Measure.addHaarMeasure_unique, one_smul, Orientation.volumeForm, OrthonormalBasis.toBasis, Module.Basis.parallelepiped, AlternatingMap.measure, stdOrthonormalBasis
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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)
    (addHaarMeasure
        (Basis.parallelepiped (ι := Fin (finrank ℝ F)) (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) :
      Measure F)
    (volume : Measure F)

Tactic:
simp only [volume, Basis.addHaar]

Premises used: MeasureTheory.MeasureSpace.volume, Module.Basis.addHaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
⊢ Fact (finrank ℝ F = finrank ℝ F)

Tactic:
haveI : Fact (finrank ℝ F = finrank ℝ F) := ⟨rfl⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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))
rw :
  Eq (α := ENNReal)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) :
      ENNReal)
    (1 : ENNReal)
⊢ Eq (α := ENNReal)
    (((volume : Measure F) : (a : Set F) → ENNReal) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) : ENNReal)
    (1 : ENNReal)

Tactic:
rw [← o.measure_eq_volume]

Premises used: Orientation.measure_eq_volume
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) :
      ENNReal)
    (1 : ENNReal)

Tactic:
o.measure_orthonormalBasis b

Premises used: Orientation.measure_orthonormalBasis
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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)
    (((o.volumeForm.measure : Measure F) : (a : Set F) → ENNReal)
        (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → F)) :
      ENNReal)
    (1 : ENNReal)

Tactic:
exact o.measure_orthonormalBasis b

Premises used: Orientation.measure_orthonormalBasis
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
rw :
  Eq (α := ENNReal) (((volume : Measure F) : (a : Set F) → ENNReal) (↑b.toBasis.parallelepiped : Set F) : ENNReal)
    (1 : ENNReal)
⊢ Eq (α := Measure F) (b.toBasis.addHaar : Measure F) (volume : Measure F)

Tactic:
rw [Basis.addHaar_eq_iff]

Premises used: Module.Basis.addHaar_eq_iff
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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 (α := ENNReal) (((volume : Measure F) : (a : Set F) → ENNReal) (↑b.toBasis.parallelepiped : Set F) : ENNReal)
    (1 : ENNReal)

Tactic:
b.volume_parallelepiped

Premises used: PiLp.single, Function.update, setOf, OrthonormalBasis.volume_parallelepiped, Pi.single, dite, Set.image, parallelepiped
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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 (α := ENNReal) (((volume : Measure F) : (a : Set F) → ENNReal) (↑b.toBasis.parallelepiped : Set F) : ENNReal)
    (1 : ENNReal)

Tactic:
exact b.volume_parallelepiped

Premises used: OrthonormalBasis.volume_parallelepiped
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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 ℝ ι)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.symm b.measurableEquiv)) : (a : F) → EuclideanSpace ℝ ι)
    (map.{u_1, u_3} (α := EuclideanSpace ℝ ι) (⇑(MeasurableEquiv.symm b.measurableEquiv) : (a : EuclideanSpace ℝ ι) → F)
      (volume : Measure (EuclideanSpace ℝ ι)))
    (volume : Measure (EuclideanSpace ℝ ι))

Tactic:
(b.measurableEquiv.symm.measurable.measurePreserving _).symm

Premises used: MeasureTheory.MeasurePreserving.symm, Measurable.measurePreserving, MeasurableEquiv.symm, OrthonormalBasis.measurableEquiv, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
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 ℝ ι)))
⊢ MeasurePreserving.{u_3, u_1} (α := F) (β := EuclideanSpace ℝ ι) (⇑b.measurableEquiv : (a : F) → EuclideanSpace ℝ ι)
    volume volume

Tactic:
convert! (b.measurableEquiv.symm.measurable.measurePreserving _).symm

Premises used: MeasureTheory.MeasurePreserving.symm, Measurable.measurePreserving, MeasurableEquiv.symm, OrthonormalBasis.measurableEquiv, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
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 ι ℝ))))
⊢ 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:
rw [← (EuclideanSpace.basisFun ι ℝ).addHaar_eq_volume]

Premises used: Real, EuclideanSpace.basisFun, OrthonormalBasis.addHaar_eq_volume
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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
h :
  Eq (α := autoParam (Measure F) MeasurePreserving._auto_1) volume
    (Basis.map (OrthonormalBasis.toBasis (EuclideanSpace.basisFun ι ℝ))
        (↑(↑b.repr.symm : EuclideanSpace ℝ ι ≃L[ℝ] F) : EuclideanSpace ℝ ι ≃ₗ[ℝ] F)).addHaar
⊢ 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:
erw [MeasurableEquiv.coe_toEquiv_symm, Basis.map_addHaar _ b.repr.symm.toContinuousLinearEquiv]

Premises used: LinearIsometryEquiv.symm, OrthonormalBasis.repr, MeasurableEquiv.coe_toEquiv_symm, LinearIsometryEquiv.toContinuousLinearEquiv, Module.Basis.map_addHaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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 (α := autoParam (Measure F) MeasurePreserving._auto_1) volume
    (Basis.map (OrthonormalBasis.toBasis (EuclideanSpace.basisFun ι ℝ))
        (↑(↑b.repr.symm : EuclideanSpace ℝ ι ≃L[ℝ] F) : EuclideanSpace ℝ ι ≃ₗ[ℝ] F)).addHaar

Tactic:
b.addHaar_eq_volume.symm

Premises used: Module.Basis.ofEquivFun, LinearEquiv.symm, Module.Basis.map, LinearEquiv.toEquiv, Eq.symm, OrthonormalBasis.addHaar_eq_volume, LinearEquiv.trans, OrthonormalBasis.toBasis
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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 (α := autoParam (Measure F) MeasurePreserving._auto_1) volume
    (Basis.map (OrthonormalBasis.toBasis (EuclideanSpace.basisFun ι ℝ))
        (↑(↑b.repr.symm : EuclideanSpace ℝ ι ≃L[ℝ] F) : EuclideanSpace ℝ ι ≃ₗ[ℝ] F)).addHaar

Tactic:
exact b.addHaar_eq_volume.symm

Premises used: Eq.symm, OrthonormalBasis.addHaar_eq_volume
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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.repr : (a : F) → EuclideanSpace ℝ ι) volume volume

Tactic:
b.measurePreserving_measurableEquiv

Premises used: OrthonormalBasis.measurePreserving_measurableEquiv
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
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_1, u_3} (α := EuclideanSpace ℝ ι) (β := F) (⇑b.repr.symm : (a : EuclideanSpace ℝ ι) → F) volume
    volume

Tactic:
b.measurePreserving_measurableEquiv.symm

Premises used: MeasureTheory.MeasurePreserving.symm, OrthonormalBasis.measurePreserving_measurableEquiv
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
ι : Type u_4
inst : Fintype ι
this :
  Eq.{u_4 + 1} (α := Measure (WithLp 2 (ι → ℝ))) volume
    (map (α := ι → ℝ) (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)) : (a : ι → ℝ) → WithLp 2 (ι → ℝ)) volume)
⊢ MeasurePreserving.{u_4, u_4} (α := WithLp 2 (ι → ℝ)) (β := ι → ℝ)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (ι → ℝ))) : (a : WithLp 2 (ι → ℝ)) → ι → ℝ)
    (map (α := ι → ℝ) (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)) : (a : ι → ℝ) → WithLp 2 (ι → ℝ)) (volume : Measure (ι → ℝ)))
    (volume : Measure (ι → ℝ))

Tactic:
((MeasurableEquiv.toLp 2 (ι → ℝ)).measurable.measurePreserving _).symm

Premises used: MeasurableEquiv.toLp, MeasureTheory.MeasurePreserving.symm, Measurable.measurePreserving, MeasurableEquiv.measurable, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
ι : Type u_4
inst : Fintype ι
this :
  Eq.{u_4 + 1} (α := Measure (WithLp 2 (ι → ℝ))) volume
    (map (α := ι → ℝ) (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)) : (a : ι → ℝ) → WithLp 2 (ι → ℝ)) volume)
⊢ MeasurePreserving.{u_4, u_4} (α := WithLp 2 (ι → ℝ)) (β := ι → ℝ)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (ι → ℝ))) : (a : WithLp 2 (ι → ℝ)) → ι → ℝ)
    (volume : Measure (WithLp 2 (ι → ℝ))) (volume : Measure (ι → ℝ))

Tactic:
convert! ((MeasurableEquiv.toLp 2 (ι → ℝ)).measurable.measurePreserving _).symm

Premises used: MeasurableEquiv.toLp, MeasureTheory.MeasurePreserving.symm, Measurable.measurePreserving, MeasurableEquiv.measurable, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
ι : Type u_4
inst : Fintype ι
suffices :
  Eq.{u_4 + 1} (α := Measure (WithLp 2 (ι → ℝ))) volume
    (map (α := ι → ℝ) (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)) : (a : ι → ℝ) → WithLp 2 (ι → ℝ)) volume)
⊢ MeasurePreserving.{u_4, u_4} (α := WithLp 2 (ι → ℝ)) (β := ι → ℝ)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.toLp 2 (ι → ℝ))) : (a : WithLp 2 (ι → ℝ)) → ι → ℝ)
    (volume : Measure (WithLp 2 (ι → ℝ))) (volume : Measure (ι → ℝ))

Tactic:
suffices volume = map (MeasurableEquiv.toLp 2 (ι → ℝ)) volume by
    convert! ((MeasurableEquiv.toLp 2 (ι → ℝ)).measurable.measurePreserving _).symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
ι : Type u_4
inst : Fintype ι
rw :
  Eq.{u_4 + 1} (α := Measure (WithLp 2 (ι → ℝ))) volume
    (Basis.addHaar (ι := ι)
      (Basis.map (Pi.basisFun ℝ ι)
        (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv 2 ℝ fun (a : ι) ↦ ℝ)) :
          (ι → ℝ) ≃ₗ[ℝ] WithLp 2 (ι → ℝ))))
⊢ Eq.{u_4 + 1} (α := Measure (WithLp 2 (ι → ℝ))) volume
    (map (α := ι → ℝ) (⇑(MeasurableEquiv.toLp 2 (ι → ℝ)) : (a : ι → ℝ) → WithLp 2 (ι → ℝ)) volume)

Tactic:
rw [← addHaarMeasure_eq_volume_pi, ← Basis.parallelepiped_basisFun, ← Basis.addHaar_def,
    MeasurableEquiv.coe_toLp, ← PiLp.coe_symm_continuousLinearEquiv 2 ℝ, Basis.map_addHaar]

Premises used: Real, Module.Basis.parallelepiped_basisFun, MeasurableEquiv.coe_toLp, Module.Basis.addHaar_def, MeasureTheory.addHaarMeasure_eq_volume_pi, PiLp.coe_symm_continuousLinearEquiv, Module.Basis.map_addHaar, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
ι : Type u_4
inst : Fintype ι
⊢ Eq.{u_4 + 1} (α := Measure (WithLp 2 (ι → ℝ))) volume
    (Basis.addHaar (ι := ι)
      (Basis.map (Pi.basisFun ℝ ι)
        (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv 2 ℝ fun (a : ι) ↦ ℝ)) :
          (ι → ℝ) ≃ₗ[ℝ] WithLp 2 (ι → ℝ))))

Tactic:
(EuclideanSpace.basisFun _ _).addHaar_eq_volume.symm

Premises used: Module.Basis.ofEquivFun, LinearEquiv.symm, Module.Basis.map, EuclideanSpace.basisFun, Eq.symm, OrthonormalBasis.addHaar_eq_volume, LinearEquiv.trans, OrthonormalBasis.toBasis
-- Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Goal:
ι : Type u_4
inst : Fintype ι
⊢ Eq.{u_4 + 1} (α := Measure (WithLp 2 (ι → ℝ))) volume
    (Basis.addHaar (ι := ι)
      (Basis.map (Pi.basisFun ℝ ι)
        (↑(ContinuousLinearEquiv.symm (PiLp.continuousLinearEquiv 2 ℝ fun (a : ι) ↦ ℝ)) :
          (ι → ℝ) ≃ₗ[ℝ] WithLp 2 (ι → ℝ))))

Tactic:
exact (EuclideanSpace.basisFun _ _).addHaar_eq_volume.symm

Premises used: EuclideanSpace.basisFun, Eq.symm, OrthonormalBasis.addHaar_eq_volume