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
v : Fin Nat.zero → E
⊢ abs (↑(volumeForm o) v) = abs (↑(Basis.det (OrthonormalBasis.toBasis b)) v)

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
v : Fin (Nat.succ n✝) → E
⊢ abs (↑(volumeForm o) v) = abs (↑(Basis.det (OrthonormalBasis.toBasis b)) v)
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
v : Fin n → E
⊢ abs (↑(volumeForm o) v) = abs (↑(Basis.det (OrthonormalBasis.toBasis b)) v)
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
v : Fin Nat.zero → E
⊢ abs (↑(volumeForm o) v) = abs (↑(Basis.det (OrthonormalBasis.toBasis b)) v)
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _ <;> rintro rfl <;> simp
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
v : Fin (Nat.succ n✝) → E
⊢ abs (↑(volumeForm o) v) = abs (↑(Basis.det (OrthonormalBasis.toBasis b)) v)
rw [o.volumeForm_robust (b.adjustToOrientation o) (b.orientation_adjustToOrientation o),
  b.abs_det_adjustToOrientation]