[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = 1
[PROOFSTEP]
apply (e.det_to_matrix_orthonormalBasis_real f).resolve_right
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ¬↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
[PROOFSTEP]
have : 0 < e.toBasis.det f := by
  rw [e.toBasis.orientation_eq_iff_det_pos] at h 
  simpa using h
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
[PROOFSTEP]
rw [e.toBasis.orientation_eq_iff_det_pos] at h 
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑(OrthonormalBasis.toBasis f)
⊢ 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
[PROOFSTEP]
simpa using h
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
this : 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
⊢ ¬↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
[PROOFSTEP]
linarith
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) ≠ Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
[PROOFSTEP]
contrapose! h
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f ≠ -1
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
[PROOFSTEP]
simp [e.toBasis.orientation_eq_iff_det_pos, (e.det_to_matrix_orthonormalBasis_real f).resolve_right h]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f) ↔
    Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
[PROOFSTEP]
constructor
[GOAL]
case mp
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f) →
    Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
[PROOFSTEP]
intro h
[GOAL]
case mp
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
[PROOFSTEP]
dsimp [Basis.orientation]
[GOAL]
case mp
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
⊢ rayOfNeZero ℝ (Basis.det (OrthonormalBasis.toBasis e)) (_ : Basis.det (OrthonormalBasis.toBasis e) ≠ 0) =
    rayOfNeZero ℝ (Basis.det (OrthonormalBasis.toBasis f)) (_ : Basis.det (OrthonormalBasis.toBasis f) ≠ 0)
[PROOFSTEP]
congr
[GOAL]
case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f) →
    Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
[PROOFSTEP]
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
[GOAL]
case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑(OrthonormalBasis.toBasis f) • Basis.det (OrthonormalBasis.toBasis f) =
    Basis.det (OrthonormalBasis.toBasis f)
[PROOFSTEP]
simp [e.det_to_matrix_orthonormalBasis_of_same_orientation f h]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) ≠ Basis.orientation (OrthonormalBasis.toBasis f)
⊢ Basis.det (OrthonormalBasis.toBasis e) = -Basis.det (OrthonormalBasis.toBasis f)
[PROOFSTEP]
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
  -- Porting note: added `neg_one_smul` with explicit type
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) ≠ Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑(OrthonormalBasis.toBasis f) • Basis.det (OrthonormalBasis.toBasis f) =
    -Basis.det (OrthonormalBasis.toBasis f)
[PROOFSTEP]
simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h, neg_one_smul ℝ (M := AlternatingMap ℝ E ℝ ι)]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Orthonormal ℝ ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x)
[PROOFSTEP]
apply e.orthonormal.orthonormal_of_forall_eq_or_eq_neg
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ ∀ (i : ι),
    ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x) i = ↑e i ∨
      ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x) i = -↑e i
[PROOFSTEP]
simpa using e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.orientation (OrthonormalBasis.toBasis (adjustToOrientation e x)) = x
[PROOFSTEP]
rw [e.toBasis_adjustToOrientation]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.orientation (Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x) = x
[PROOFSTEP]
exact e.toBasis.orientation_adjustToOrientation x
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
i : ι
⊢ ↑(adjustToOrientation e x) i = ↑e i ∨ ↑(adjustToOrientation e x) i = -↑e i
[PROOFSTEP]
simpa [← e.toBasis_adjustToOrientation] using e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x i
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.det (OrthonormalBasis.toBasis (adjustToOrientation e x)) = Basis.det (OrthonormalBasis.toBasis e) ∨
    Basis.det (OrthonormalBasis.toBasis (adjustToOrientation e x)) = -Basis.det (OrthonormalBasis.toBasis e)
