awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : Type u_8
inst_5 : AddCommMonoid N
inst_6 : Module R N
a : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (x : ι₁) ↦ N) N₁
b : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (x : ι₂) ↦ N) N₂
⊢ (domCoprod' :
        (a : MultilinearMap R (fun (x : ι₁) ↦ N) N₁ ⊗[R] MultilinearMap R (fun (x : ι₂) ↦ N) N₂) →
          MultilinearMap R (fun (x : ι₁ ⊕ ι₂) ↦ N) (N₁ ⊗[R] N₂))
      (a ⊗ₜ[R] b) =
    a.domCoprod b

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MultilinearMap.domCoprod, List.foldl, MultilinearMap.domCoprodDep, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct
Goal:
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst : CommSemiring R
N₁ : Type u_6
inst_1 : AddCommMonoid N₁
inst_2 : Module R N₁
N₂ : Type u_7
inst_3 : AddCommMonoid N₂
inst_4 : Module R N₂
N : Type u_8
inst_5 : AddCommMonoid N
inst_6 : Module R N
a : MultilinearMap.{u_1, u_2, u_8, u_6} R (fun (x : ι₁) ↦ N) N₁
b : MultilinearMap.{u_1, u_3, u_8, u_7} R (fun (x : ι₂) ↦ N) N₂
σa : ι₁ ≃ ι₃
σb : ι₂ ≃ ι₄
⊢ domDomCongr (σa.sumCongr σb) (a.domCoprod b) = (domDomCongr σa a).domCoprod (domDomCongr σb b)

Tactic:
rfl

Premises used: Sum.map, MultilinearMap.domCoprod, MultilinearMap.domDomCongr, TensorProduct.tmul, MultilinearMap.domCoprodDep, AddCon.toQuotient, rfl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
ι : Type u_4
e : M ≃ₗ[R] N
v : M [⋀^ι]→ₗ[R] R
hv : v ≠ 0
⊢ Eq (α := Orientation R N ι)
    ((map ι e : (a : Orientation R M ι) → Orientation R N ι) (rayOfNeZero R v hv) : Orientation R N ι)
    (rayOfNeZero R (v.compLinearMap (↑e.symm : N →ₗ[R] M)) ⋯ : Ray R (N [⋀^ι]→ₗ[R] R))

Tactic:
rfl

Premises used: rayOfNeZero, Quot.map, AlternatingMap.compLinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
rw :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (AlternatingMap.domLCongr R R ι R (LinearEquiv.refl R M)))
    (Equiv.refl (Orientation R M ι))
rw₁ :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (LinearEquiv.refl R (M [⋀^ι]→ₗ[R] R)))
    (Equiv.refl (Orientation R M ι))
rw₂ rw₃ :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Equiv.refl (Ray R (M [⋀^ι]→ₗ[R] R))) (Equiv.refl (Orientation R M ι))
⊢ Eq (α := Orientation R M ι ≃ Orientation R M ι) (map ι (LinearEquiv.refl R M)) (Equiv.refl (Orientation R M ι))

Tactic:
rw [Orientation.map, AlternatingMap.domLCongr_refl, Module.Ray.map_refl]

Premises used: AlternatingMap.domLCongr_refl, Module.Ray.map_refl, Orientation.map
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
ι : Type u_4
e : M ≃ₗ[R] N
⊢ Eq (α := Orientation R N ι ≃ Orientation R M ι) (Equiv.symm (map ι e)) (map ι e.symm)

Tactic:
rfl

