[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
⊢ ↑↑(AlternatingMap.measure (volumeForm o)) (parallelepiped ↑b) = 1
[PROOFSTEP]
have e : ι ≃ Fin n := by
  refine' Fintype.equivFinOfCardEq _
  rw [← _i.out, finrank_eq_card_basis b.toBasis]
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
⊢ ι ≃ Fin n
[PROOFSTEP]
refine' Fintype.equivFinOfCardEq _
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
⊢ Fintype.card ι = n
[PROOFSTEP]
rw [← _i.out, finrank_eq_card_basis b.toBasis]
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
⊢ ↑↑(AlternatingMap.measure (volumeForm o)) (parallelepiped ↑b) = 1
[PROOFSTEP]
have A : ⇑b = b.reindex e ∘ e := by
  ext x
  simp only [OrthonormalBasis.coe_reindex, Function.comp_apply, Equiv.symm_apply_apply]
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
⊢ ↑b = ↑(OrthonormalBasis.reindex b e) ∘ ↑e
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
x : ι
⊢ ↑b x = (↑(OrthonormalBasis.reindex b e) ∘ ↑e) x
[PROOFSTEP]
simp only [OrthonormalBasis.coe_reindex, Function.comp_apply, Equiv.symm_apply_apply]
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
A : ↑b = ↑(OrthonormalBasis.reindex b e) ∘ ↑e
⊢ ↑↑(AlternatingMap.measure (volumeForm o)) (parallelepiped ↑b) = 1
[PROOFSTEP]
rw [A, parallelepiped_comp_equiv, AlternatingMap.measure_parallelepiped, o.abs_volumeForm_apply_of_orthonormal,
  ENNReal.ofReal_one]
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
⊢ AlternatingMap.measure (volumeForm o) = volume
[PROOFSTEP]
have A : o.volumeForm.measure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped = 1 :=
  Orientation.measure_orthonormalBasis o (stdOrthonormalBasis ℝ F)
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A :
  ↑↑(AlternatingMap.measure (volumeForm o))
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) =
    1
⊢ AlternatingMap.measure (volumeForm o) = volume
[PROOFSTEP]
rw [addHaarMeasure_unique o.volumeForm.measure (stdOrthonormalBasis ℝ F).toBasis.parallelepiped, A, one_smul]
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
m n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
A :
  ↑↑(AlternatingMap.measure (volumeForm o))
      ↑(Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) =
    1
⊢ addHaarMeasure (Basis.parallelepiped (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))) = volume
[PROOFSTEP]
simp only [volume, Basis.addHaar]
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
⊢ ↑↑volume (parallelepiped ↑b) = 1
[PROOFSTEP]
haveI : Fact (finrank ℝ F = finrank ℝ F) := ⟨rfl⟩
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
⊢ ↑↑volume (parallelepiped ↑b) = 1
[PROOFSTEP]
let o := (stdOrthonormalBasis ℝ F).toBasis.orientation
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := Basis.orientation (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))
⊢ ↑↑volume (parallelepiped ↑b) = 1
[PROOFSTEP]
rw [← o.measure_eq_volume]
[GOAL]
ι : Type u_1
F : Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
this : Fact (finrank ℝ F = finrank ℝ F)
o : Orientation ℝ F (Fin (finrank ℝ F)) := Basis.orientation (OrthonormalBasis.toBasis (stdOrthonormalBasis ℝ F))
⊢ ↑↑(AlternatingMap.measure (Orientation.volumeForm o)) (parallelepiped ↑b) = 1
[PROOFSTEP]
exact o.measure_orthonormalBasis b
