awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
hnc :
  ¬Eq.{u_1 + 1} (α := Orientation ℝ E (Fin 0))
      (-rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) ⋯ :
        Orientation ℝ E (Fin 0))
      (rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) ⋯ :
        Ray ℝ (E [⋀^Fin 0]→ₗ[ℝ] ℝ))
⊢ Eq.{u_1 + 1} (α := E [⋀^Fin 0]→ₗ[ℝ] ℝ)
    (Nat.casesAuxOn (motive := fun (a : ℕ) ↦ (h : 0 = a) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
        (fun (h : Eq (α := ℕ) 0 0) ↦
          if hp :
              Eq.{u_1 + 1} (α := Orientation ℝ E (Fin 0))
                (-rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) ⋯ :
                  Orientation ℝ E (Fin 0))
                (rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) ⋯ :
                  Ray ℝ (E [⋀^Fin 0]→ₗ[ℝ] ℝ)) then
            AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
          else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
        (fun (n : ℕ) (h : 0 = n + 1) ↦
          Eq.rec (motive := fun (x : ℕ) (x_1 : n + 1 = x) ↦
            [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
            (fun [Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) ↦
              (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det)
            ⋯ (-rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) ⋯))
        ⋯ :
      E [⋀^Fin 0]→ₗ[ℝ] ℝ)
    (-(AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1 : E [⋀^Fin 0]→ₗ[ℝ] ℝ)

Tactic:
apply if_neg

Premises used: if_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
hnc :
  ¬SameRay.{0, u_1} ℝ (M := E [⋀^Fin 0]→ₗ[ℝ] ℝ)
      ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1 : E [⋀^Fin 0]→ₗ[ℝ] ℝ)
      (-(AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1 : E [⋀^Fin 0]→ₗ[ℝ] ℝ)
⊢ ¬Eq.{u_1 + 1} (α := Orientation ℝ E (Fin 0))
      (rayOfNeZero ℝ (-(AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) ⋯ :
        Ray ℝ (E [⋀^Fin 0]→ₗ[ℝ] ℝ))
      (rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) ⋯ :
        Ray ℝ (E [⋀^Fin 0]→ₗ[ℝ] ℝ))

Tactic:
rw [ray_eq_iff, SameRay.sameRay_comm]

Premises used: SameRay.sameRay_comm, ray_eq_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
h :
  SameRay.{0, u_1} ℝ (M := E [⋀^Fin 0]→ₗ[ℝ] ℝ)
    ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1 : E [⋀^Fin 0]→ₗ[ℝ] ℝ)
    (-(AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1 : E [⋀^Fin 0]→ₗ[ℝ] ℝ)
⊢ False

Tactic:
simpa using
    congr_arg AlternatingMap.constLinearEquivOfIsEmpty.symm (eq_zero_of_sameRay_self_neg h)

Premises used: LinearEquiv.symm, congr_arg, eq_zero_of_sameRay_self_neg, DFunLike.coe, AlternatingMap.constLinearEquivOfIsEmpty
-- 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
hb : b.toBasis.orientation = o
zero :
  ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)) (b : OrthonormalBasis (Fin 0) ℝ E)
    (hb : b.toBasis.orientation = o), o.volumeForm = b.toBasis.det
succ :
  ∀ (n : ℕ) [_i : Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1)))
    (b : OrthonormalBasis (Fin (n + 1)) ℝ E) (hb : b.toBasis.orientation = o), o.volumeForm = b.toBasis.det
⊢ o.volumeForm = b.toBasis.det

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
hb : b.toBasis.orientation = o
⊢ o = positiveOrientation

