awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ Eq.{u_1 + 1} (α := R) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) : R)
    (((⇑(↑f : M [⋀^ι]→ₗ[R] R →ₗ[R] R) : (a : M [⋀^ι]→ₗ[R] R) → R) ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1])
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, ⋯⟩) :
      R)

Tactic:
simp [f]
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ Eq.{u_1 + 1} (α := R) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) : R)
    (((⇑(↑f : M [⋀^ι]→ₗ[R] R →ₗ[R] R) : (a : M [⋀^ι]→ₗ[R] R) → R) ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1])
        ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨1, ⋯⟩) :
      R)

Tactic:
simp [f]
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
⊢ LinearIndependent R (M := R) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] : Fin (Nat.succ 0).succ → R)

Tactic:
have H : LinearIndependent R ![f x, 1] := by
    convert! h.map' f.toLinearMap f.ker
    ext i
    fin_cases i <;> simp [f]
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H : LinearIndependent R (M := R) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] : Fin (Nat.succ 0).succ → R)
⊢ ∀ (s : Finset (Fin (Nat.succ 0).succ)) (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_1 + 1} (α := R) (∑ i ∈ s, HSMul.hSMul (β := R) (g i) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] i : R)) 0 →
      ∀ i ∈ s, g i = 0

Tactic:
rw [linearIndependent_iff'] at H

Premises used: linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H :
  ∀ (s : Finset (Fin (Nat.succ 0).succ)) (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_1 + 1} (α := R) (∑ i ∈ s, HSMul.hSMul (β := R) (g i) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] i : R)) 0 →
      ∀ i ∈ s, g i = 0
⊢ Eq.{u_1 + 1} (α := R)
    (∑ i : Fin (Nat.succ 0).succ,
      HSMul.hSMul (α := R) (β := R) (![1, -(f : (a : M [⋀^ι]→ₗ[R] R) → R) x] i : R)
        (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] i : R))
    0

Tactic:
simp [Fin.sum_univ_succ]

Premises used: Fin.sum_univ_succ
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H :
  ∀ (s : Finset (Fin (Nat.succ 0).succ)) (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_1 + 1} (α := R) (∑ i ∈ s, HSMul.hSMul (β := R) (g i) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] i : R)) 0 →
      ∀ i ∈ s, g i = 0
⊢ Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constOfIsEmpty R M ι 1]
f : M [⋀^ι]→ₗ[R] R ≃ₗ[R] R := LinearEquiv.symm AlternatingMap.constLinearEquivOfIsEmpty
H :
  ∀ (s : Finset (Fin (Nat.succ 0).succ)) (g : Fin (Nat.succ 0).succ → R),
    Eq.{u_1 + 1} (α := R) (∑ i ∈ s, HSMul.hSMul (β := R) (g i) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] i : R)) 0 →
      ∀ i ∈ s, g i = 0
⊢ False

Tactic:
simpa using H Finset.univ ![1, -f x] (by simp [Fin.sum_univ_succ]) 0 (by simp)

Premises used: Finset.univ, Matrix.vecEmpty, OfNat.ofNat, DFunLike.coe, Matrix.vecCons, Neg.neg
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : IsEmpty ι
o : Orientation R M ι
h :
  ∀ (x : M [⋀^ι]→ₗ[R] R) (hx : x ≠ 0),
    Eq (α := Orientation R M ι) (rayOfNeZero R x hx) positiveOrientation ∨
      Eq (α := Orientation R M ι) (rayOfNeZero R x hx) (-positiveOrientation)
⊢ o = positiveOrientation ∨ o = -positiveOrientation

