awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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
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‖
⊢ Eq (α := ℝ) (∏ x : Fin n.succ, |⟪(b : (a : Fin n.succ) → E) x, v x⟫|) (∏ i : Fin (n + 1), ‖v i‖)

Tactic:
congr
-- 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))
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
neg : ∀ (i : Fin n.succ), |⟪(b : (a : Fin n.succ) → E) i, v i⟫| = ‖v i‖
⊢ 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:
ext i
-- 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))
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

Tactic:
have hb : b i = ‖v i‖⁻¹ • v i := gramSchmidtOrthonormalBasis_apply_of_orthogonal hdim hv (h i)
-- 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))
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‖
⊢ |⟪(b : (a : Fin n.succ) → E) i, v i⟫| = ‖v i‖

Tactic:
simp only [hb, inner_smul_left, real_inner_self_eq_norm_mul_norm, RCLike.conj_to_real]

Premises used: real_inner_self_eq_norm_mul_norm, RCLike.conj_to_real, inner_smul_left
-- 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))
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‖
neg₁ : 0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)
⊢ |‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)| = ‖v i‖

Tactic:
rw [abs_of_nonneg]

Premises used: abs_of_nonneg
-- 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))
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‖

Tactic:
field
-- 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))
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
⊢ 0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)

Tactic:
positivity
-- 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)
v : OrthonormalBasis (Fin n) ℝ E
⊢ Eq (α := ℝ) (|(o.volumeForm : (a : Fin n → E) → ℝ) (⇑v : (a : Fin n) → E)| : ℝ) (1 : ℝ)

Tactic:
simpa [o.volumeForm_robust' v v] using congr_arg abs v.toBasis.det_self

Premises used: abs, congr_arg, Module.Basis.det_self, Orientation.volumeForm_robust', DFunLike.coe, 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)
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) : ℝ)
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) : ℝ)
⊢ 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) : ℝ)

Tactic:
rcases n with - | n
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
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) : ℝ)

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
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) : ℝ)
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) : ℝ)

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
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 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))
              positiveOrientation) :
          (a : Fin 0 → F) → ℝ)
        x :
      ℝ)
    ((volumeForm positiveOrientation : (a : Fin 0 → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
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)
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))
              (-positiveOrientation)) :
          (a : Fin 0 → F) → ℝ)
        x :
      ℝ)
    ((volumeForm (-positiveOrientation) : (a : Fin 0 → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
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
⊢ e.toBasis.orientation = o

Tactic:
have he : e.toBasis.orientation = o :=
    o.finOrthonormalBasis_orientation n.succ_pos Fact.out
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
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
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)
⊢ 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:
rw [← he]
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
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))
      e.toBasis.orientation)

Tactic:
e.toBasis.orientation_map φ.toLinearEquiv

Premises used: Module.Basis.ofEquivFun, LinearEquiv.symm, LinearIsometryEquiv.toLinearEquiv, Module.Basis.map, LinearEquiv.toEquiv, LinearMap.inverse, LinearEquiv.trans, Module.Basis.orientation_map, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
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))
      e.toBasis.orientation)

Tactic:
exact e.toBasis.orientation_map φ.toLinearEquiv

Premises used: LinearIsometryEquiv.toLinearEquiv, Module.Basis.orientation_map, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
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)

Tactic:
have heφ : (e.map φ).toBasis.orientation = Orientation.map (Fin n.succ) φ.toLinearEquiv o := by
    rw [← he]
    exact e.toBasis.orientation_map φ.toLinearEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
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)
succ :
  Eq (α := ℝ) (((e.map φ).toBasis.det : (a : Fin (n + 1) → F) → ℝ) x : ℝ)
    ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)
⊢ 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:
rw [(Orientation.map (Fin n.succ) φ.toLinearEquiv o).volumeForm_robust (e.map φ) heφ]

Premises used: LinearIsometryEquiv.toLinearEquiv, Orientation.volumeForm_robust, OrthonormalBasis.map, Orientation.map, Fin, Nat.succ, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
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)
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) : ℝ)
⊢ 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 [o.volumeForm_robust e he]

Premises used: Orientation.volumeForm_robust
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
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 : ℝ)
    ((e.toBasis.det : (a : Fin (n + 1) → E) → ℝ) ((⇑φ.symm : (a : F) → E) ∘ x) : ℝ)

Tactic:
simp
-- 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)
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
x : Fin n → E
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 : ℝ)
succ :
  ∀ (n : ℕ) [_i : Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) (x : Fin (n + 1) → E),
    Eq (α := ℝ) ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
      ((o.volumeForm : (a : Fin (n + 1) → E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin n → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin n → E) → ℝ) x : ℝ)

Tactic:
rcases n with - | n
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
_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:
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
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
x : Fin 0 → E
zero :
  o = positiveOrientation →
    Eq (α := ℝ) ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
      ((o.volumeForm : (a : Fin 0 → E) → ℝ) x : ℝ)
zero₁ :
  o = -positiveOrientation →
    Eq (α := ℝ) ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
      ((o.volumeForm : (a : Fin 0 → E) → ℝ) x : ℝ)
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((o.volumeForm : (a : Fin 0 → E) → ℝ) x : ℝ)

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
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
_i : Fact (finrank ℝ E = 0)
x : Fin 0 → E
⊢ Eq (α := ℝ) ((volumeForm positiveOrientation : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((volumeForm positiveOrientation : (a : Fin 0 → E) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
_i : Fact (finrank ℝ E = 0)
x : Fin 0 → E
⊢ Eq (α := ℝ) ((volumeForm (-positiveOrientation) : (a : Fin 0 → E) → ℝ) ((⇑φ : (a : E) → E) ∘ x) : ℝ)
    ((volumeForm (-positiveOrientation) : (a : Fin 0 → E) → ℝ) x : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : E →ₗ[ℝ] E) → ℝ) (↑φ.toLinearEquiv : E →ₗ[ℝ] E) : ℝ)
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
x : Fin (n + 1) → E
⊢ FiniteDimensional ℝ E

Tactic:
have : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n