case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)

case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = Nat.succ n✝)
o : Orientation ℝ E (Fin (Nat.succ n✝))
b : OrthonormalBasis (Fin (Nat.succ n✝)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
b : OrthonormalBasis (Fin n) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
cases n
no goals
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
classical
  have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty
  simp_rw [volumeForm, Or.by_cases, dif_pos this, Basis.det_isEmpty]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
this : o = positiveOrientation
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty
no goals
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
this : o = positiveOrientation
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
simp_rw [volumeForm, Or.by_cases, dif_pos this, Basis.det_isEmpty]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = Nat.succ n✝)
o : Orientation ℝ E (Fin (Nat.succ n✝))
b : OrthonormalBasis (Fin (Nat.succ n✝)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ Basis.det
      (OrthonormalBasis.toBasis
        (Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n✝) (_ : finrank ℝ E = Nat.succ n✝) o)) =
    Basis.det (OrthonormalBasis.toBasis b)
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = Nat.succ n✝)
o : Orientation ℝ E (Fin (Nat.succ n✝))
b : OrthonormalBasis (Fin (Nat.succ n✝)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
simp_rw [volumeForm]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = Nat.succ n✝)
o : Orientation ℝ E (Fin (Nat.succ n✝))
b : OrthonormalBasis (Fin (Nat.succ n✝)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ Basis.orientation
      (OrthonormalBasis.toBasis
        (Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n✝) (_ : finrank ℝ E = Nat.succ n✝) o)) =
    o
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = Nat.succ n✝)
o : Orientation ℝ E (Fin (Nat.succ n✝))
b : OrthonormalBasis (Fin (Nat.succ n✝)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ Basis.det
      (OrthonormalBasis.toBasis
        (Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n✝) (_ : finrank ℝ E = Nat.succ n✝) o)) =
    Basis.det (OrthonormalBasis.toBasis b)
rw [same_orientation_iff_det_eq_det, hb]
no goals
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = Nat.succ n✝)
o : Orientation ℝ E (Fin (Nat.succ n✝))
b : OrthonormalBasis (Fin (Nat.succ n✝)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ Basis.orientation
      (OrthonormalBasis.toBasis
        (Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n✝) (_ : finrank ℝ E = Nat.succ n✝) o)) =
    o
exact o.finOrthonormalBasis_orientation _ _