[PROOFSTEP]
simpa using e.toBasis.det_adjustToOrientation x
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
v : ι → E
⊢ |↑(Basis.det (OrthonormalBasis.toBasis (adjustToOrientation e x))) v| = |↑(Basis.det (OrthonormalBasis.toBasis e)) v|
[PROOFSTEP]
simp [toBasis_adjustToOrientation]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
⊢ OrthonormalBasis (Fin n) ℝ E
[PROOFSTEP]
haveI := Fin.pos_iff_nonempty.1 hn
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ OrthonormalBasis (Fin n) ℝ E
[PROOFSTEP]
haveI := finiteDimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this✝ : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ OrthonormalBasis (Fin n) ℝ E
[PROOFSTEP]
exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <| finCongr h).adjustToOrientation x
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
[PROOFSTEP]
haveI := Fin.pos_iff_nonempty.1 hn
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
[PROOFSTEP]
haveI := finiteDimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this✝ : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
[PROOFSTEP]
exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <| finCongr h).orientation_adjustToOrientation x
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ IsEmpty (Fin Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ IsEmpty (Fin 0)
[PROOFSTEP]
infer_instance
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ AlternatingMap ℝ E ℝ (Fin n)
[PROOFSTEP]
classical
cases' n with n
· let opos : AlternatingMap ℝ E ℝ (Fin 0) := AlternatingMap.constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
  exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
· exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ AlternatingMap ℝ E ℝ (Fin n)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
⊢ AlternatingMap ℝ E ℝ (Fin Nat.zero)
[PROOFSTEP]
let opos : AlternatingMap ℝ E ℝ (Fin 0) := AlternatingMap.constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
opos : AlternatingMap ℝ E ℝ (Fin 0) := AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
⊢ AlternatingMap ℝ E ℝ (Fin Nat.zero)
[PROOFSTEP]
exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
[GOAL]
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))
⊢ AlternatingMap ℝ E ℝ (Fin (Nat.succ n))
[PROOFSTEP]
exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ volumeForm positiveOrientation = ↑AlternatingMap.constLinearEquivOfIsEmpty 1
[PROOFSTEP]
simp [volumeForm, Or.by_cases, if_pos]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ volumeForm (-positiveOrientation) = -↑AlternatingMap.constLinearEquivOfIsEmpty 1
[PROOFSTEP]
simp_rw [volumeForm, Or.by_cases, positiveOrientation]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ Nat.rec (motive := fun t => 0 = t → AlternatingMap ℝ E ℝ (Fin 0))
      (fun h =>
        if hp :
            -rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
                  (_ :
                    ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠
                      ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1) =
              rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
                (_ :
                  ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠
                    ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1) then
          AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n n_ih h =>
        Eq.rec (motive := fun x x_1 =>
          [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → AlternatingMap ℝ E ℝ (Fin x))
          (fun [Fact (finrank ℝ E = Nat.succ n)] o =>
            Basis.det
              (OrthonormalBasis.toBasis
                (Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o)))
          (_ : Nat.succ n = 0)
          (-rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
              (_ :
                ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠
                  ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1)))
      0 (_ : 0 = 0) =
    -↑AlternatingMap.constLinearEquivOfIsEmpty 1
[PROOFSTEP]
apply if_neg
[GOAL]
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ ¬-rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
          (_ :
            ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠
              ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1) =
      rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
        (_ : ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠ ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1)
[PROOFSTEP]
simp only [neg_rayOfNeZero]
[GOAL]
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ ¬rayOfNeZero ℝ (-↑AlternatingMap.constLinearEquivOfIsEmpty 1) (_ : -↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠ 0) =
      rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
        (_ : ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠ ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1)
[PROOFSTEP]
rw [ray_eq_iff, SameRay.sameRay_comm]
[GOAL]
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ ¬SameRay ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1) (-↑AlternatingMap.constLinearEquivOfIsEmpty 1)
[PROOFSTEP]
intro h
[GOAL]
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
h : SameRay ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1) (-↑AlternatingMap.constLinearEquivOfIsEmpty 1)
⊢ False
[PROOFSTEP]
simpa using congr_arg AlternatingMap.constLinearEquivOfIsEmpty.symm (eq_zero_of_sameRay_self_neg h)
[GOAL]
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)
[PROOFSTEP]
cases n
[GOAL]
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)
[PROOFSTEP]
classical
have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty
simp_rw [volumeForm, Or.by_cases, dif_pos this, Basis.det_isEmpty]
[GOAL]
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)
[PROOFSTEP]
have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty
[GOAL]
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)
[PROOFSTEP]
simp_rw [volumeForm, Or.by_cases, dif_pos this, Basis.det_isEmpty]
[GOAL]
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)
[PROOFSTEP]
simp_rw [volumeForm]
[GOAL]
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)
[PROOFSTEP]
rw [same_orientation_iff_det_eq_det, hb]
[GOAL]
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
[PROOFSTEP]
exact o.finOrthonormalBasis_orientation _ _
[GOAL]
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)
[PROOFSTEP]
cases' n with n
[GOAL]
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)
[PROOFSTEP]
classical
have : positiveOrientation ≠ o := by rwa [b.toBasis.orientation_isEmpty] at hb 
simp_rw [volumeForm, Or.by_cases, dif_neg this.symm, Basis.det_isEmpty]
[GOAL]
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)
[PROOFSTEP]
have : positiveOrientation ≠ o := by rwa [b.toBasis.orientation_isEmpty] at hb 
[GOAL]
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
⊢ positiveOrientation ≠ o
[PROOFSTEP]
rwa [b.toBasis.orientation_isEmpty] at hb 
[GOAL]
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 : positiveOrientation ≠ o
⊢ volumeForm o = -Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
simp_rw [volumeForm, Or.by_cases, dif_neg this.symm, Basis.det_isEmpty]
[GOAL]
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)
[PROOFSTEP]
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out
[GOAL]
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
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ volumeForm o = -Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
simp_rw [volumeForm]
[GOAL]
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
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ Basis.det
      (OrthonormalBasis.toBasis
        (Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o)) =
    -Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