Tactic:
induction o using Module.Ray.ind with | h x hx =>
  dsimp [positiveOrientation]
  simp only [ray_eq_iff]
  rw [sameRay_or_sameRay_neg_iff_not_linearIndependent]
  intro h
  set f : (M [⋀^ι]→ₗ[R] R) ≃ₗ[R] R := AlternatingMap.constLinearEquivOfIsEmpty.symm
  have H : LinearIndependent R ![f x, 1] := by
    convert! h.map' f.toLinearMap f.ker
    ext i
    fin_cases i <;> simp [f]
  rw [linearIndependent_iff'] at H
  simpa using H Finset.univ ![1, -f x] (by simp [Fin.sum_univ_succ]) 0 (by simp)

Premises used: AlternatingMap, LinearEquiv.symm, linearIndependent_iff', sameRay_or_sameRay_neg_iff_not_linearIndependent, ray_eq_iff, Module.Oriented.positiveOrientation, AlternatingMap.constLinearEquivOfIsEmpty, Module.Ray.ind
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e₁ e₂ : Basis ι R M
rw rw₁ : SameRay R e₁.det e₂.det ↔ SameRay R e₁.det e₂.det
⊢ SameRay R e₁.det e₂.det ↔
    SameRay R (HSMul.hSMul (α := R) ((e₁.det : (a : ι → M) → R) (⇑e₂ : (a : ι) → M) : R) e₂.det) e₂.det

Tactic:
rw [← e₁.det.eq_smul_basis_det e₂]

Premises used: Module.Basis.det, AlternatingMap.eq_smul_basis_det
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ Ne.{u_1 + 1} (α := R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) (0 : R)

Tactic:
rw [← x.map_basis_ne_zero_iff e] at hx

Premises used: AlternatingMap.map_basis_ne_zero_iff
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
x : M [⋀^ι]→ₗ[R] R
hx_1 : x ≠ 0
hx : Ne.{u_1 + 1} (α := R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) (0 : R)
h :
  Eq (α := Orientation R M ι) (rayOfNeZero R x hx_1) (rayOfNeZero R e.det ⋯) ∨
    Eq (α := Orientation R M ι) (rayOfNeZero R x hx_1) (-rayOfNeZero R e.det ⋯)
h₁ : SameRay R x e.det ∨ Eq (α := Orientation R M ι) (rayOfNeZero R x hx_1) (-rayOfNeZero R e.det ⋯)
h₂ : SameRay R x e.det ∨ Eq (α := Orientation R M ι) (rayOfNeZero R x hx_1) (rayOfNeZero R (-e.det) ⋯)
h₃ : SameRay R x e.det ∨ SameRay R x (-e.det)
h₄ :
  SameRay R (HSMul.hSMul (α := R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det) e.det ∨
    SameRay R (HSMul.hSMul (α := R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det) (-e.det)
h₅ :
  SameRay R (HSMul.hSMul (α := R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det) e.det ∨
    LT.lt.{u_1} (α := R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) (0 : R)
h₆ :
  LT.lt.{u_1} (α := R) (0 : R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) ∨
    LT.lt.{u_1} (α := R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) (0 : R)
h₇ : Ne.{u_1 + 1} (α := R) (0 : R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R)
h₈ h₉ h₁₀ h₁₁ : Ne.{u_1 + 1} (α := R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) (0 : R)
⊢ Eq (α := Orientation R M ι) (rayOfNeZero R x hx_1) e.orientation ∨
    Eq (α := Orientation R M ι) (rayOfNeZero R x hx_1) (-e.orientation)

Tactic:
rwa [Basis.orientation, ray_eq_iff, neg_rayOfNeZero, ray_eq_iff, x.eq_smul_basis_det e,
    sameRay_neg_smul_left_iff_of_ne e.det_ne_zero hx, sameRay_smul_left_iff_of_ne e.det_ne_zero hx,
    lt_or_lt_iff_ne, ne_comm]

Premises used: sameRay_smul_left_iff_of_ne, neg_rayOfNeZero, Module.Basis.orientation, sameRay_neg_smul_left_iff_of_ne, AlternatingMap.eq_smul_basis_det, ne_comm, ray_eq_iff, Module.Basis.det_ne_zero, lt_or_lt_iff_ne
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
x : Orientation R M ι
h :
  ∀ (x : M [⋀^ι]→ₗ[R] R) (hx : x ≠ 0),
    Eq (α := Orientation R M ι) (rayOfNeZero R x hx) e.orientation ∨
      Eq (α := Orientation R M ι) (rayOfNeZero R x hx) (-e.orientation)
⊢ x = e.orientation ∨ x = -e.orientation

Tactic:
induction x using Module.Ray.ind with | h x hx =>
  rw [← x.map_basis_ne_zero_iff e] at hx
  rwa [Basis.orientation, ray_eq_iff, neg_rayOfNeZero, ray_eq_iff, x.eq_smul_basis_det e,
    sameRay_neg_smul_left_iff_of_ne e.det_ne_zero hx, sameRay_smul_left_iff_of_ne e.det_ne_zero hx,
    lt_or_lt_iff_ne, ne_comm]

Premises used: neg_rayOfNeZero, Module.Basis.orientation, ne_comm, ray_eq_iff, lt_or_lt_iff_ne, Module.Ray.ind
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
x : Orientation R M ι
⊢ x ≠ e.orientation ↔ x = -e.orientation

Tactic:
⟨fun h => (e.orientation_eq_or_eq_neg x).resolve_left h, fun h =>
    h.symm ▸ (Module.Ray.ne_neg_self e.orientation).symm⟩

Premises used: Eq.rec, Module.Basis.orientation_eq_or_eq_neg, Or.resolve_left, Ne.symm, Module.Basis.orientation, Module.Ray.ne_neg_self, Iff.intro, Eq.symm
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] M
rw :
  Eq (α := Orientation R M ι)
      ((Orientation.map ι f : (a : Orientation R M ι) → Orientation R M ι) e.orientation : Orientation R M ι)
      (e.orientation : Orientation R M ι) ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
rw₁ :
  HSMul.hSMul (α := Rˣ) (β := Orientation R M ι) (((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f)⁻¹ : Rˣ) e.orientation =
      e.orientation ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
rw₂ :
  HSMul.hSMul (α := Rˣ) (β := Ray R (M [⋀^ι]→ₗ[R] R)) ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ) e.orientation =
      e.orientation ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
rw₃ :
  LT.lt.{u_1} (α := R) 0 (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
rw₄ rw₅ :
  LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
⊢ Eq (α := Orientation R M ι) (e.map f).orientation e.orientation ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)

Tactic:
rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_self_iff,
    LinearEquiv.coe_det]

Premises used: units_inv_smul, units_smul_eq_self_iff, Module.Basis.map_orientation_eq_det_inv_smul, Module.Basis.orientation_map, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] M
rw :
  Eq (α := Orientation R M ι)
      ((Orientation.map ι f : (a : Orientation R M ι) → Orientation R M ι) e.orientation : Orientation R M ι)
      (-e.orientation : Orientation R M ι) ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
rw₁ :
  HSMul.hSMul (α := Rˣ) (β := Orientation R M ι) (((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f)⁻¹ : Rˣ) e.orientation =
      -e.orientation ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
rw₂ :
  HSMul.hSMul (α := Rˣ) (β := Ray R (M [⋀^ι]→ₗ[R] R)) ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ) e.orientation =
      -e.orientation ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
rw₃ :
  LT.lt.{u_1} (α := R) (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) 0 ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
rw₄ rw₅ :
  LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R) ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
