case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
⊢ volumeForm (-o) = -volumeForm 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))
⊢ volumeForm (-o) = -volumeForm o
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ volumeForm (-o) = -volumeForm o
cases' n with n
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))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ volumeForm (-o) = -volumeForm 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))
⊢ volumeForm (-o) = -volumeForm o
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out
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))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ volumeForm (-o) = -volumeForm 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))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ volumeForm (-o) = -volumeForm o
have h₁ : e.toBasis.orientation = o := o.finOrthonormalBasis_orientation _ _
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))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
h₂ : Basis.orientation (OrthonormalBasis.toBasis e) ≠ -o
⊢ volumeForm (-o) = -volumeForm 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))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ volumeForm (-o) = -volumeForm o
have h₂ : e.toBasis.orientation ≠ -o := by
  symm
  rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]
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))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
h₂ : Basis.orientation (OrthonormalBasis.toBasis e) ≠ -o
⊢ volumeForm (-o) = -volumeForm o
rw [o.volumeForm_robust e h₁, (-o).volumeForm_robust_neg e h₂]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm (-positiveOrientation) = -volumeForm positiveOrientation

case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm (- -positiveOrientation) = -volumeForm (-positiveOrientation)
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
⊢ volumeForm (-o) = -volumeForm o
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _ <;> rintro rfl
no goals
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm (-positiveOrientation) = -volumeForm positiveOrientation
simp [volumeForm_zero_neg]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm positiveOrientation = -volumeForm (-positiveOrientation)
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm (- -positiveOrientation) = -volumeForm (-positiveOrientation)
rw [neg_neg (positiveOrientation (R := ℝ))]
no goals
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm positiveOrientation = -volumeForm (-positiveOrientation)
simp [volumeForm_zero_neg]
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))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ -o ≠ Basis.orientation (OrthonormalBasis.toBasis e)
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))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ Basis.orientation (OrthonormalBasis.toBasis e) ≠ -o
symm
no goals
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))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ -o ≠ Basis.orientation (OrthonormalBasis.toBasis e)
rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]