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
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin Nat.zero, ‖v i‖

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
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin (Nat.succ n), ‖v i‖
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
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin n, ‖v i‖
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))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin (Nat.succ n), ‖v i‖
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
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin (Nat.succ n), ‖v i‖
haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ 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))
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))
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin (Nat.succ n), ‖v i‖
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
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin (Nat.succ n), ‖v i‖
have hdim : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.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))
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
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin (Nat.succ n), ‖v i‖
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))
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin (Nat.succ n), ‖v i‖
let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim 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))
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)
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin (Nat.succ n), ‖v i‖
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
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin (Nat.succ n), ‖v i‖
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det hdim 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))
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), abs (inner (↑b x) (v x)) = ∏ i : Fin (Nat.succ n), ‖v i‖
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)
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin (Nat.succ n), ‖v i‖
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]
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), abs (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), abs (inner (↑b x) (v x)) = ∏ i : Fin (Nat.succ n), ‖v i‖
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), abs (inner (↑b x) (v x)) = ∏ i : Fin (Nat.succ n), ‖v i‖
by_cases h : ∃ i, v i = 0
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), abs (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), abs (inner (↑b x) (v x)) = ∏ i : Fin (Nat.succ n), ‖v i‖
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), abs (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), abs (inner (↑b x) (v x)) = ∏ i : Fin (Nat.succ n), ‖v i‖
obtain ⟨i, hi⟩ := h
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), abs (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), abs (inner (↑b x) (v x)) = ∏ i : Fin (Nat.succ n), ‖v i‖
push_neg at h
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 => abs (inner (↑b x) (v x))) = fun i => ‖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 : Fin (Nat.succ n)), v i ≠ 0
⊢ ∏ x : Fin (Nat.succ n), abs (inner (↑b x) (v x)) = ∏ i : Fin (Nat.succ n), ‖v i‖
congr
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)
⊢ abs (inner (↑b i) (v i)) = ‖v i‖
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 => abs (inner (↑b x) (v x))) = fun i => ‖v i‖
ext i
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
⊢ abs (inner (↑b i) (v i)) = ‖v i‖
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)
⊢ abs (inner (↑b i) (v i)) = ‖v i‖
have hb : b i = ‖v i‖⁻¹ • v i := gramSchmidtOrthonormalBasis_apply_of_orthogonal hdim hv (h i)
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
⊢ abs (‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)) = ‖v i‖
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
⊢ abs (inner (↑b i) (v i)) = ‖v i‖
simp only [hb, inner_smul_left, real_inner_self_eq_norm_mul_norm, IsROrC.conj_to_real]
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‖

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‖)
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
⊢ abs (‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)) = ‖v i‖
rw [abs_of_nonneg]
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)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ abs (↑(volumeForm o) v) = ∏ i : Fin Nat.zero, ‖v i‖
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _ <;> rintro rfl <;> simp
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))
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))
simpa using _i.out
no goals
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), abs (inner (↑b x) (v x)) = ∏ i : Fin (Nat.succ n), ‖v i‖
rw [Finset.prod_eq_zero (Finset.mem_univ i), Finset.prod_eq_zero (Finset.mem_univ i)] <;>
  simp [hi]
no goals
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‖
field_simp
no goals
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‖)
positivity