Premises used: Module.Ray, Module.Ray.map, Quotient, Quot.map, Quotient.congr, Orientation.map, Quot.congr, Equiv.symm, AlternatingMap.compLinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
ι' : Type u_5
e : ι ≃ ι'
v : M [⋀^ι]→ₗ[R] R
hv : v ≠ 0
⊢ Eq (α := Orientation R M ι')
    ((reindex R M e : (a : Orientation R M ι) → Orientation R M ι') (rayOfNeZero R v hv) : Orientation R M ι')
    (rayOfNeZero R (AlternatingMap.domDomCongr e v) ⋯ : Ray R (M [⋀^ι']→ₗ[R] R))

Tactic:
rfl

Premises used: rayOfNeZero, AlternatingMap.domDomCongr, Quot.map, rfl
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
rw :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (AlternatingMap.domDomCongrₗ R (Equiv.refl ι)))
    (Equiv.refl (Orientation R M ι))
rw₁ :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Ray.map (LinearEquiv.refl R (M [⋀^ι]→ₗ[R] R)))
    (Equiv.refl (Orientation R M ι))
rw₂ rw₃ :
  Eq (α := Orientation R M ι ≃ Orientation R M ι) (Equiv.refl (Ray R (M [⋀^ι]→ₗ[R] R))) (Equiv.refl (Orientation R M ι))
⊢ Eq (α := Orientation R M ι ≃ Orientation R M ι) (reindex R M (Equiv.refl ι)) (Equiv.refl (Orientation R M ι))

Tactic:
rw [Orientation.reindex, AlternatingMap.domDomCongrₗ_refl, Module.Ray.map_refl]

Premises used: AlternatingMap.domDomCongrₗ_refl, Module.Ray.map_refl, Orientation.reindex
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
ι' : Type u_5
e : ι ≃ ι'
⊢ Eq (α := Orientation R M ι' ≃ Orientation R M ι) (Equiv.symm (reindex R M e)) (reindex R M e.symm)

Tactic:
rfl

Premises used: Module.Ray, Module.Ray.map, AlternatingMap.domDomCongr, Quotient, Orientation.reindex, Quot.map, Quotient.congr, Quot.congr, Equiv.symm, rfl
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
ι : Type u_4
ι' : Type u_5
inst_7 : IsEmpty ι
⊢ Ne.{u_1 + 1} (α := R) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
ι : Type u_4
ι' : Type u_5
inst_7 : IsEmpty ι
⊢ Ne.{u_1 + 1} (α := R) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
N : Type u_3
inst_5 : AddCommMonoid N
inst_6 : Module R N
ι : Type u_4
inst_7 : IsEmpty ι
f : M ≃ₗ[R] N
⊢ Eq (α := Orientation R N ι)
    ((map ι f : (a : Orientation R M ι) → Orientation R N ι) positiveOrientation : Orientation R N ι)
    (positiveOrientation : Orientation R N ι)

Tactic:
rfl

Premises used: rayOfNeZero, AlternatingMap.constOfIsEmpty, MultilinearMap.compLinearMap, Quot.map, AlternatingMap.compLinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
h : Eq (α := Orientation R M ι) (rayOfNeZero R (g.compLinearMap (↑f.symm : M →ₗ[R] M)) ⋯) (rayOfNeZero R g hg)
⊢ Eq (α := Orientation R M ι)
    ((map ι f : (a : Orientation R M ι) → Orientation R M ι) (rayOfNeZero R g hg) : Orientation R M ι)
    (rayOfNeZero R g hg : Ray R (M [⋀^ι]→ₗ[R] R))

Tactic:
rw [Orientation.map_apply]

Premises used: Orientation.map_apply
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
h : g.compLinearMap (↑f.symm : M →ₗ[R] M) = g
⊢ Eq (α := Orientation R M ι) (rayOfNeZero R (g.compLinearMap (↑f.symm : M →ₗ[R] M)) ⋯) (rayOfNeZero R g hg)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
h :
  ∀ (i : ι → M),
    Eq.{u_1 + 1} (α := R) ((g.compLinearMap (↑f.symm : M →ₗ[R] M) : (a : ι → M) → R) i : R)
      ((g : (a : ι → M) → R) i : R)
⊢ g.compLinearMap (↑f.symm : M →ₗ[R] M) = g

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
h :
  Eq.{u_1 + 1} (α := R) ((g : (a : ι → M) → R) fun (i_1 : ι) ↦ ((↑f.symm : M →ₗ[R] M) : (a : M) → M) (i i_1) : R)
    ((g : (a : ι → M) → R) i : R)
⊢ Eq.{u_1 + 1} (α := R) ((g.compLinearMap (↑f.symm : M →ₗ[R] M) : (a : ι → M) → R) i : R) ((g : (a : ι → M) → R) i : R)

Tactic:
rw [AlternatingMap.compLinearMap_apply]

Premises used: AlternatingMap.compLinearMap_apply
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
h : (fun (i_1 : ι) ↦ ((↑f.symm : M →ₗ[R] M) : (a : M) → M) (i i_1)) = i
⊢ Eq.{u_1 + 1} (α := R) ((g : (a : ι → M) → R) fun (i_1 : ι) ↦ ((↑f.symm : M →ₗ[R] M) : (a : M) → M) (i i_1) : R)
    ((g : (a : ι → M) → R) i : R)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
f : M ≃ₗ[R] M
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
i : ι → M
⊢ (fun (i_1 : ι) ↦ ((↑f.symm : M →ₗ[R] M) : (a : M) → M) (i i_1)) = i

Tactic:
simp only [LinearEquiv.coe_coe, eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommMonoid M
inst_4 : Module R M
ι : Type u_4
inst_5 : IsEmpty ι
x : Orientation R M ι
f : M ≃ₗ[R] M
h :
  ∀ (g : M [⋀^ι]→ₗ[R] R) (hg : g ≠ 0),
    Eq (α := Orientation R M ι)
      ((map ι f : (a : Orientation R M ι) → Orientation R M ι) (rayOfNeZero R g hg) : Orientation R M ι)
      (rayOfNeZero R g hg : Ray R (M [⋀^ι]→ₗ[R] R))
⊢ (map ι f : (a : Orientation R M ι) → Orientation R M ι) x = x

Tactic:
induction x using Module.Ray.ind with | h g hg =>
  rw [Orientation.map_apply]
  congr
  ext i
  rw [AlternatingMap.compLinearMap_apply]
  congr
  simp only [LinearEquiv.coe_coe, eq_iff_true_of_subsingleton]

Premises used: Orientation.map_apply, AlternatingMap.compLinearMap_apply, eq_iff_true_of_subsingleton, Module.Ray.ind, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
N : Type u_3
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
ι : Type u_4
f : M ≃ₗ[R] N
x : Orientation R M ι
⊢ Eq (α := Orientation R N ι) ((map ι f : (a : Orientation R M ι) → Orientation R N ι) (-x) : Orientation R N ι)
    (-(map ι f : (a : Orientation R M ι) → Orientation R N ι) x : Orientation R N ι)

Tactic:
Module.Ray.map_neg _ x

Premises used: Module.Ray.map_neg
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_4
ι' : Type u_5
e : ι ≃ ι'
x : Orientation R M ι
⊢ Eq (α := Orientation R M ι')
    ((reindex R M e : (a : Orientation R M ι) → Orientation R M ι') (-x) : Orientation R M ι')
    (-(reindex R M e : (a : Orientation R M ι) → Orientation R M ι') x : Orientation R M ι')

Tactic:
Module.Ray.map_neg _ x

Premises used: Module.Ray.map_neg
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
N : Type u_3
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
ι : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
e : Basis ι R M
f : M ≃ₗ[R] N
simp_rw :
  Eq (α := Orientation R N ι) (rayOfNeZero R (e.map f).det ⋯)
    ((Orientation.map ι f : (a : Orientation R M ι) → Orientation R N ι) (rayOfNeZero R e.det ⋯))
simp_rw₁ :
  Eq (α := Orientation R N ι) (rayOfNeZero R (e.map f).det ⋯)
    (rayOfNeZero R (e.det.compLinearMap (↑f.symm : N →ₗ[R] M)) ⋯)
⊢ Eq (α := Orientation R N ι) (e.map f).orientation
    ((Orientation.map ι f : (a : Orientation R M ι) → Orientation R N ι) e.orientation)

Tactic:
simp_rw [Basis.orientation, Orientation.map_apply, Basis.det_map']

Premises used: Module.Basis.orientation, Module.Basis.det_map', Orientation.map_apply
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_4
ι' : Type u_5
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : Fintype ι'
inst_8 : DecidableEq ι'
e : Basis ι R M
eι : ι ≃ ι'
simp_rw :
  Eq (α := Orientation R M ι') (rayOfNeZero R (e.reindex eι).det ⋯)
    ((Orientation.reindex R M eι : (a : Orientation R M ι) → Orientation R M ι') (rayOfNeZero R e.det ⋯))
simp_rw₁ :
  Eq (α := Orientation R M ι') (rayOfNeZero R (e.reindex eι).det ⋯)
    (rayOfNeZero R (AlternatingMap.domDomCongr eι e.det) ⋯)
⊢ Eq (α := Orientation R M ι') (e.reindex eι).orientation
    ((Orientation.reindex R M eι : (a : Orientation R M ι) → Orientation R M ι') e.orientation)

Tactic:
simp_rw [Basis.orientation, Orientation.reindex_apply, Basis.det_reindex']

Premises used: Module.Basis.det_reindex', Module.Basis.orientation, Orientation.reindex_apply
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_4
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
rw :
  SameRay R (e.unitsSMul w).det
    (HMul.hMul (α := R) (↑(∏ i : ι, w i)⁻¹ : R) (∏ i : ι, (↑(w i) : R)) • (e.unitsSMul w).det)
⊢ (e.unitsSMul w).orientation = HSMul.hSMul (α := Rˣ) (β := Orientation R M ι) (∏ i : ι, w i)⁻¹ e.orientation

Tactic:
rw [Basis.orientation, Basis.orientation, smul_rayOfNeZero, ray_eq_iff,
    e.det.eq_smul_basis_det (e.unitsSMul w), det_unitsSMul_self, Units.smul_def, smul_smul]

Premises used: smul_rayOfNeZero, Module.Basis.unitsSMul, smul_smul, Module.Basis.orientation, Module.Basis.det, AlternatingMap.eq_smul_basis_det, Units.smul_def, ray_eq_iff, Module.Basis.det_unitsSMul_self
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_4
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
norm_cast :
  SameRay R (e.unitsSMul w).det ((↑(HMul.hMul (α := Rˣ) (∏ i : ι, w i)⁻¹ (∏ i : ι, w i)) : R) • (e.unitsSMul w).det)
⊢ SameRay R (e.unitsSMul w).det
    (HMul.hMul (α := R) (↑(∏ i : ι, w i)⁻¹ : R) (∏ i : ι, (↑(w i) : R)) • (e.unitsSMul w).det)

Tactic:
norm_cast
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_4
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
simp : SameRay R (e.unitsSMul w).det (e.unitsSMul w).det
⊢ SameRay R (e.unitsSMul w).det ((↑(HMul.hMul (α := Rˣ) (∏ i : ι, w i)⁻¹ (∏ i : ι, w i)) : R) • (e.unitsSMul w).det)

Tactic:
simp only [inv_mul_cancel, Units.val_one, one_smul]

Premises used: inv_mul_cancel, one_smul, Units.val_one
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_4
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det (e.unitsSMul w).det

Tactic:
SameRay.rfl

Premises used: SameRay.rfl
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_4
inst_5 : Fintype ι
inst_6 : DecidableEq ι
e : Basis ι R M
w : ι → Rˣ
⊢ SameRay R (e.unitsSMul w).det (e.unitsSMul w).det

Tactic:
exact SameRay.rfl

Premises used: SameRay.rfl
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_4
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : IsEmpty ι
b : Basis ι R M
e_v : b.det = (AlternatingMap.constLinearEquivOfIsEmpty : (a : R) → M [⋀^ι]→ₗ[R] R) 1
⊢ Eq (α := Orientation R M ι) (rayOfNeZero R b.det ⋯) positiveOrientation

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_4
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : IsEmpty ι
b : Basis ι R M
⊢ b.det = (AlternatingMap.constLinearEquivOfIsEmpty : (a : R) → M [⋀^ι]→ₗ[R] R) 1

Tactic:
b.det_isEmpty

Premises used: Module.Basis.det_isEmpty, AlternatingMap.constOfIsEmpty
-- Module: Mathlib.LinearAlgebra.Orientation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
M : Type u_2
inst_3 : AddCommGroup M
inst_4 : Module R M
ι : Type u_4
inst_5 : Fintype ι
inst_6 : DecidableEq ι
inst_7 : IsEmpty ι
b : Basis ι R M
⊢ b.det = (AlternatingMap.constLinearEquivOfIsEmpty : (a : R) → M [⋀^ι]→ₗ[R] R) 1

Tactic:
exact b.det_isEmpty

Premises used: Module.Basis.det_isEmpty
-- 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 :
  Eq (α := Orientation R M ι) (rayOfNeZero R x hx) (rayOfNeZero R (AlternatingMap.constOfIsEmpty R M ι 1) ⋯) ∨
    Eq (α := Orientation R M ι) (rayOfNeZero R x hx) (rayOfNeZero R (-AlternatingMap.constOfIsEmpty R M ι 1) ⋯)
⊢ Eq (α := Orientation R M ι) (rayOfNeZero R x hx) positiveOrientation ∨
    Eq (α := Orientation R M ι) (rayOfNeZero R x hx) (-positiveOrientation)

Tactic:
dsimp [positiveOrientation]

Premises used: Module.Oriented.positiveOrientation
-- 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 : SameRay R x (AlternatingMap.constOfIsEmpty R M ι 1) ∨ SameRay R x (-AlternatingMap.constOfIsEmpty R M ι 1)
⊢ Eq (α := Orientation R M ι) (rayOfNeZero R x hx) (rayOfNeZero R (AlternatingMap.constOfIsEmpty R M ι 1) ⋯) ∨
    Eq (α := Orientation R M ι) (rayOfNeZero R x hx) (rayOfNeZero R (-AlternatingMap.constOfIsEmpty R M ι 1) ⋯)

Tactic:
simp only [ray_eq_iff]

Premises used: ray_eq_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]
⊢ SameRay R x (AlternatingMap.constOfIsEmpty R M ι 1) ∨ SameRay R x (-AlternatingMap.constOfIsEmpty R M ι 1)

Tactic:
rw [sameRay_or_sameRay_neg_iff_not_linearIndependent]

Premises used: sameRay_or_sameRay_neg_iff_not_linearIndependent
-- 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 : M [⋀^ι]→ₗ[R] R →ₗ[R] R) : (a : M [⋀^ι]→ₗ[R] R) → R) ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1])

Tactic:
h.map' f.toLinearMap f.ker

Premises used: LinearIndependent.map', LinearEquiv.toLinearMap, LinearEquiv.ker
-- 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₁ :
  Eq.{u_1 + 1} (α := Fin (Nat.succ 0).succ → R) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] : Fin (Nat.succ 0).succ → R)
    ((⇑(↑f : M [⋀^ι]→ₗ[R] R →ₗ[R] R) : (a : M [⋀^ι]→ₗ[R] R) → R) ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1] :
      Fin (Nat.succ 0).succ → R)
⊢ LinearIndependent R (M := R) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] : Fin (Nat.succ 0).succ → R)

Tactic:
convert! h.map' f.toLinearMap f.ker

Premises used: LinearIndependent.map', LinearEquiv.toLinearMap, LinearEquiv.ker
-- 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₁ :
  ∀ (i : Fin (Nat.succ 0).succ),
    Eq.{u_1 + 1} (α := R) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] i : R)
      (((⇑(↑f : M [⋀^ι]→ₗ[R] R →ₗ[R] R) : (a : M [⋀^ι]→ₗ[R] R) → R) ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]) i :
        R)
⊢ Eq.{u_1 + 1} (α := Fin (Nat.succ 0).succ → R) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] : Fin (Nat.succ 0).succ → R)
    ((⇑(↑f : M [⋀^ι]→ₗ[R] R →ₗ[R] R) : (a : M [⋀^ι]→ₗ[R] R) → R) ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1] :
      Fin (Nat.succ 0).succ → R)

Tactic:
ext i
-- 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
i : Fin (Nat.succ 0).succ
h₁ :
  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)
h₂ :
  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)
⊢ Eq.{u_1 + 1} (α := R) (![(f : (a : M [⋀^ι]→ₗ[R] R) → R) x, 1] i : R)
    (((⇑(↑f : M [⋀^ι]→ₗ[R] R →ₗ[R] R) : (a : M [⋀^ι]→ₗ[R] R) → R) ∘ ![x, AlternatingMap.constOfIsEmpty R M ι 1]) i : R)

Tactic:
fin_cases i