awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
b : OrthonormalBasis (Fin n) ℝ E
v : Fin n → E
zero :
  ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)) (b : OrthonormalBasis (Fin 0) ℝ E) (v : Fin 0 → E),
    Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin 0 → E) → ℝ) v| : ℝ)
succ :
  ∀ (n : ℕ) [_i : Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1)))
    (b : OrthonormalBasis (Fin (n + 1)) ℝ E) (v : Fin (n + 1) → E),
    Eq (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ)
      (|(b.toBasis.det : (a : Fin (n + 1) → E) → ℝ) v| : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin n → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin n → E) → ℝ) v| : ℝ)

Tactic:
cases n
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin 0 → E) → ℝ) v| : ℝ)

Tactic:
o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Premises used: Or.elim, Orientation.eq_or_eq_neg_of_isEmpty
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
zero :
  o = positiveOrientation →
    Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin 0 → E) → ℝ) v| : ℝ)
zero₁ :
  o = -positiveOrientation →
    Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin 0 → E) → ℝ) v| : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin 0 → E) → ℝ) v| : ℝ)

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Premises used: Or.elim, Orientation.eq_or_eq_neg_of_isEmpty
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ Eq (α := ℝ) (|(volumeForm positiveOrientation : (a : Fin 0 → E) → ℝ) v| : ℝ)
    (|(b.toBasis.det : (a : Fin 0 → E) → ℝ) v| : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ Eq (α := ℝ) (|(volumeForm (-positiveOrientation) : (a : Fin 0 → E) → ℝ) v| : ℝ)
    (|(b.toBasis.det : (a : Fin 0 → E) → ℝ) v| : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
b : OrthonormalBasis (Fin (n + 1)) ℝ E
v : Fin (n + 1) → E
succ :
  Eq (α := ℝ) (|((b.adjustToOrientation o).toBasis.det : (a : Fin (n + 1) → E) → ℝ) v| : ℝ)
    (|(b.toBasis.det : (a : Fin (n + 1) → E) → ℝ) v| : ℝ)
succ₁ succ₂ :
  Eq (α := ℝ) (|(b.toBasis.det : (a : Fin (n + 1) → E) → ℝ) v| : ℝ)
    (|(b.toBasis.det : (a : Fin (n + 1) → E) → ℝ) v| : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin (n + 1) → E) → ℝ) v| : ℝ)

Tactic:
rw [o.volumeForm_robust (b.adjustToOrientation o) (b.orientation_adjustToOrientation o),
      b.abs_det_adjustToOrientation]