apply e.det_eq_neg_det_of_opposite_orientation b
[GOAL]
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
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ Basis.orientation (OrthonormalBasis.toBasis e) ≠ Basis.orientation (OrthonormalBasis.toBasis b)
[PROOFSTEP]
convert hb.symm
[GOAL]
case h.e'_2
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
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = o
[PROOFSTEP]
exact o.finOrthonormalBasis_orientation _ _
[GOAL]
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
[PROOFSTEP]
cases' n with n
[GOAL]
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
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
⊢ o = positiveOrientation → volumeForm (-o) = -volumeForm o
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
⊢ o = -positiveOrientation → volumeForm (-o) = -volumeForm o
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm (-positiveOrientation) = -volumeForm positiveOrientation
[PROOFSTEP]
simp [volumeForm_zero_neg]
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm (- -positiveOrientation) = -volumeForm (-positiveOrientation)
[PROOFSTEP]
rw [neg_neg (positiveOrientation (R := ℝ))]
  -- Porting note: added
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm positiveOrientation = -volumeForm (-positiveOrientation)
[PROOFSTEP]
simp [volumeForm_zero_neg]
[GOAL]
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
[PROOFSTEP]
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out
[GOAL]
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
[PROOFSTEP]
have h₁ : e.toBasis.orientation = o := o.finOrthonormalBasis_orientation _ _
[GOAL]
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
[PROOFSTEP]
have h₂ : e.toBasis.orientation ≠ -o := by
  symm
  rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]