Tactic:
have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_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
hb : b.toBasis.orientation = o
this : o = positiveOrientation
zero :
  Nat.casesAuxOn (motive := fun (a : ℕ) ↦ (h : 0 = a) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun (h : Eq (α := ℕ) 0 0) ↦
        ⋯.by_cases (fun (x : o = positiveOrientation) ↦ AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
          fun (x : o = -positiveOrientation) ↦ -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun (n : ℕ) (h : 0 = n + 1) ↦
        Eq.rec (motive := fun (x : ℕ) (x_1 : n + 1 = x) ↦
          [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) ↦
            (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det)
          ⋯ o)
      ⋯ =
    b.toBasis.det
zero₁ :
  Nat.casesAuxOn (motive := fun (a : ℕ) ↦ (h : 0 = a) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun (h : Eq (α := ℕ) 0 0) ↦
        if h : o = positiveOrientation then AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun (n : ℕ) (h : 0 = n + 1) ↦
        Eq.rec (motive := fun (x : ℕ) (x_1 : n + 1 = x) ↦
          [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) ↦
            (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det)
          ⋯ o)
      ⋯ =
    b.toBasis.det
zero₂ :
  Nat.casesAuxOn (motive := fun (a : ℕ) ↦ (h : 0 = a) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun (h : Eq (α := ℕ) 0 0) ↦ AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun (n : ℕ) (h : 0 = n + 1) ↦
        Eq.rec (motive := fun (x : ℕ) (x_1 : n + 1 = x) ↦
          [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) ↦
            (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det)
          ⋯ o)
      ⋯ =
    b.toBasis.det
zero₃ : AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1 = b.toBasis.det
⊢ o.volumeForm = b.toBasis.det

Tactic:
simp_rw [volumeForm, Or.by_cases, dif_pos this, Nat.rec_zero, Basis.det_isEmpty]

Premises used: Nat.rec_zero, Module.Basis.det_isEmpty, dif_pos, Or.by_cases, Orientation.volumeForm
-- 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
hb : b.toBasis.orientation = o
zero zero₁ zero₂ : ∀ (this : o = positiveOrientation), o.volumeForm = b.toBasis.det
⊢ o.volumeForm = b.toBasis.det

Tactic:
classical
      have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty
      simp_rw [volumeForm, Or.by_cases, dif_pos this, Nat.rec_zero, Basis.det_isEmpty]

Premises used: Nat.rec_zero, Module.Basis.det_isEmpty, Or.by_cases, Orientation.volumeForm
-- 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
hb : b.toBasis.orientation = o
succ :
  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
⊢ o.volumeForm = b.toBasis.det

Tactic:
simp_rw [volumeForm]

Premises used: Orientation.volumeForm
-- 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
hb : b.toBasis.orientation = o
⊢ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.orientation = o

Tactic:
o.finOrthonormalBasis_orientation _ _

Premises used: Orientation.finOrthonormalBasis_orientation
-- 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
hb : b.toBasis.orientation = o
⊢ (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.orientation = o

Tactic:
exact o.finOrthonormalBasis_orientation _ _

Premises used: Orientation.finOrthonormalBasis_orientation
-- 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
hb : b.toBasis.orientation ≠ o
zero :
  ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)) (b : OrthonormalBasis (Fin 0) ℝ E)
    (hb : b.toBasis.orientation ≠ o), o.volumeForm = -b.toBasis.det
succ :
  ∀ (n : ℕ) [_i : Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1)))
    (b : OrthonormalBasis (Fin (n + 1)) ℝ E) (hb : b.toBasis.orientation ≠ o), o.volumeForm = -b.toBasis.det
⊢ o.volumeForm = -b.toBasis.det

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)
b : OrthonormalBasis (Fin 0) ℝ E
hb : b.toBasis.orientation ≠ o
rwa rwa₁ rwa₂ rwa₃ : ∀ (hb : positiveOrientation ≠ o), positiveOrientation ≠ o
⊢ positiveOrientation ≠ o

Tactic:
rwa [b.toBasis.orientation_isEmpty] at hb

Premises used: Module.Basis.orientation_isEmpty, OrthonormalBasis.toBasis
-- 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
hb : b.toBasis.orientation ≠ o
⊢ positiveOrientation ≠ o

