awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜) +
          HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) -
        HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜)) =
    4⁻¹ *
      (-I *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) -
              HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) +
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)))

Tactic:
linear_combination (- 𝓚 ‖(I : 𝕜) • x - y‖ ^ 2 + 𝓚 ‖(I : 𝕜) • x + y‖ ^ 2) * hI' / 4
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
r : 𝕜
x y : E
rw :
  (↑((re : (a : 𝕜) → ℝ) r) : 𝕜) * inner_ 𝕜 x y + (↑((im : (a : 𝕜) → ℝ) r) : 𝕜) * (-I * inner_ 𝕜 x y) =
    ((↑((re : (a : 𝕜) → ℝ) r) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) r) : 𝕜) (-I)) * inner_ 𝕜 x y
⊢ inner_ 𝕜 (r • x) y = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) (inner_ 𝕜 x y)

Tactic:
rw [← re_add_im r, add_smul, add_left, real_prop _ x, ← smul_smul, real_prop _ _ y, I_prop,
    map_add, map_mul, conj_ofReal, conj_ofReal, conj_I]

Premises used: RCLike.re_add_im, _private.0.InnerProductSpaceable.real_prop, RCLike.conj_ofReal, smul_smul, map_add, map_mul, InnerProductSpaceable.add_left, add_smul, RCLike.conj_I, _private.0.InnerProductSpaceable.I_prop
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ (↑((re : (a : 𝕜) → ℝ) r) : 𝕜) * inner_ 𝕜 x y + (↑((im : (a : 𝕜) → ℝ) r) : 𝕜) * (-I * inner_ 𝕜 x y) =
    ((↑((re : (a : 𝕜) → ℝ) r) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) r) : 𝕜) (-I)) * inner_ 𝕜 x y

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
⊢ Nonempty (InnerProductSpace 𝕜 E)

Tactic:
⟨{  inner := inner_ 𝕜
      norm_sq_eq_re_inner := inner_.norm_sq
      conj_inner_symm := inner_.conj_symm
      add_left := add_left
      smul_left := fun _ _ _ => innerProp _ _ _ }⟩

Premises used: InnerProductSpaceable.inner_.norm_sq, Nonempty.intro, InnerProductSpace.mk, InnerProductSpaceable.add_left, InnerProductSpaceable.innerProp, InnerProductSpaceable.inner_.conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
inst_4 : NormedSpace ℝ E
intro : ∀ (val : InnerProductSpace ℝ E), UniformConvexSpace E
⊢ UniformConvexSpace E

Tactic:
cases nonempty_innerProductSpace ℝ E

Premises used: Real, nonempty_innerProductSpace
-- Module: Mathlib.Analysis.InnerProductSpace.OfNorm
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
inst_4 : NormedSpace ℝ E
val : InnerProductSpace ℝ E
⊢ UniformConvexSpace E

Tactic:
infer_instance
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
apply : ¬Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ)
⊢ Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (1 : ℝ)

Tactic:
apply (e.det_to_matrix_orthonormalBasis_real f).resolve_right

Premises used: Or.resolve_right, OrthonormalBasis.det_to_matrix_orthonormalBasis_real
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ LT.lt (α := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f.toBasis : (a : ι) → E) : ℝ)

Tactic:
rw [e.toBasis.orientation_eq_iff_det_pos] at h

Premises used: Module.Basis.orientation_eq_iff_det_pos, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : LT.lt (α := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f.toBasis : (a : ι) → E) : ℝ)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ)

Tactic:
simpa using h
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ LT.lt (α := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ)

Tactic:
have : 0 < e.toBasis.det f := by
    rw [e.toBasis.orientation_eq_iff_det_pos] at h
    simpa using h
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
this : LT.lt (α := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ)
linarith :
  Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ) →
    -1 + HSub.hSub (α := ℝ) (β := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) +
        HSub.hSub (α := ℝ) (β := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ) =
      0
⊢ ¬Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ)

Tactic:
linarith
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Ne (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
contrapose! :
  ∀ (h : Ne (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ)),
    Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ)

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Ne (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ)
⊢ Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation

Tactic:
simp [e.toBasis.orientation_eq_iff_det_pos,
    (e.det_to_matrix_orthonormalBasis_real f).resolve_right h]