⊢ Eq (α := Orientation R M ι) (e.map f).orientation (-e.orientation) ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)

Tactic:
rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_neg_iff,
    LinearEquiv.coe_det]

Premises used: units_inv_smul, units_smul_eq_neg_iff, Module.Basis.map_orientation_eq_det_inv_smul, Module.Basis.orientation_map, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
i : ι
rw :
  HSMul.hSMul (β := Orientation R M ι) (HMul.hMul (α := Rˣ) (-1) (∏ x ∈ Finset.univ \ {i}, 1 x))⁻¹ e.orientation =
    -e.orientation
⊢ Eq (α := Orientation R M ι) (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 i (-1))).orientation
    (-e.orientation)

Tactic:
rw [orientation_unitsSMul, Finset.prod_update_of_mem (Finset.mem_univ _)]

Premises used: Finset.mem_univ, Module.Basis.orientation_unitsSMul, Finset.prod_update_of_mem
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
i : ι
⊢ HSMul.hSMul (β := Orientation R M ι) (HMul.hMul (α := Rˣ) (-1) (∏ x ∈ Finset.univ \ {i}, 1 x))⁻¹ e.orientation =
    -e.orientation

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
pos : ∀ (h : e.orientation = x), e.orientation = x
neg :
  ∀ (h : ¬e.orientation = x),
    (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).orientation = x
⊢ (if e.orientation = x then e
      else e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).orientation =
    x

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : e.orientation = x
⊢ e.orientation = x

Tactic:
h
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : e.orientation = x
⊢ e.orientation = x

Tactic:
exact h
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
neg : e.orientation ≠ x
⊢ (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).orientation = x

Tactic:
rw [orientation_neg_single, eq_comm, ← orientation_ne_iff_eq_neg, ne_comm]

