awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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)
⊢ Eq (α := Orientation R M ι) (rayOfNeZero R x hx_1) e.orientation ∨
    Eq (α := Orientation R M ι) (rayOfNeZero R x hx_1) (-e.orientation)
have h₇ : Ne.{u_1 + 1} (α := R) (0 : R) ((x : (a : ι → M) → R) (⇑e : (a : ι) → M) : R)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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
have 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)
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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
⊢ 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)
have 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)
Tactic: rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_self_iff,
    LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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)
⊢ 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)
have 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)
Tactic: rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_self_iff,
    LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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)
⊢ 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)
have 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)
Tactic: rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_self_iff,
    LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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)
⊢ 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)
have 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)
Tactic: rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_self_iff,
    LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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)
⊢ 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)
have 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)
Tactic: rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_self_iff,
    LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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
⊢ 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)
have 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)
Tactic: rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_neg_iff,
    LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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)
⊢ 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)
have 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)
Tactic: rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_neg_iff,
    LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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)
⊢ 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)
have 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)
Tactic: rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_neg_iff,
    LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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)
⊢ 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)
have 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)
Tactic: rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_neg_iff,
    LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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)
⊢ 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)
have 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)
Tactic: rw [orientation_map, e.map_orientation_eq_det_inv_smul, units_inv_smul, units_smul_eq_neg_iff,
    LinearEquiv.coe_det]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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 : ι
⊢ Eq (α := Orientation R M ι) (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 i (-1))).orientation
    (-e.orientation)
have rw : HSMul.hSMul (β := Orientation R M ι) (HMul.hMul (α := Rˣ) (-1) (∏ x ∈ Finset.univ \ {i}, 1 x))⁻¹ e.orientation =
  -e.orientation
Tactic: rw [orientation_unitsSMul, Finset.prod_update_of_mem (Finset.mem_univ _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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 ι
⊢ (if e.orientation = x then e
      else e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).orientation =
    x
have pos : ∀ (h : e.orientation = x), e.orientation = x
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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
⊢ (if e.orientation = x then e
      else e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).orientation =
    x
have neg : ∀ (h : ¬e.orientation = x),
  (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).orientation = x
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).orientation = x
have neg : e.orientation ≠ x
Tactic: rw [orientation_neg_single, eq_comm, ← orientation_ne_iff_eq_neg, ne_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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 : ι
⊢ 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)
have 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)
Tactic: rw [adjustToOrientation]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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 : ι
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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.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)
have 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)
Tactic: by_cases hi : i = Classical.arbitrary ι