awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ Nat.casesAuxOn (motive := fun (a : ℕ) ↦ (h : n + 1 = a) → E [⋀^Fin (n + 1)]→ₗ[ℝ] ℝ) (n + 1)
      (fun (h : n + 1 = 0) ↦
        Eq.rec (motive := fun (x : ℕ) (x_1 : 0 = x) ↦
          [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)) ↦
            ⋯.by_cases (fun (x : o = positiveOrientation) ↦ AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
              fun (x : o = -positiveOrientation) ↦ -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
          ⋯ o)
      (fun (n_1 : ℕ) (h : n + 1 = n_1 + 1) ↦
        Eq.rec (motive := fun (x : ℕ) (x_1 : n_1 + 1 = x) ↦
          [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n_1 + 1)] (o : Orientation ℝ E (Fin (n_1 + 1))) ↦
            (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det)
          ⋯ o)
      ⋯ =
    -b.toBasis.det
have succ : Ne (α := Orientation ℝ E (Fin n.succ)) e.toBasis.orientation b.toBasis.orientation
Tactic: apply e.det_eq_neg_det_of_opposite_orientation b
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ Ne (α := Orientation ℝ E (Fin n.succ)) e.toBasis.orientation b.toBasis.orientation
have h : e.toBasis.orientation = o
Tactic: convert! hb.symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ (-o).volumeForm = -o.volumeForm
have zero : ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)), (-o).volumeForm = -o.volumeForm
Tactic: rcases n with - | n
Cleared hypotheses: n, _i, o
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
zero : ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)), (-o).volumeForm = -o.volumeForm
⊢ (-o).volumeForm = -o.volumeForm
have succ : ∀ (n : ℕ) [_i : Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))), (-o).volumeForm = -o.volumeForm
Tactic: rcases n with - | n
Cleared hypotheses: n, _i, o
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
⊢ (-o).volumeForm = -o.volumeForm
have zero : o = positiveOrientation → (-o).volumeForm = -o.volumeForm
Tactic: refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
zero : o = positiveOrientation → (-o).volumeForm = -o.volumeForm
⊢ (-o).volumeForm = -o.volumeForm
have zero₁ : o = -positiveOrientation → (-o).volumeForm = -o.volumeForm
Tactic: refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ Eq.{u_1 + 1} (α := E [⋀^Fin 0]→ₗ[ℝ] ℝ) (volumeForm (- -positiveOrientation)) (-volumeForm (-positiveOrientation))
have zero : Eq (α := E [⋀^Fin 0]→ₗ[ℝ] ℝ) (volumeForm (- -positiveOrientation)) (AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
Tactic: simp [volumeForm_zero_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ (-o).volumeForm = -o.volumeForm
have h₁ : e.toBasis.orientation = o
Tactic: have h₁ : e.toBasis.orientation = o := o.finOrthonormalBasis_orientation _ _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
⊢ e.toBasis.orientation ≠ -o
have symm : -o ≠ e.toBasis.orientation
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
⊢ -o ≠ e.toBasis.orientation
have rw : -o = -e.toBasis.orientation
Tactic: rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
rw : -o = -e.toBasis.orientation
⊢ -o ≠ e.toBasis.orientation
have rw₁ : -o = -o
Tactic: rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
⊢ (-o).volumeForm = -o.volumeForm
have h₂ : e.toBasis.orientation ≠ -o
Tactic: have h₂ : e.toBasis.orientation ≠ -o := by
    symm
    rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
h₂ : e.toBasis.orientation ≠ -o
⊢ (-o).volumeForm = -o.volumeForm
have succ : (-o).volumeForm = -e.toBasis.det
Tactic: rw [o.volumeForm_robust e h₁, (-o).volumeForm_robust_neg e h₂]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
h₂ : e.toBasis.orientation ≠ -o
succ : (-o).volumeForm = -e.toBasis.det
⊢ (-o).volumeForm = -o.volumeForm
have succ₁ : -e.toBasis.det = -e.toBasis.det
Tactic: rw [o.volumeForm_robust e h₁, (-o).volumeForm_robust_neg e h₂]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin n → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin n → E) → ℝ) v| : ℝ)
have 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| : ℝ)
Tactic: cases n
Cleared hypotheses: n, _i, o, b, v
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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| : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin n → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin n → E) → ℝ) v| : ℝ)
have 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| : ℝ)
Tactic: cases n
Cleared hypotheses: n, _i, o, b, v
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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| : ℝ)
have zero : o = positiveOrientation →
  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 ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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| : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin 0 → E) → ℝ) v| : ℝ)
