-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem volumeForm_robust (b : OrthonormalBasis (Fin n) ℝ E) (hb : b.toBasis.orientation = o) :
    o.volumeForm = b.toBasis.det

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
⊢ o.volumeForm = b.toBasis.det

Tactic:
simp_rw [volumeForm]

Result:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
⊢ Nat.casesAuxOn (motive := fun a => n✝ + 1 = a → E [⋀^Fin (n✝ + 1)]→ₗ[ℝ] ℝ) (n✝ + 1)
      (fun h =>
        Eq.rec (motive := fun x x_1 => [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = 0)] o =>
            ⋯.by_cases (fun x => AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) fun x =>
              -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
          ⋯ o)
      (fun n h =>
        Eq.rec (motive := fun x x_1 => [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o => (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o)
      ⋯ =
    b.toBasis.det

Proof state:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
⊢ o.volumeForm = b.toBasis.det

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

Result:
no goals

Proof state:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_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

Tactic:
have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty

Result:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
⊢ o.volumeForm = b.toBasis.det

Proof state:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_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

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]

Result:
no goals

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
⊢ Nat.casesAuxOn (motive := fun a => n✝ + 1 = a → E [⋀^Fin (n✝ + 1)]→ₗ[ℝ] ℝ) (n✝ + 1)
      (fun h =>
        Eq.rec (motive := fun x x_1 => [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = 0)] o =>
            ⋯.by_cases (fun x => AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) fun x =>
              -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
          ⋯ o)
      (fun n h =>
        Eq.rec (motive := fun x x_1 => [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] o => (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ o)
      ⋯ =
    b.toBasis.det

Tactic:
rw [same_orientation_iff_det_eq_det, hb]

Result:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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 _ _

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
b : OrthonormalBasis (Fin n) ℝ E
hb : b.toBasis.orientation = o
⊢ o.volumeForm = b.toBasis.det

Tactic:
cases n

Result:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_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

case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
⊢ o.volumeForm = b.toBasis.det