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 : 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
-- 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 : e.orientation = x → e.det = e.det ∨ e.det = -e.det
neg :
  ¬e.orientation = x →
    (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det = e.det ∨
      (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det = -e.det
⊢ (if e.orientation = x then e
        else e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det =
      e.det ∨
    (if e.orientation = x then e
        else e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det =
      -e.det

Tactic:
split_ifs
-- 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
pos : e.det = e.det
⊢ e.det = e.det ∨ e.det = -e.det

Tactic:
left
-- 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.det = e.det

Tactic:
rfl
-- 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.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det = -e.det
⊢ (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det = e.det ∨
    (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det = -e.det

Tactic:
right
-- 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 : HSMul.hSMul (α := R) (-1) e.det = -e.det
⊢ (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det = -e.det

Tactic:
simp only [e.det_unitsSMul, Finset.mem_univ, Finset.prod_update_of_mem,
      Pi.one_apply, Finset.prod_const_one, mul_one, inv_neg, inv_one, Units.val_neg, Units.val_one]

Premises used: Finset.mem_univ, inv_one, Pi.one_apply, Module.Basis.det_unitsSMul, inv_neg, Finset.prod_const_one, Units.val_neg, Units.val_one, mul_one, 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 ι
inst_7 : Nonempty ι
e : Basis ι R M
x : Orientation R M ι
h : ¬e.orientation = x
neg :
  ∀ (x : ι → M),
    Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (α := R) (-1) e.det : (a : ι → M) → R) x : R) ((-e.det : (a : ι → M) → R) x : R)
⊢ HSMul.hSMul (α := R) (-1) e.det = -e.det

Tactic:
ext
-- 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
x_1 : ι → M
⊢ Eq.{u_1 + 1} (α := R) ((HSMul.hSMul (α := R) (-1) e.det : (a : ι → M) → R) x_1 : R)
    ((-e.det : (a : ι → M) → R) x_1 : R)

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 ι
v : ι → M
inl :
  ∀ (h : (e.adjustToOrientation x).det = e.det),
    Eq.{u_1 + 1} (α := R) (|((e.adjustToOrientation x).det : (a : ι → M) → R) v| : R)
      (|(e.det : (a : ι → M) → R) v| : R)
inr :
  ∀ (h : (e.adjustToOrientation x).det = -e.det),
    Eq.{u_1 + 1} (α := R) (|((e.adjustToOrientation x).det : (a : ι → M) → R) v| : R)
      (|(e.det : (a : ι → M) → R) v| : R)
⊢ Eq.{u_1 + 1} (α := R) (|((e.adjustToOrientation x).det : (a : ι → M) → R) v| : R) (|(e.det : (a : ι → M) → R) v| : R)

Tactic:
rcases e.det_adjustToOrientation x with h | h

Premises used: Module.Basis.det_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 ι
v : ι → M
h : (e.adjustToOrientation x).det = e.det
⊢ Eq.{u_1 + 1} (α := R) (|((e.adjustToOrientation x).det : (a : ι → M) → R) v| : R) (|(e.det : (a : ι → M) → R) v| : R)

Tactic:
simp [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 ι
v : ι → M
h : (e.adjustToOrientation x).det = -e.det
⊢ Eq.{u_1 + 1} (α := R) (|((e.adjustToOrientation x).det : (a : ι → M) → R) v| : R) (|(e.det : (a : ι → M) → R) v| : R)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
have : ∀ (e : Basis ι R M), x₁ = x₂ ∨ x₁ = -x₂
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
have e := (finBasis R M).reindex (Fintype.equivFinOfCardEq h).symm
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
inl : ∀ (h₁ : x₁ = e.orientation), x₁ = x₂ ∨ x₁ = -x₂
inr : ∀ (h₁ : x₁ = -e.orientation), x₁ = x₂ ∨ x₁ = -x₂
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
rcases e.orientation_eq_or_eq_neg x₁ with (h₁ | h₁)

Premises used: Module.Basis.orientation_eq_or_eq_neg
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = e.orientation
inl : ∀ (h₂ : x₂ = e.orientation), x₁ = x₂ ∨ x₁ = -x₂
inl₁ : ∀ (h₂ : x₂ = -e.orientation), x₁ = x₂ ∨ x₁ = -x₂
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂)

Premises used: Module.Basis.orientation_eq_or_eq_neg
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = -e.orientation
inr : ∀ (h₂ : x₂ = e.orientation), x₁ = x₂ ∨ x₁ = -x₂
inr₁ : ∀ (h₂ : x₂ = -e.orientation), x₁ = x₂ ∨ x₁ = -x₂
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂)

Premises used: Module.Basis.orientation_eq_or_eq_neg
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = e.orientation
h₂ : x₂ = e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = e.orientation
h₂ : x₂ = -e.orientation
inl :
  Eq (α := Orientation R M ι) e.orientation (-e.orientation) ∨
    Eq (α := Orientation R M ι) e.orientation (- -e.orientation)
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = -e.orientation
h₂ : x₂ = e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
h₁ : x₁ = -e.orientation
h₂ : x₂ = -e.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
⊢ x₁ ≠ x₂ ↔ x₁ = -x₂

Tactic:
⟨fun hn => (eq_or_eq_neg x₁ x₂ h).resolve_left hn, fun he =>
    he.symm ▸ (Module.Ray.ne_neg_self x₂).symm⟩

Premises used: Orientation.eq_or_eq_neg, Eq.rec, Or.resolve_left, Ne.symm, Module.Ray.ne_neg_self, Iff.intro, Eq.symm
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x =
    HSMul.hSMul (α := Rˣ) (((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f)⁻¹ : Rˣ) x

Tactic:
haveI e := (finBasis R M).reindex (Fintype.equivFinOfCardEq h).symm
  e.map_orientation_eq_det_inv_smul x f

Premises used: Fintype.equivFinOfCardEq, Module.finBasis, Module.Basis.map_orientation_eq_det_inv_smul, Module.Basis.reindex, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
inl :
  IsEmpty ι →
    ((map ι f : (a : Orientation R M ι) → Orientation R M ι) x = x ↔
      LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R))
inr :
  Nonempty ι →
    ((map ι f : (a : Orientation R M ι) → Orientation R M ι) x = x ↔
      LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R))
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x = x ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : IsEmpty ι
⊢ finrank R M = 0

Tactic:
have H : finrank R M = 0 := h.symm.trans Fintype.card_eq_zero
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : IsEmpty ι
H : finrank R M = 0
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x = x ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)

Tactic:
simp [LinearMap.det_eq_one_of_finrank_eq_zero H]

Premises used: LinearMap.det_eq_one_of_finrank_eq_zero
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : FiniteDimensional R M
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : Nonempty ι
inr :
  HSMul.hSMul (α := Rˣ) (((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f)⁻¹ : Rˣ) x = x ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
inr₁ :
  HSMul.hSMul (α := Rˣ) ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ) x = x ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
inr₂ :
  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)
inr₃ inr₄ :
  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)
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x = x ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)