Premises used: Module.Basis.orientation_eq_iff_det_pos, Or.resolve_right, OrthonormalBasis.det_to_matrix_orthonormalBasis_real, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
mp : e.toBasis.det = f.toBasis.det → Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
mpr : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation → e.toBasis.det = f.toBasis.det
⊢ e.toBasis.det = f.toBasis.det ↔ Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.det = f.toBasis.det
⊢ Eq (α := Orientation ℝ E ι) (rayOfNeZero ℝ e.toBasis.det ⋯) (rayOfNeZero ℝ f.toBasis.det ⋯)

Tactic:
congr
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
mpr :
  HSMul.hSMul (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f.toBasis : (a : ι) → E) : ℝ) f.toBasis.det = f.toBasis.det
⊢ e.toBasis.det = f.toBasis.det

Tactic:
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]

Premises used: Module.Basis.det, AlternatingMap.eq_smul_basis_det, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ HSMul.hSMul (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f.toBasis : (a : ι) → E) : ℝ) f.toBasis.det = f.toBasis.det

Tactic:
simp [e.det_to_matrix_orthonormalBasis_of_same_orientation f h]

Premises used: OrthonormalBasis.det_to_matrix_orthonormalBasis_of_same_orientation
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Ne (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
rw :
  HSMul.hSMul (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f.toBasis : (a : ι) → E) : ℝ) f.toBasis.det = -f.toBasis.det
⊢ e.toBasis.det = -f.toBasis.det

Tactic:
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]

Premises used: Module.Basis.det, AlternatingMap.eq_smul_basis_det, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Ne (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
simp : HSMul.hSMul (α := ℝ) (-1) f.toBasis.det = -f.toBasis.det
⊢ HSMul.hSMul (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f.toBasis : (a : ι) → E) : ℝ) f.toBasis.det = -f.toBasis.det

Tactic:
simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h]

Premises used: OrthonormalBasis.det_to_matrix_orthonormalBasis_of_opposite_orientation
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
apply :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := E) ((e.toBasis.adjustToOrientation x : (a : ι) → E) i : E) ((e : (a : ι) → E) i : E) ∨
      Eq.{u_1 + 1} (α := E) ((e.toBasis.adjustToOrientation x : (a : ι) → E) i : E) (-(e : (a : ι) → E) i : E)
⊢ Orthonormal.{0, u_1, u_2} ℝ (E := E) (ι := ι) (⇑(e.toBasis.adjustToOrientation x) : (a : ι) → E)

Tactic:
apply e.orthonormal.orthonormal_of_forall_eq_or_eq_neg

Premises used: OrthonormalBasis.orthonormal, Orthonormal.orthonormal_of_forall_eq_or_eq_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
⊢ ∀ (i : ι),
    Eq.{u_1 + 1} (α := E) ((e.toBasis.adjustToOrientation x : (a : ι) → E) i : E) ((e : (a : ι) → E) i : E) ∨
      Eq.{u_1 + 1} (α := E) ((e.toBasis.adjustToOrientation x : (a : ι) → E) i : E) (-(e : (a : ι) → E) i : E)

Tactic:
simpa using e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x

Premises used: Module.Basis.adjustToOrientation_apply_eq_or_eq_neg, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
⊢ (e.adjustToOrientation x).toBasis = e.toBasis.adjustToOrientation x

Tactic:
(e.toBasis.adjustToOrientation x).toBasis_toOrthonormalBasis _

Premises used: Module.Basis.adjustToOrientation, Module.Basis.toBasis_toOrthonormalBasis, OrthonormalBasis.adjustToOrientation, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
rw : (e.toBasis.adjustToOrientation x).orientation = x
⊢ (e.adjustToOrientation x).toBasis.orientation = x

Tactic:
rw [e.toBasis_adjustToOrientation]

Premises used: OrthonormalBasis.toBasis_adjustToOrientation
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
⊢ (e.toBasis.adjustToOrientation x).orientation = x

Tactic:
e.toBasis.orientation_adjustToOrientation x

Premises used: Module.Basis.orientation_adjustToOrientation, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
⊢ (e.toBasis.adjustToOrientation x).orientation = x

Tactic:
exact e.toBasis.orientation_adjustToOrientation x

Premises used: Module.Basis.orientation_adjustToOrientation, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
i : ι
⊢ Eq.{u_1 + 1} (α := E) ((e.adjustToOrientation x : (a : ι) → E) i : E) ((e : (a : ι) → E) i : E) ∨
    Eq.{u_1 + 1} (α := E) ((e.adjustToOrientation x : (a : ι) → E) i : E) (-(e : (a : ι) → E) i : E)

