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))
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⟫ : ℝ)
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin (n + 1) → E) → ℝ) v| : ℝ) (∏ i : Fin (n + 1), ‖v i‖ : ℝ)
have succ : Eq (α := ℝ) (∏ 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
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⟫ : ℝ)
⊢ Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
have 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‖)
Tactic: by_cases! h : ∃ i, v i = 0
-- 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
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‖)
⊢ Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
have 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‖)
Tactic: by_cases! h : ∃ i, v i = 0
-- 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
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
⊢ Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
have 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‖)
Tactic: obtain ⟨i, hi⟩ := h
Cleared hypotheses: 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))
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
⊢ Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
have pos : ‖v i‖ = 0
Tactic: rw [Finset.prod_eq_zero (Finset.mem_univ i), Finset.prod_eq_zero (Finset.mem_univ 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 + 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
⊢ Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
have pos₁ : |⟪(b : (a : Fin n.succ) → E) i, v i⟫| = 0
Tactic: rw [Finset.prod_eq_zero (Finset.mem_univ i), Finset.prod_eq_zero (Finset.mem_univ 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 + 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
⊢ Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)
have neg : Eq (α := Fin n.succ → ℝ) (fun (x : Fin n.succ) ↦ |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) fun (i : Fin (n + 1)) ↦ ‖v i‖
Tactic: congr
-- 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
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
⊢ Eq (α := Fin n.succ → ℝ) (fun (x : Fin n.succ) ↦ |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) fun (i : Fin (n + 1)) ↦ ‖v i‖
have neg : ∀ (i : Fin n.succ), |⟪(b : (a : Fin n.succ) → E) i, v i⟫| = ‖v i‖
Tactic: ext i
-- 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
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
i : Fin n.succ
⊢ |⟪(b : (a : Fin n.succ) → E) i, v i⟫| = ‖v i‖
have hb₁ : (b : (a : Fin n.succ) → E) i = ‖v i‖⁻¹ • v i
Tactic: have hb : b i = ‖v i‖⁻¹ • v i := gramSchmidtOrthonormalBasis_apply_of_orthogonal hdim hv (h 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 + 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_1 :
  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
i : Fin n.succ
hb : (b : (a : Fin n.succ) → E) i = ‖v i‖⁻¹ • v i
⊢ |⟪(b : (a : Fin n.succ) → E) i, v i⟫| = ‖v i‖
have neg : |‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)| = ‖v i‖
Tactic: simp only [hb, inner_smul_left, real_inner_self_eq_norm_mul_norm, RCLike.conj_to_real]
-- 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
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_1 :
  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
i : Fin n.succ
hb : (b : (a : Fin n.succ) → E) i = ‖v i‖⁻¹ • v i
⊢ |‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)| = ‖v i‖
have neg : ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖) = ‖v i‖
Tactic: rw [abs_of_nonneg]
-- 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
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_1 :
  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
i : Fin n.succ
hb : (b : (a : Fin n.succ) → E) i = ‖v i‖⁻¹ • v i
neg : ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖) = ‖v i‖
⊢ |‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)| = ‖v i‖
have neg₁ : 0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)
Tactic: rw [abs_of_nonneg]
-- 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)
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
inst_4 : Fact (finrank ℝ F = n)
φ : E ≃ₗᵢ[ℝ] F
x : Fin n → F
⊢ Eq (α := ℝ)
    ((volumeForm
            (((map (Fin n) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin n)) (Orientation ℝ F (Fin n))) :
                (a : Orientation ℝ E (Fin n)) → Orientation ℝ F (Fin n))
              o) :
          (a : Fin n → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin n → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
have zero : ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)) [inst_5 : Fact (finrank ℝ F = 0)] (x : Fin 0 → F),
  Eq (α := ℝ)
    ((volumeForm
            (((map (Fin 0) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 0)) (Orientation ℝ F (Fin 0))) :
                (a : Orientation ℝ E (Fin 0)) → Orientation ℝ F (Fin 0))
              o) :
          (a : Fin 0 → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
Tactic: rcases n with - | n
Cleared hypotheses: n, _i, o, inst_4, x
-- 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)
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
inst_4 : Fact (finrank ℝ F = n)
φ : E ≃ₗᵢ[ℝ] F
x : Fin n → F
zero :
  ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)) [inst_5 : Fact (finrank ℝ F = 0)] (x : Fin 0 → F),
    Eq (α := ℝ)
      ((volumeForm
              (((map (Fin 0) φ.toLinearEquiv :
                    Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 0)) (Orientation ℝ F (Fin 0))) :
                  (a : Orientation ℝ E (Fin 0)) → Orientation ℝ F (Fin 0))
                o) :
            (a : Fin 0 → F) → ℝ)
          x :
        ℝ)
      ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