Premises used: Orientation.volumeForm_robust, OrthonormalBasis.adjustToOrientation, OrthonormalBasis.orientation_adjustToOrientation, OrthonormalBasis.abs_det_adjustToOrientation
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : Fin n → E
zero :
  ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)) (v : Fin 0 → E),
    LE.le (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
succ :
  ∀ (n : ℕ) [_i : Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) (v : Fin (n + 1) → E),
    LE.le (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)
⊢ LE.le (α := ℝ) (|(o.volumeForm : (a : Fin n → E) → ℝ) v| : ℝ) (∏ i : Fin n, ‖v i‖ : ℝ)

Tactic:
rcases n with - | n
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
⊢ LE.le (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)

Tactic:
o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Premises used: Or.elim, Orientation.eq_or_eq_neg_of_isEmpty
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
zero : o = positiveOrientation → LE.le (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
zero₁ :
  o = -positiveOrientation → LE.le (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
⊢ LE.le (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Premises used: Or.elim, Orientation.eq_or_eq_neg_of_isEmpty
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
v : Fin 0 → E
⊢ LE.le (α := ℝ) (|(volumeForm positiveOrientation : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
v : Fin 0 → E
⊢ LE.le (α := ℝ) (|(volumeForm (-positiveOrientation) : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
⊢ FiniteDimensional ℝ E

Tactic:
haveI : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this : FiniteDimensional ℝ E
⊢ finrank ℝ E = Fintype.card (Fin n.succ)

Tactic:
simpa using _i.out

Premises used: Fact.out
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this : FiniteDimensional ℝ E
⊢ finrank ℝ E = Fintype.card (Fin n.succ)

Tactic:
have : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this_1 : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
⊢ Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)

Tactic:
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det this v
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this_1 : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
succ : LE.le (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
⊢ LE.le (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)

Tactic:
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]

Premises used: Orientation.volumeForm_robust', Finset.abs_prod
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this_1 : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
succ :
  ∀ (i : Fin n.succ),
    Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i → 0 ≤ |⟪(b : (a : Fin n.succ) → E) i, v i⟫|
succ₁ :
  ∀ (i : Fin n.succ),
    Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i → |⟪(b : (a : Fin n.succ) → E) i, v i⟫| ≤ ‖v i‖
⊢ LE.le (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)

Tactic:
apply Finset.prod_le_prod

Premises used: Finset.prod_le_prod
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this_1 : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
i : Fin n.succ
succ : Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i → 0 ≤ |⟪(b : (a : Fin n.succ) → E) i, v i⟫|
⊢ Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i → 0 ≤ |⟪(b : (a : Fin n.succ) → E) i, v i⟫|

Tactic:
_
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this_1 : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i
⊢ 0 ≤ |⟪(b : (a : Fin n.succ) → E) i, v i⟫|

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this_1 : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
i : Fin n.succ
succ : Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i → |⟪(b : (a : Fin n.succ) → E) i, v i⟫| ≤ ‖v i‖
⊢ Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i → |⟪(b : (a : Fin n.succ) → E) i, v i⟫| ≤ ‖v i‖

Tactic:
_
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this_1 : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i
⊢ |⟪(b : (a : Fin n.succ) → E) i, v i⟫| ≤ norm (E := E) ((b : (a : Fin n.succ) → E) i : E) * ‖v i‖

Tactic:
abs_real_inner_le_norm (b i) (v i)

Premises used: abs_real_inner_le_norm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this_1 : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
i : Fin n.succ
h_1 : Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i
h : ‖v i‖ = norm (E := E) ((b : (a : Fin n.succ) → E) i : E) * ‖v i‖
⊢ |⟪(b : (a : Fin n.succ) → E) i, v i⟫| ≤ ‖v i‖

Tactic:
convert! abs_real_inner_le_norm (b i) (v i)

Premises used: abs_real_inner_le_norm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this_1 : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
i : Fin n.succ
h : Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i
⊢ ‖v i‖ = norm (E := E) ((b : (a : Fin n.succ) → E) i : E) * ‖v i‖

Tactic:
simp [b.orthonormal.1 i]

Premises used: And.left, OrthonormalBasis.orthonormal
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : Fin n → E
⊢ LE.le (α := ℝ) ((o.volumeForm : (a : Fin n → E) → ℝ) v : ℝ) (∏ i : Fin n, ‖v i‖ : ℝ)

Tactic:
(le_abs_self _).trans (o.abs_volumeForm_apply_le v)

Premises used: le_abs_self, LE.le.trans, Orientation.abs_volumeForm_apply_le
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : Fin n → E
hv : Pairwise fun (i j : Fin n) ↦ ⟪v i, v j⟫ = 0
zero :
  ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)) {v : Fin 0 → E}
    (hv : Pairwise fun (i j : Fin 0) ↦ ⟪v i, v j⟫ = 0),
    Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
succ :
  ∀ (n : ℕ) [_i : Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) {v : Fin (n + 1) → E}
    (hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0),
    Eq (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin n → E) → ℝ) v| : ℝ) (∏ i : Fin n, ‖v i‖ : ℝ)

Tactic:
rcases n with - | n
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
hv : Pairwise fun (i j : Fin 0) ↦ ⟪v i, v j⟫ = 0
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)

Tactic:
o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Premises used: Or.elim, Orientation.eq_or_eq_neg_of_isEmpty
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
hv : Pairwise fun (i j : Fin 0) ↦ ⟪v i, v j⟫ = 0
zero : o = positiveOrientation → Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
zero₁ : o = -positiveOrientation → Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_

Premises used: Or.elim, Orientation.eq_or_eq_neg_of_isEmpty
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
v : Fin 0 → E
hv : Pairwise fun (i j : Fin 0) ↦ ⟪v i, v j⟫ = 0
⊢ Eq (α := ℝ) (|(volumeForm positiveOrientation : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
v : Fin 0 → E
hv : Pairwise fun (i j : Fin 0) ↦ ⟪v i, v j⟫ = 0
⊢ Eq (α := ℝ) (|(volumeForm (-positiveOrientation) : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0
⊢ FiniteDimensional ℝ E

Tactic:
haveI : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
⊢ finrank ℝ E = Fintype.card (Fin n.succ)

Tactic:
simpa using _i.out

Premises used: Fact.out
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
⊢ finrank ℝ E = Fintype.card (Fin n.succ)

Tactic:
have hdim : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
⊢ Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)

Tactic:
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det hdim v
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
succ : Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)

Tactic:
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]

Premises used: Orientation.volumeForm_robust', Finset.abs_prod
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
pos :
  ∀ (h : ∃ (i : Fin (n + 1)), v i = 0),
    Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
neg :
  ∀ (h : ∀ (i : Fin (n + 1)), v i ≠ 0),
    Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
⊢ Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)

Tactic:
by_cases! h : ∃ i, v i = 0
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
h : ∃ (i : Fin (n + 1)), v i = 0
pos :
  ∀ (i : Fin (n + 1)) (hi : v i = 0),
    Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
⊢ Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)

Tactic:
obtain ⟨i, hi⟩ := h
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
i : Fin (n + 1)
hi : v i = 0
pos : ‖v i‖ = 0
pos₁ : |⟪(b : (a : Fin n.succ) → E) i, v i⟫| = 0
⊢ Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)

Tactic:
rw [Finset.prod_eq_zero (Finset.mem_univ i), Finset.prod_eq_zero (Finset.mem_univ i)]

Premises used: Finset.mem_univ, Finset.prod_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
i : Fin (n + 1)
hi : v i = 0
⊢ ‖v i‖ = 0

Tactic:
simp [hi]
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
hv : Pairwise fun (i j : Fin (n + 1)) ↦ ⟪v i, v j⟫ = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb :
  Eq (α := ℝ) ((b.toBasis.det : (a : Fin n.succ → E) → ℝ) v : ℝ)
    (∏ i : Fin n.succ, ⟪(b : (a : Fin n.succ) → E) i, v i⟫ : ℝ)
i : Fin (n + 1)
hi : v i = 0
⊢ |⟪(b : (a : Fin n.succ) → E) i, v i⟫| = 0

Tactic:
simp [hi]