Premises used: Module.Basis.orientation_ne_iff_eq_neg, eq_comm, ne_comm, Module.Basis.orientation_neg_single
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
⊢ e.orientation ≠ x

Tactic:
h
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
⊢ e.orientation ≠ x

Tactic:
exact h
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
rw :
  Eq.{u_2 + 1} (α := M)
      ((if e.orientation = x then e
            else e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) :
            (a : ι) → M)
          i :
        M)
      ((e : (a : ι) → M) i : M) ∨
    Eq.{u_2 + 1} (α := M)
      ((if e.orientation = x then e
            else e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) :
            (a : ι) → M)
          i :
        M)
      (-(e : (a : ι) → M) i : M)
⊢ Eq.{u_2 + 1} (α := M) ((e.adjustToOrientation x : (a : ι) → M) i : M) ((e : (a : ι) → M) i : M) ∨
    Eq.{u_2 + 1} (α := M) ((e.adjustToOrientation x : (a : ι) → M) i : M) (-(e : (a : ι) → M) i : M)

Tactic:
rw [adjustToOrientation]

Premises used: Module.Basis.adjustToOrientation
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
pos :
  ∀ (h : e.orientation = x),
    Eq.{u_2 + 1} (α := M) ((e : (a : ι) → M) i : M) ((e : (a : ι) → M) i : M) ∨
      Eq.{u_2 + 1} (α := M) ((e : (a : ι) → M) i : M) (-(e : (a : ι) → M) i : M)
neg :
  ∀ (h : ¬e.orientation = x),
    Eq.{u_2 + 1} (α := M)
        ((e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) : (a : ι) → M) i : M)
        ((e : (a : ι) → M) i : M) ∨
      Eq.{u_2 + 1} (α := M)
        ((e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) : (a : ι) → M) i : M)
        (-(e : (a : ι) → M) i : M)
⊢ Eq.{u_2 + 1} (α := M)
      ((if e.orientation = x then e
            else e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) :
            (a : ι) → M)
          i :
        M)
      ((e : (a : ι) → M) i : M) ∨
    Eq.{u_2 + 1} (α := M)
      ((if e.orientation = x then e
            else e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) :
            (a : ι) → M)
          i :
        M)
      (-(e : (a : ι) → M) i : M)

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : e.orientation = x
⊢ Eq.{u_2 + 1} (α := M) ((e : (a : ι) → M) i : M) ((e : (a : ι) → M) i : M) ∨
    Eq.{u_2 + 1} (α := M) ((e : (a : ι) → M) i : M) (-(e : (a : ι) → M) i : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : ¬e.orientation = x
pos :
  ∀ (hi : i = Classical.arbitrary ι),
    Eq.{u_2 + 1} (α := M)
        ((e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) : (a : ι) → M) i : M)
        ((e : (a : ι) → M) i : M) ∨
      Eq.{u_2 + 1} (α := M)
        ((e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) : (a : ι) → M) i : M)
        (-(e : (a : ι) → M) i : M)
neg :
  ∀ (hi : ¬i = Classical.arbitrary ι),
    Eq.{u_2 + 1} (α := M)
        ((e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) : (a : ι) → M) i : M)
        ((e : (a : ι) → M) i : M) ∨
      Eq.{u_2 + 1} (α := M)
        ((e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) : (a : ι) → M) i : M)
        (-(e : (a : ι) → M) i : M)
⊢ Eq.{u_2 + 1} (α := M)
      ((e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) : (a : ι) → M) i : M)
      ((e : (a : ι) → M) i : M) ∨
    Eq.{u_2 + 1} (α := M)
      ((e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) : (a : ι) → M) i : M)
      (-(e : (a : ι) → M) i : M)

Tactic:
by_cases hi : i = Classical.arbitrary ι

Premises used: Classical.arbitrary
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_3
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
i : ι
h : ¬e.orientation = x
hi : i = Classical.arbitrary ι
⊢ Eq.{u_2 + 1} (α := M)
      ((e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) : (a : ι) → M) i : M)
      ((e : (a : ι) → M) i : M) ∨
    Eq.{u_2 + 1} (α := M)
      ((e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1)) : (a : ι) → M) i : M)
      (-(e : (a : ι) → M) i : M)

Tactic:
simp [unitsSMul_apply, hi]

Premises used: Module.Basis.unitsSMul_apply