⊢ Eq (α := ℝ)
    ((volumeForm
            (((map (Fin n) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin n)) (Orientation ℝ F (Fin n))) :
                (a : Orientation ℝ E (Fin n)) → Orientation ℝ F (Fin n))
              o) :
          (a : Fin n → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin n → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
have succ : ∀ (n : ℕ) [_i : Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) [inst_5 : Fact (finrank ℝ F = n + 1)]
  (x : Fin (n + 1) → F),
  Eq (α := ℝ)
    ((volumeForm
            (((map (Fin (n + 1)) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin (n + 1))) (Orientation ℝ F (Fin (n + 1)))) :
                (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ F (Fin (n + 1)))
              o) :
          (a : Fin (n + 1) → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
Tactic: rcases n with - | n
Cleared hypotheses: n, _i, o, inst_4, x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
inst_4 : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ Eq (α := ℝ)
    ((volumeForm
            (((map (Fin 0) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 0)) (Orientation ℝ F (Fin 0))) :
                (a : Orientation ℝ E (Fin 0)) → Orientation ℝ F (Fin 0))
              o) :
          (a : Fin 0 → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
have zero : o = positiveOrientation →
  Eq (α := ℝ)
    ((volumeForm
            (((map (Fin 0) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 0)) (Orientation ℝ F (Fin 0))) :
                (a : Orientation ℝ E (Fin 0)) → Orientation ℝ F (Fin 0))
              o) :
          (a : Fin 0 → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
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
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
inst_4 : Fact (finrank ℝ F = 0)
x : Fin 0 → F
zero :
  o = positiveOrientation →
    Eq (α := ℝ)
      ((volumeForm
              (((map (Fin 0) φ.toLinearEquiv :
                    Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 0)) (Orientation ℝ F (Fin 0))) :
                  (a : Orientation ℝ E (Fin 0)) → Orientation ℝ F (Fin 0))
                o) :
            (a : Fin 0 → F) → ℝ)
          x :
        ℝ)
      ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
⊢ Eq (α := ℝ)
    ((volumeForm
            (((map (Fin 0) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 0)) (Orientation ℝ F (Fin 0))) :
                (a : Orientation ℝ E (Fin 0)) → Orientation ℝ F (Fin 0))
              o) :
          (a : Fin 0 → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
have zero₁ : o = -positiveOrientation →
  Eq (α := ℝ)
    ((volumeForm
            (((map (Fin 0) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin 0)) (Orientation ℝ F (Fin 0))) :
                (a : Orientation ℝ E (Fin 0)) → Orientation ℝ F (Fin 0))
              o) :
          (a : Fin 0 → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
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
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst_4 : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
⊢ Eq (α := ℝ)
    ((volumeForm
            (((map (Fin (n + 1)) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin (n + 1))) (Orientation ℝ F (Fin (n + 1)))) :
                (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ F (Fin (n + 1)))
              o) :
          (a : Fin (n + 1) → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
have he : e.toBasis.orientation = o
Tactic: have he : e.toBasis.orientation = o :=
    o.finOrthonormalBasis_orientation n.succ_pos Fact.out
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst_4 : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
he : e.toBasis.orientation = o
⊢ Eq (α := Orientation ℝ F (Fin n.succ)) (e.map φ).toBasis.orientation
    (((map (Fin n.succ) φ.toLinearEquiv :
          Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin n.succ)) (Orientation ℝ F (Fin n.succ))) :
        (a : Orientation ℝ E (Fin n.succ)) → Orientation ℝ F (Fin n.succ))
      o)
have rw : Eq (α := Orientation ℝ F (Fin n.succ)) (e.map φ).toBasis.orientation
  (((map (Fin n.succ) φ.toLinearEquiv :
        Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin n.succ)) (Orientation ℝ F (Fin n.succ))) :
      (a : Orientation ℝ E (Fin n.succ)) → Orientation ℝ F (Fin n.succ))
    e.toBasis.orientation)
Tactic: rw [← he]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst_4 : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
he : e.toBasis.orientation = o
⊢ Eq (α := ℝ)
    ((volumeForm
            (((map (Fin (n + 1)) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin (n + 1))) (Orientation ℝ F (Fin (n + 1)))) :
                (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ F (Fin (n + 1)))
              o) :
          (a : Fin (n + 1) → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
have heφ : Eq (α := Orientation ℝ F (Fin n.succ)) (e.map φ).toBasis.orientation
  (((map (Fin n.succ) φ.toLinearEquiv :
        Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin n.succ)) (Orientation ℝ F (Fin n.succ))) :
      (a : Orientation ℝ E (Fin n.succ)) → Orientation ℝ F (Fin n.succ))
    o)
Tactic: have heφ : (e.map φ).toBasis.orientation = Orientation.map (Fin n.succ) φ.toLinearEquiv o := by
    rw [← he]
    exact e.toBasis.orientation_map φ.toLinearEquiv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst_4 : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
he : e.toBasis.orientation = o
heφ :
  Eq (α := Orientation ℝ F (Fin n.succ)) (e.map φ).toBasis.orientation
    (((map (Fin n.succ) φ.toLinearEquiv :
          Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin n.succ)) (Orientation ℝ F (Fin n.succ))) :
        (a : Orientation ℝ E (Fin n.succ)) → Orientation ℝ F (Fin n.succ))
      o)
⊢ Eq (α := ℝ)
    ((volumeForm
            (((map (Fin (n + 1)) φ.toLinearEquiv :
                  Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin (n + 1))) (Orientation ℝ F (Fin (n + 1)))) :
                (a : Orientation ℝ E (Fin (n + 1))) → Orientation ℝ F (Fin (n + 1)))
              o) :
          (a : Fin (n + 1) → F) → ℝ)
        x :
      ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