Tactic:
rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_self_iff, LinearEquiv.coe_det]

Premises used: units_inv_smul, units_smul_eq_self_iff, Orientation.map_eq_det_inv_smul, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
inl :
  IsEmpty ι →
    ((map ι f : (a : Orientation R M ι) → Orientation R M ι) x = -x ↔
      LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R))
inr :
  Nonempty ι →
    ((map ι f : (a : Orientation R M ι) → Orientation R M ι) x = -x ↔
      LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R))
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : IsEmpty ι
⊢ finrank R M = 0

Tactic:
have H : finrank R M = 0 := h.symm.trans Fintype.card_eq_zero
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : IsEmpty ι
H : finrank R M = 0
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)

Tactic:
simp [LinearMap.det_eq_one_of_finrank_eq_zero H, Module.Ray.ne_neg_self x]

Premises used: Module.Ray.ne_neg_self, LinearMap.det_eq_one_of_finrank_eq_zero
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : Nonempty ι
rw : 0 < Fintype.card ι
⊢ 0 < finrank R M

Tactic:
rw [← h]
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : Nonempty ι
⊢ 0 < Fintype.card ι

Tactic:
Fintype.card_pos

Premises used: Fintype.card_pos
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : Nonempty ι
⊢ 0 < Fintype.card ι

Tactic:
exact Fintype.card_pos

Premises used: Fintype.card_pos
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : Nonempty ι
⊢ 0 < finrank R M

Tactic:
have H : 0 < finrank R M := by
    rw [← h]
    exact Fintype.card_pos
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : Nonempty ι
H : 0 < finrank R M
⊢ FiniteDimensional R M

Tactic:
haveI : FiniteDimensional R M := of_finrank_pos H
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h : Fintype.card ι = finrank R M
h_1 : Nonempty ι
H : 0 < finrank R M
this : FiniteDimensional R M
inr :
  HSMul.hSMul (α := Rˣ) (((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f)⁻¹ : Rˣ) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
inr₁ :
  HSMul.hSMul (α := Rˣ) ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)
inr₂ :
  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)
inr₃ inr₄ :
  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)
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x = -x ↔
    LT.lt.{u_1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R) (0 : R)

Tactic:
rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_neg_iff, LinearEquiv.coe_det]

Premises used: units_inv_smul, units_smul_eq_neg_iff, Orientation.map_eq_det_inv_smul, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : Field 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 : Nonempty ι
inst_7 : DecidableEq ι
inst_8 : FiniteDimensional R M
x : Orientation R M ι
h : Fintype.card ι = finrank R M
⊢ (x.someBasis h).orientation = x

Tactic:
Basis.orientation_adjustToOrientation _ _

Premises used: Module.Basis.orientation_adjustToOrientation, Orientation.someBasis
-- Module: Mathlib.LinearAlgebra.PID
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Module.Free R M
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) p ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
obtain :
  ∀ (n : ℕ) (snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n),
    Eq.{u_1 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (f.restrict hf') : R)
      ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (f.restrict hf') : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
obtain ⟨n, snf⟩ := p.smithNormalForm (Module.Free.chooseBasis R M)

Premises used: Submodule.smithNormalForm, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.PID
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : Module.Free R M
inst_5 : IsDomain R
inst_6 : IsPrincipalIdealRing R
p : Submodule R M
f : M →ₗ[R] M
hf : ∀ (x : M), Membership.mem (α := M) p ((f : (a : M) → M) x : M)
hf' : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
ι : Type u_2 := Module.Free.ChooseBasisIndex R M
n : ℕ
snf : Module.Basis.SmithNormalForm p (Module.Free.ChooseBasisIndex R M) n
rw :
  Eq.{u_1 + 1} (α := R)
    (Matrix.trace (n := Fin n)
      ((toMatrix snf.bN snf.bN : (a : ↥p →ₗ[R] ↥p) → Matrix (Fin n) (Fin n) R) (f.restrict hf')))
    (Matrix.trace.{u_2, u_1} (n := Module.Free.ChooseBasisIndex R M)
      ((toMatrix snf.bM snf.bM :
          (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
        f))
⊢ Eq.{u_1 + 1} (α := R) ((trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) (f.restrict hf') : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
rw [trace_eq_matrix_trace R snf.bM, trace_eq_matrix_trace R snf.bN]

Premises used: LinearMap.trace_eq_matrix_trace, Module.Basis.SmithNormalForm.bM, Module.Basis.SmithNormalForm.bN