-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem volumeForm_zero_neg [_i : Fact (finrank ℝ E = 0)] :
    Orientation.volumeForm (-positiveOrientation : Orientation ℝ E (Fin 0)) =
      -AlternatingMap.constLinearEquivOfIsEmpty 1

Proof state:
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
h : SameRay ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) (-AlternatingMap.constLinearEquivOfIsEmpty 1)
⊢ False

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

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ Nat.casesAuxOn (motive := fun a => 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h =>
        if hp :
            -rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ =
              rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ then
          AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (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) ⋯
          (-rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯))
      ⋯ =
    -AlternatingMap.constLinearEquivOfIsEmpty 1

Tactic:
apply if_neg

Result:
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ ¬-rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ =
      rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯

Proof state:
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ ¬SameRay ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) (-AlternatingMap.constLinearEquivOfIsEmpty 1)

Tactic:
intro h

Result:
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
h : SameRay ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) (-AlternatingMap.constLinearEquivOfIsEmpty 1)
⊢ False

Proof state:
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ ¬-rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ =
      rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯

Tactic:
simp only [neg_rayOfNeZero]

Result:
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ ¬rayOfNeZero ℝ (-AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ =
      rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯

Proof state:
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ ¬rayOfNeZero ℝ (-AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ =
      rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯

Tactic:
rw [ray_eq_iff, SameRay.sameRay_comm]

Result:
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ ¬SameRay ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) (-AlternatingMap.constLinearEquivOfIsEmpty 1)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ (-positiveOrientation).volumeForm = -AlternatingMap.constLinearEquivOfIsEmpty 1

Tactic:
simp_rw [volumeForm, Or.by_cases, positiveOrientation]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ Nat.casesAuxOn (motive := fun a => 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun h =>
        if hp :
            -rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ =
              rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ then
          AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (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) ⋯
          (-rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯))
      ⋯ =
    -AlternatingMap.constLinearEquivOfIsEmpty 1