have succ : Eq (α := ℝ) (((e.map φ).toBasis.det : (a : Fin (n + 1) → F) → ℝ) x : ℝ)
  ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
Tactic: rw [(Orientation.map (Fin n.succ) φ.toLinearEquiv o).volumeForm_robust (e.map φ) heφ]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
inst_4 : Fact (finrank ℝ F = n + 1)
x : Fin (n + 1) → F
e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o
he : e.toBasis.orientation = o
heφ :
  Eq (α := Orientation ℝ F (Fin n.succ)) (e.map φ).toBasis.orientation
    (((map (Fin n.succ) φ.toLinearEquiv :
          Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ E (Fin n.succ)) (Orientation ℝ F (Fin n.succ))) :
        (a : Orientation ℝ E (Fin n.succ)) → Orientation ℝ F (Fin n.succ))
      o)
⊢ Eq (α := ℝ) (((e.map φ).toBasis.det : (a : Fin (n + 1) → F) → ℝ) x : ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
have succ : Eq (α := ℝ) (((e.map φ).toBasis.det : (a : Fin (n + 1) → F) → ℝ) x : ℝ)
  ((e.toBasis.det : (a : Fin (n + 1) → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
Tactic: rw [o.volumeForm_robust e he]
-- 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)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x : Fin n → E
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin n → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin n → E) → ℝ) x : ℝ)
have zero : ∀ [_i : Fact (finrank ℝ E = 0)] (o : Orientation ℝ E (Fin 0)) (x : Fin 0 → E),
  Eq (α := ℝ) ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) x : ℝ)
Tactic: rcases n with - | n
Cleared hypotheses: n, _i, o, x