Tactic:
simpa [← e.toBasis_adjustToOrientation] using
    e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x i

Premises used: OrthonormalBasis.toBasis_adjustToOrientation, Module.Basis.adjustToOrientation_apply_eq_or_eq_neg, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
⊢ (e.adjustToOrientation x).toBasis.det = e.toBasis.det ∨ (e.adjustToOrientation x).toBasis.det = -e.toBasis.det

Tactic:
simpa using e.toBasis.det_adjustToOrientation x

Premises used: Module.Basis.det_adjustToOrientation, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
v : ι → E
⊢ Eq (α := ℝ) (|((e.adjustToOrientation x).toBasis.det : (a : ι → E) → ℝ) v| : ℝ)
    (|(e.toBasis.det : (a : ι → E) → ℝ) v| : ℝ)

Tactic:
simp [toBasis_adjustToOrientation]

Premises used: OrthonormalBasis.toBasis_adjustToOrientation
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
⊢ Nonempty (Fin n)

Tactic:
haveI := Fin.pos_iff_nonempty.1 hn
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ FiniteDimensional ℝ E

Tactic:
haveI : FiniteDimensional ℝ E := .of_finrank_pos <| h.symm ▸ hn
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this_1 : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ OrthonormalBasis (Fin n) ℝ E

Tactic:
exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <| finCongr h).adjustToOrientation x

Premises used: OrthonormalBasis.reindex, finCongr, OrthonormalBasis.adjustToOrientation, stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this_1 : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x

Tactic:
((@stdOrthonormalBasis _ _ _ _ _ this).reindex <|
    finCongr h).orientation_adjustToOrientation x

Premises used: OrthonormalBasis.reindex, finCongr, OrthonormalBasis.orientation_adjustToOrientation, stdOrthonormalBasis, Orientation.finOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.Orientation
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this_1 : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x

Tactic:
exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <|
    finCongr h).orientation_adjustToOrientation x

Premises used: OrthonormalBasis.reindex, finCongr, OrthonormalBasis.orientation_adjustToOrientation, stdOrthonormalBasis
-- 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)
opos : E [⋀^Fin 0]→ₗ[ℝ] ℝ := AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
⊢ E [⋀^Fin 0]→ₗ[ℝ] ℝ

Tactic:
exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos

Premises used: Or.by_cases, Orientation.eq_or_eq_neg_of_isEmpty, Neg.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 [⋀^Fin (n + 1)]→ₗ[ℝ] ℝ

Tactic:
exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det

Premises used: Module.Basis.det, Nat.succ_pos, Fact.out, OrthonormalBasis.toBasis, Orientation.finOrthonormalBasis
-- 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)) → E [⋀^Fin 0]→ₗ[ℝ] ℝ
succ : (n : ℕ) → [_i : Fact (finrank ℝ E = n + 1)] → (o : Orientation ℝ E (Fin (n + 1))) → E [⋀^Fin (n + 1)]→ₗ[ℝ] ℝ
⊢ E [⋀^Fin n]→ₗ[ℝ] ℝ

Tactic:
cases n with
    | zero =>
      let opos : E [⋀^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
      exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
    | succ n => exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det

Premises used: Module.Basis.det, Nat.succ_pos, OrthonormalBasis.toBasis, Orientation.finOrthonormalBasis
-- 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)) → E [⋀^Fin 0]→ₗ[ℝ] ℝ
succ : (n : ℕ) → [_i : Fact (finrank ℝ E = n + 1)] → (o : Orientation ℝ E (Fin (n + 1))) → E [⋀^Fin (n + 1)]→ₗ[ℝ] ℝ
⊢ E [⋀^Fin n]→ₗ[ℝ] ℝ

Tactic:
classical
    cases n with
    | zero =>
      let opos : E [⋀^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
      exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
    | succ n => exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det

Premises used: Module.Basis.det, Nat.succ_pos, OrthonormalBasis.toBasis, Orientation.finOrthonormalBasis
-- 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)
    ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1)

Tactic:
simp [volumeForm, Or.by_cases]

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

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

Premises used: Or.by_cases, Module.Oriented.positiveOrientation, Orientation.volumeForm