have zero₁ : o = -positiveOrientation →
  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 ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin (n + 1) → E) → ℝ) v| : ℝ)
have succ : Eq (α := ℝ) (|((b.adjustToOrientation o).toBasis.det : (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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| : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (|(b.toBasis.det : (a : Fin (n + 1) → E) → ℝ) v| : ℝ)
have succ₁ : Eq (α := ℝ) (|(b.toBasis.det : (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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‖ : ℝ)
have 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‖ : ℝ)
Tactic: rcases n with - | n
Cleared hypotheses: n, _i, o, v
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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‖ : ℝ)
⊢ LE.le (α := ℝ) (|(o.volumeForm : (a : Fin n → E) → ℝ) v| : ℝ) (∏ i : Fin n, ‖v i‖ : ℝ)
have 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‖ : ℝ)
Tactic: rcases n with - | n
Cleared hypotheses: n, _i, o, v
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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‖ : ℝ)
have zero : o = positiveOrientation → LE.le (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
Tactic: refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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‖ : ℝ)
⊢ LE.le (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
have zero₁ : o = -positiveOrientation → LE.le (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
Tactic: refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
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
⊢ LE.le (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)
have this : FiniteDimensional ℝ E
Tactic: haveI : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
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
⊢ LE.le (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)
have this₁ : finrank ℝ E = Fintype.card (Fin n.succ)
Tactic: have : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
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
⊢ LE.le (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)
have hb : 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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⟫ : ℝ)
⊢ LE.le (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)
have succ : LE.le (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
Tactic: rw [o.volumeForm_robust' b, hb, Finset.abs_prod]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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⟫ : ℝ)
⊢ LE.le (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
have succ : ∀ (i : Fin n.succ), Membership.mem (γ := Finset (Fin n.succ)) Finset.univ i → 0 ≤ |⟪(b : (a : Fin n.succ) → E) i, v i⟫|
Tactic: apply Finset.prod_le_prod
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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⟫|
⊢ LE.le (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
have 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‖
Tactic: apply Finset.prod_le_prod
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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⟫| ≤ ‖v i‖
have h : ‖v i‖ = norm (E := E) ((b : (a : Fin n.succ) → E) i : E) * ‖v i‖
Tactic: convert! abs_real_inner_le_norm (b i) (v i)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin n → E) → ℝ) v| : ℝ) (∏ i : Fin n, ‖v i‖ : ℝ)
have 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‖ : ℝ)
Tactic: rcases n with - | n
Cleared hypotheses: n, _i, o, v, hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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‖ : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin n → E) → ℝ) v| : ℝ) (∏ i : Fin n, ‖v i‖ : ℝ)
have 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‖ : ℝ)
Tactic: rcases n with - | n
Cleared hypotheses: n, _i, o, v, hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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‖ : ℝ)
have zero : o = positiveOrientation → Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
Tactic: refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
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‖ : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
have zero₁ : o = -positiveOrientation → Eq (α := ℝ) (|(o.volumeForm : (a : Fin 0 → E) → ℝ) v| : ℝ) (∏ i : Fin 0, ‖v i‖ : ℝ)
Tactic: refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
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
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)
have this : FiniteDimensional ℝ E
Tactic: haveI : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
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
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)
have hdim : finrank ℝ E = Fintype.card (Fin n.succ)
Tactic: have hdim : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
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 (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)
have hb : 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