Tactic:
have : positiveOrientation ≠ o := by rwa [b.toBasis.orientation_isEmpty] at hb
-- 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
hb : b.toBasis.orientation ≠ o
this : positiveOrientation ≠ o
zero :
  Nat.casesAuxOn (motive := fun (a : ℕ) ↦ (h : 0 = a) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun (h : Eq (α := ℕ) 0 0) ↦
        ⋯.by_cases (fun (x : o = positiveOrientation) ↦ AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
          fun (x : o = -positiveOrientation) ↦ -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun (n : ℕ) (h : 0 = n + 1) ↦
        Eq.rec (motive := fun (x : ℕ) (x_1 : n + 1 = x) ↦
          [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) ↦
            (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det)
          ⋯ o)
      ⋯ =
    -b.toBasis.det
zero₁ :
  Nat.casesAuxOn (motive := fun (a : ℕ) ↦ (h : 0 = a) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun (h : Eq (α := ℕ) 0 0) ↦
        if h : o = positiveOrientation then AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun (n : ℕ) (h : 0 = n + 1) ↦
        Eq.rec (motive := fun (x : ℕ) (x_1 : n + 1 = x) ↦
          [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) ↦
            (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det)
          ⋯ o)
      ⋯ =
    -b.toBasis.det
zero₂ :
  Nat.casesAuxOn (motive := fun (a : ℕ) ↦ (h : 0 = a) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun (h : Eq (α := ℕ) 0 0) ↦ -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun (n : ℕ) (h : 0 = n + 1) ↦
        Eq.rec (motive := fun (x : ℕ) (x_1 : n + 1 = x) ↦
          [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) ↦
            (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det)
          ⋯ o)
      ⋯ =
    -b.toBasis.det
zero₃ : -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1 = -b.toBasis.det
⊢ o.volumeForm = -b.toBasis.det

Tactic:
simp_rw [volumeForm, Or.by_cases, dif_neg this.symm, Nat.rec_zero, Basis.det_isEmpty]

Premises used: Nat.rec_zero, Module.Basis.det_isEmpty, Ne.symm, dif_neg, Or.by_cases, Orientation.volumeForm
-- 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
hb : b.toBasis.orientation ≠ o
have : positiveOrientation ≠ o
zero : ∀ (this : positiveOrientation ≠ o), o.volumeForm = -b.toBasis.det
have₁ : positiveOrientation ≠ o
zero₁ zero₂ : ∀ (this : positiveOrientation ≠ o), o.volumeForm = -b.toBasis.det
⊢ o.volumeForm = -b.toBasis.det

Tactic:
classical
      have : positiveOrientation ≠ o := by rwa [b.toBasis.orientation_isEmpty] at hb
      simp_rw [volumeForm, Or.by_cases, dif_neg this.symm, Nat.rec_zero, Basis.det_isEmpty]

Premises used: Nat.rec_zero, Module.Basis.det_isEmpty, Or.by_cases, Orientation.volumeForm
-- 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
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
succ :
  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
⊢ o.volumeForm = -b.toBasis.det

Tactic:
simp_rw [volumeForm]

Premises used: Orientation.volumeForm
-- 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
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
succ : Ne (α := Orientation ℝ E (Fin n.succ)) e.toBasis.orientation b.toBasis.orientation
⊢ 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

Tactic:
apply e.det_eq_neg_det_of_opposite_orientation b

Premises used: OrthonormalBasis.det_eq_neg_det_of_opposite_orientation
-- 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
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ o ≠ b.toBasis.orientation

Tactic:
hb.symm

Premises used: Ne.symm
-- 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
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h : e.toBasis.orientation = o
⊢ Ne (α := Orientation ℝ E (Fin n.succ)) e.toBasis.orientation b.toBasis.orientation

Tactic:
convert! hb.symm

Premises used: Ne.symm
-- 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
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ e.toBasis.orientation = o

Tactic:
o.finOrthonormalBasis_orientation _ _

Premises used: Orientation.finOrthonormalBasis_orientation
-- 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
hb : b.toBasis.orientation ≠ o
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ e.toBasis.orientation = o

Tactic:
exact o.finOrthonormalBasis_orientation _ _

Premises used: Orientation.finOrthonormalBasis_orientation
-- 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)
zero : ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)), (-o).volumeForm = -o.volumeForm
succ : ∀ (n : ℕ) [_i : Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))), (-o).volumeForm = -o.volumeForm
⊢ (-o).volumeForm = -o.volumeForm

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)
⊢ (-o).volumeForm = -o.volumeForm

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)
zero : o = positiveOrientation → (-o).volumeForm = -o.volumeForm
zero₁ : o = -positiveOrientation → (-o).volumeForm = -o.volumeForm
⊢ (-o).volumeForm = -o.volumeForm

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)
⊢ Eq.{u_1 + 1} (α := E [⋀^Fin 0]→ₗ[ℝ] ℝ) (volumeForm (-positiveOrientation)) (-volumeForm positiveOrientation)

Tactic:
simp [volumeForm_zero_neg]

Premises used: Orientation.volumeForm_zero_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
zero : Eq (α := E [⋀^Fin 0]→ₗ[ℝ] ℝ) (volumeForm (- -positiveOrientation)) (AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
⊢ Eq.{u_1 + 1} (α := E [⋀^Fin 0]→ₗ[ℝ] ℝ) (volumeForm (- -positiveOrientation)) (-volumeForm (-positiveOrientation))

Tactic:
simp [volumeForm_zero_neg]

Premises used: Orientation.volumeForm_zero_neg
-- 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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ e.toBasis.orientation = o

Tactic:
have h₁ : e.toBasis.orientation = o := o.finOrthonormalBasis_orientation _ _
-- 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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
symm : -o ≠ e.toBasis.orientation
⊢ e.toBasis.orientation ≠ -o

Tactic:
symm
-- 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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
rw : -o = -e.toBasis.orientation
rw₁ rw₂ : -o = -o
⊢ -o ≠ e.toBasis.orientation

Tactic:
rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]

Premises used: Module.Basis.orientation_ne_iff_eq_neg, OrthonormalBasis.toBasis
-- 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))
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
h₁ : e.toBasis.orientation = o
⊢ e.toBasis.orientation ≠ -o

Tactic:
have h₂ : e.toBasis.orientation ≠ -o := by
    symm
    rw [e.toBasis.orientation_ne_iff_eq_neg, 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))
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
succ₁ succ₂ : -e.toBasis.det = -e.toBasis.det
⊢ (-o).volumeForm = -o.volumeForm

Tactic:
rw [o.volumeForm_robust e h₁, (-o).volumeForm_robust_neg e h₂]

Premises used: Orientation.volumeForm_robust_neg, Orientation.volumeForm_robust, Neg.neg