[GOAL]
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
[PROOFSTEP]
symm
[GOAL]
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)
[PROOFSTEP]
rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]
[GOAL]
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
[PROOFSTEP]
rw [o.volumeForm_robust e h₁, (-o).volumeForm_robust_neg e h₂]
[GOAL]
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
⊢ |↑(volumeForm o) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
cases n
[GOAL]
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
⊢ |↑(volumeForm o) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
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
⊢ o = positiveOrientation → |↑(volumeForm o) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
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
⊢ o = -positiveOrientation → |↑(volumeForm o) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
v : Fin Nat.zero → E
⊢ |↑(volumeForm positiveOrientation) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
v : Fin Nat.zero → E
⊢ |↑(volumeForm (-positiveOrientation)) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
simp
[GOAL]
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
⊢ |↑(volumeForm o) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
rw [o.volumeForm_robust (b.adjustToOrientation o) (b.orientation_adjustToOrientation o), b.abs_det_adjustToOrientation]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : Fin n → E
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin n, ‖v i‖
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
⊢ o = positiveOrientation → |↑(volumeForm o) v| ≤ ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
⊢ o = -positiveOrientation → |↑(volumeForm o) v| ≤ ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
v : Fin Nat.zero → E
⊢ |↑(volumeForm positiveOrientation) v| ≤ ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
v : Fin Nat.zero → E
⊢ |↑(volumeForm (-positiveOrientation)) v| ≤ ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
simp
[GOAL]
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))
v : Fin (Nat.succ n) → E
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
[GOAL]
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))
v : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
have : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
[GOAL]
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))
v : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ finrank ℝ E = Fintype.card (Fin (Nat.succ n))
[PROOFSTEP]
simpa using _i.out
[GOAL]
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))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
[GOAL]
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))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det this v
[GOAL]
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))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]
[GOAL]
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))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
apply Finset.prod_le_prod
[GOAL]
case succ.h0
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))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∀ (i : Fin (Nat.succ n)), i ∈ Finset.univ → 0 ≤ |inner (↑b i) (v i)|
[PROOFSTEP]
intro i _
[GOAL]
case succ.h0
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))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ 0 ≤ |inner (↑b i) (v i)|
[PROOFSTEP]
positivity
[GOAL]
case succ.h1
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))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∀ (i : Fin (Nat.succ n)), i ∈ Finset.univ → |inner (↑b i) (v i)| ≤ ‖v i‖
[PROOFSTEP]
intro i _
[GOAL]
case succ.h1
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))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ |inner (↑b i) (v i)| ≤ ‖v i‖
[PROOFSTEP]
convert abs_real_inner_le_norm (b i) (v i)
[GOAL]
case h.e'_4
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))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ ‖v i‖ = ‖↑b i‖ * ‖v i‖
[PROOFSTEP]
simp [b.orthonormal.1 i]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : Fin n → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ |↑(volumeForm o) v| = ∏ i : Fin n, ‖v i‖
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ |↑(volumeForm o) v| = ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ o = positiveOrientation → |↑(volumeForm o) v| = ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ o = -positiveOrientation → |↑(volumeForm o) v| = ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ |↑(volumeForm positiveOrientation) v| = ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ |↑(volumeForm (-positiveOrientation)) v| = ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
simp
[GOAL]
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ |↑(volumeForm o) v| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
[GOAL]
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
⊢ |↑(volumeForm o) v| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
have hdim : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
[GOAL]
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
⊢ finrank ℝ E = Fintype.card (Fin (Nat.succ n))
[PROOFSTEP]
simpa using _i.out
[GOAL]
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
⊢ |↑(volumeForm o) v| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
[GOAL]
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
⊢ |↑(volumeForm o) v| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det hdim v
[GOAL]
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ |↑(volumeForm o) v| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]
[GOAL]
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
by_cases h : ∃ i, v i = 0
[GOAL]
case pos
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∃ i, v i = 0
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
case 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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ¬∃ i, v i = 0
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
obtain ⟨i, hi⟩ := h
[GOAL]
case pos.intro
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
hi : v i = 0
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
rw [Finset.prod_eq_zero (Finset.mem_univ i), Finset.prod_eq_zero (Finset.mem_univ i)]
[GOAL]
case pos.intro
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
hi : v i = 0
⊢ ‖v i‖ = 0
[PROOFSTEP]
simp [hi]
[GOAL]
case pos.intro
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
hi : v i = 0
⊢ |inner (↑b i) (v i)| = 0
[PROOFSTEP]
simp [hi]
[GOAL]
case 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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ¬∃ i, v i = 0
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
push_neg at h 
[GOAL]
case 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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
congr
[GOAL]
case neg.e_f
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
⊢ (fun x => |inner (↑b x) (v x)|) = fun i => ‖v i‖
[PROOFSTEP]
ext i
[GOAL]
case neg.e_f.h
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
i : Fin (Nat.succ n)
⊢ |inner (↑b i) (v i)| = ‖v i‖
[PROOFSTEP]
have hb : b i = ‖v i‖⁻¹ • v i := gramSchmidtOrthonormalBasis_apply_of_orthogonal hdim hv (h i)
[GOAL]
case neg.e_f.h
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
i : Fin (Nat.succ n)
hb : ↑b i = ‖v i‖⁻¹ • v i
⊢ |inner (↑b i) (v i)| = ‖v i‖
[PROOFSTEP]
simp only [hb, inner_smul_left, real_inner_self_eq_norm_mul_norm, IsROrC.conj_to_real]
[GOAL]
case neg.e_f.h
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
i : Fin (Nat.succ n)
hb : ↑b i = ‖v i‖⁻¹ • v i
⊢ |‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)| = ‖v i‖
[PROOFSTEP]
rw [abs_of_nonneg]
[GOAL]
case neg.e_f.h
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
i : Fin (Nat.succ n)
hb : ↑b i = ‖v i‖⁻¹ • v i
⊢ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖) = ‖v i‖
[PROOFSTEP]
field_simp
[GOAL]
case neg.e_f.h
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
i : Fin (Nat.succ n)
hb : ↑b i = ‖v i‖⁻¹ • v i
⊢ 0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : OrthonormalBasis (Fin n) ℝ E
⊢ |↑(volumeForm o) ↑v| = 1
[PROOFSTEP]
simpa [o.volumeForm_robust' v v] using congr_arg abs v.toBasis.det_self
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : Fact (finrank ℝ F = n)
φ : E ≃ₗᵢ[ℝ] F
x : Fin n → F
⊢ ↑(volumeForm (↑(map (Fin n) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
inst✝ : Fact (finrank ℝ F = Nat.zero)
x : Fin Nat.zero → F
⊢ ↑(volumeForm (↑(map (Fin Nat.zero) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
inst✝ : Fact (finrank ℝ F = Nat.zero)
x : Fin Nat.zero → F
⊢ o = positiveOrientation →
    ↑(volumeForm (↑(map (Fin Nat.zero) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
inst✝ : Fact (finrank ℝ F = Nat.zero)
x : Fin Nat.zero → F
⊢ o = -positiveOrientation →
    ↑(volumeForm (↑(map (Fin Nat.zero) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = Nat.zero)
inst✝ : Fact (finrank ℝ F = Nat.zero)
x : Fin Nat.zero → F
⊢ ↑(volumeForm (↑(map (Fin Nat.zero) φ.toLinearEquiv) positiveOrientation)) x =
    ↑(volumeForm positiveOrientation) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = Nat.zero)
inst✝ : Fact (finrank ℝ F = Nat.zero)
x : Fin Nat.zero → F
⊢ ↑(volumeForm (↑(map (Fin Nat.zero) φ.toLinearEquiv) (-positiveOrientation))) x =
    ↑(volumeForm (-positiveOrientation)) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
simp
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
⊢ ↑(volumeForm (↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ ↑(volumeForm (↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
have he : e.toBasis.orientation = o := o.finOrthonormalBasis_orientation n.succ_pos Fact.out
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ ↑(volumeForm (↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
have heφ : (e.map φ).toBasis.orientation = Orientation.map (Fin n.succ) φ.toLinearEquiv o :=
  by
  rw [← he]
  exact e.toBasis.orientation_map φ.toLinearEquiv
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ Basis.orientation (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ)) = ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o
[PROOFSTEP]
rw [← he]
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ Basis.orientation (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ)) =
    ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) (Basis.orientation (OrthonormalBasis.toBasis e))
[PROOFSTEP]
exact e.toBasis.orientation_map φ.toLinearEquiv
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
heφ :
  Basis.orientation (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ)) = ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o
⊢ ↑(volumeForm (↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
rw [(Orientation.map (Fin n.succ) φ.toLinearEquiv o).volumeForm_robust (e.map φ) heφ]
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
heφ :
  Basis.orientation (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ)) = ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o
⊢ ↑(Basis.det (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ))) x =
    ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
rw [o.volumeForm_robust e he]
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
heφ :
  Basis.orientation (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ)) = ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o
⊢ ↑(Basis.det (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ))) x =
    ↑(Basis.det (OrthonormalBasis.toBasis e)) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x : Fin n → E
⊢ ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
x : Fin Nat.zero → E
⊢ ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
x : Fin Nat.zero → E
⊢ o = positiveOrientation → ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
x : Fin Nat.zero → E
⊢ o = -positiveOrientation → ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = Nat.zero)
x : Fin Nat.zero → E
⊢ ↑(volumeForm positiveOrientation) (↑φ ∘ x) = ↑(volumeForm positiveOrientation) x
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = Nat.zero)
x : Fin Nat.zero → E
⊢ ↑(volumeForm (-positiveOrientation)) (↑φ ∘ x) = ↑(volumeForm (-positiveOrientation)) x
[PROOFSTEP]
simp
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
⊢ ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
convert o.volumeForm_map φ (φ ∘ x)
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ o = ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o
[PROOFSTEP]
symm
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o = o
[PROOFSTEP]
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ 
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ Fintype.card (Fin (Nat.succ n)) = finrank ℝ E
[PROOFSTEP]
rw [_i.out, Fintype.card_fin]
[GOAL]
case h.e'_3.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ x = ↑(LinearIsometryEquiv.symm φ) ∘ ↑φ ∘ x
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.e'_6.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
x✝ : Fin (Nat.succ n)
⊢ x x✝ = (↑(LinearIsometryEquiv.symm φ) ∘ ↑φ ∘ x) x✝
[PROOFSTEP]
simp
