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 ι
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)
⊢ 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 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)
Tactic: by_cases hi : i = Classical.arbitrary ι
-- 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))).det =
      e.det ∨
    (if e.orientation = x then e
        else e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det =
      -e.det
have pos : e.orientation = x → e.det = e.det ∨ e.det = -e.det
Tactic: split_ifs
-- 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 : e.orientation = x → e.det = e.det ∨ e.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
have 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
Tactic: split_ifs
-- 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.det = e.det ∨ e.det = -e.det
have pos : e.det = e.det
Tactic: left
-- 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))).det = e.det ∨
    (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det = -e.det
have neg : (e.unitsSMul (Function.update (β := fun (a : ι) ↦ Rˣ) 1 (Classical.arbitrary ι) (-1))).det = -e.det
Tactic: right
-- 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))).det = -e.det
have neg : HSMul.hSMul (α := R) (-1) e.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]
-- 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
⊢ HSMul.hSMul (α := R) (-1) e.det = -e.det
have 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)
Tactic: ext
-- 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 ι
v : ι → M
⊢ Eq.{u_1 + 1} (α := R) (|((e.adjustToOrientation x).det : (a : ι → M) → R) v| : R) (|(e.det : (a : ι → M) → R) v| : R)
have 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)
Tactic: rcases e.det_adjustToOrientation x with h | 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 ι
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)
⊢ Eq.{u_1 + 1} (α := R) (|((e.adjustToOrientation x).det : (a : ι → M) → R) v| : R) (|(e.det : (a : ι → M) → R) v| : R)
have 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)
Tactic: rcases e.det_adjustToOrientation x with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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₂
have have : ∀ (e : Basis ι R M), x₁ = x₂ ∨ x₁ = -x₂
Tactic: have e := (finBasis R M).reindex (Fintype.equivFinOfCardEq h).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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 ι
⊢ x₁ = x₂ ∨ x₁ = -x₂
have inl : ∀ (h₁ : x₁ = e.orientation), x₁ = x₂ ∨ x₁ = -x₂
Tactic: rcases e.orientation_eq_or_eq_neg x₁ with (h₁ | h₁)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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₂
⊢ x₁ = x₂ ∨ x₁ = -x₂
have inr : ∀ (h₁ : x₁ = -e.orientation), x₁ = x₂ ∨ x₁ = -x₂
Tactic: rcases e.orientation_eq_or_eq_neg x₁ with (h₁ | h₁)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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
⊢ x₁ = x₂ ∨ x₁ = -x₂
have inl : ∀ (h₂ : x₂ = e.orientation), x₁ = x₂ ∨ x₁ = -x₂
Tactic: rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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₂
⊢ x₁ = x₂ ∨ x₁ = -x₂
have inl₁ : ∀ (h₂ : x₂ = -e.orientation), x₁ = x₂ ∨ x₁ = -x₂
Tactic: rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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
⊢ x₁ = x₂ ∨ x₁ = -x₂
have inr : ∀ (h₂ : x₂ = e.orientation), x₁ = x₂ ∨ x₁ = -x₂
Tactic: rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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₂
⊢ x₁ = x₂ ∨ x₁ = -x₂
have inr₁ : ∀ (h₂ : x₂ = -e.orientation), x₁ = x₂ ∨ x₁ = -x₂
Tactic: rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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₂
have inl : Eq (α := Orientation R M ι) e.orientation (-e.orientation) ∨
  Eq (α := Orientation R M ι) e.orientation (- -e.orientation)
Tactic: simp [h₁, h₂]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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 = x ↔
    LT.lt.{u_1} (α := R) (0 : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
have 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))
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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))
⊢ (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)
have 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))
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (hypothesis)
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 ι
⊢ (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)
have H : finrank R M = 0
Tactic: have H : finrank R M = 0 := h.symm.trans Fintype.card_eq_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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 ι
⊢ (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)
have 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)
Tactic: rw [map_eq_det_inv_smul _ _ h, 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 : 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)
⊢ (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)
have 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)
Tactic: rw [map_eq_det_inv_smul _ _ h, 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 : 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)
⊢ (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)
have 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)
Tactic: rw [map_eq_det_inv_smul _ _ h, 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 : 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)
⊢ (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)
have 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)
Tactic: rw [map_eq_det_inv_smul _ _ h, 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 : 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
⊢ (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)
have 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))
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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))
⊢ (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)
have 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))
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (hypothesis)
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 ι
⊢ (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)
have H : finrank R M = 0
Tactic: have H : finrank R M = 0 := h.symm.trans Fintype.card_eq_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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
have rw : 0 < Fintype.card ι
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (hypothesis)
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 ι
⊢ (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)
have H : 0 < finrank R M
Tactic: have H : 0 < finrank R M := by
    rw [← h]
    exact Fintype.card_pos
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (hypothesis)
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
⊢ (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)
have this : FiniteDimensional R M
Tactic: haveI : FiniteDimensional R M := of_finrank_pos H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Orientation (goal)
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
⊢ (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)
have 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)
Tactic: rw [map_eq_det_inv_smul _ _ h, 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 : 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)
⊢ (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)
have 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)
Tactic: rw [map_eq_det_inv_smul _ _ h, units_inv_smul, units_smul_eq_neg_iff, LinearEquiv.coe_det]