awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι_1 : Type u_4
inst_5 : DecidableEq ι_1
inst_6 : Fintype ι_1
e : Basis ι_1 R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
this_1 : Finite ι
this : Fintype ι
pos : (this : DecidableEq ι) → M ≃ₗ[R] M
⊢ M ≃ₗ[R] M

Tactic:
have : DecidableEq ι := Classical.typeDecidableEq ι
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι_1 : Type u_4
inst_5 : DecidableEq ι_1
inst_6 : Fintype ι_1
e : Basis ι_1 R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
this_1 : Finite ι
this_2 : Fintype ι
this : DecidableEq ι
rwa rwa₁ rwa₂ rwa₃ : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
⊢ IsUnit.{u_1} (M := R) (det.{u_1, u_2} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f))

Tactic:
rwa [det_toMatrix b]

Premises used: LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι_1 : Type u_4
inst_5 : DecidableEq ι_1
inst_6 : Fintype ι_1
e : Basis ι_1 R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
this_1 : Finite ι
this_2 : Fintype ι
this : DecidableEq ι
⊢ M ≃ₗ[R] M

Tactic:
exact LinearEquiv.ofIsUnitDet (v := b) (v' := b) (f := f) (by rwa [det_toMatrix b])

Premises used: LinearEquiv.ofIsUnitDet
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : ¬Nontrivial R
⊢ M ≃ₗ[R] M

Tactic:
exact 1
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
x : M
⊢ Nontrivial M

Tactic:
nontriviality M
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
x : M
h_1 : Nontrivial M
⊢ Eq (α := M) ((equivOfIsUnitDet h : (a : M) → M) x : M) ((f : (a : M) → M) x : M)

Tactic:
simp [equivOfIsUnitDet, dif_pos (Module.nontrivial R M)]

Premises used: LinearMap.equivOfIsUnitDet, dif_pos, Module.nontrivial
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
h₁ : ∀ (x : M), Eq (α := M) (((↑(equivOfIsUnitDet h) : M →ₗ[R] M) : (a : M) → M) x : M) ((f : (a : M) → M) x : M)
⊢ (↑(equivOfIsUnitDet h) : M →ₗ[R] M) = f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
x : M
⊢ Eq (α := M) (((↑(equivOfIsUnitDet h) : M →ₗ[R] M) : (a : M) → M) x : M) ((f : (a : M) → M) x : M)

Tactic:
apply LinearMap.equivOfIsUnitDet_apply

Premises used: LinearMap.equivOfIsUnitDet_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M_1
𝕜 : Type u_5
inst_7 : Field 𝕜
M : Type u_6
inst_8 : AddCommGroup M
inst_9 : Module 𝕜 M
inst_10 : FiniteDimensional 𝕜 M
f : M →ₗ[𝕜] M
hf : Ne.{u_5 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
rw : IsUnit.{u_5} (M := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜)
⊢ IsUnit.{u_5} (M := 𝕜)
    (det (n := Fin (finrank 𝕜 M))
      (((toMatrix (finBasis 𝕜 M) (finBasis 𝕜 M) :
            LinearEquiv.{u_5, u_5, u_6, u_5} (RingHom.id 𝕜) (M →ₗ[𝕜] M)
              (Matrix (Fin (finrank 𝕜 M)) (Fin (finrank 𝕜 M)) 𝕜)) :
          (a : M →ₗ[𝕜] M) → Matrix (Fin (finrank 𝕜 M)) (Fin (finrank 𝕜 M)) 𝕜)
        f))

Tactic:
rw [LinearMap.det_toMatrix]

Premises used: LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M_1
𝕜 : Type u_5
inst_7 : Field 𝕜
M : Type u_6
inst_8 : AddCommGroup M
inst_9 : Module 𝕜 M
inst_10 : FiniteDimensional 𝕜 M
f : M →ₗ[𝕜] M
hf : Ne.{u_5 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
⊢ IsUnit.{u_5} (M := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜)

Tactic:
isUnit_iff_ne_zero.2 hf

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M_1 : Type u_2
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M_1
𝕜 : Type u_5
inst_7 : Field 𝕜
M : Type u_6
inst_8 : AddCommGroup M
inst_9 : Module 𝕜 M
inst_10 : FiniteDimensional 𝕜 M
f : M →ₗ[𝕜] M
hf : Ne.{u_5 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (0 : 𝕜)
⊢ IsUnit.{u_5} (M := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜)

Tactic:
exact isUnit_iff_ne_zero.2 hf

Premises used: Iff.mpr, isUnit_iff_ne_zero
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
this :
  Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
⊢ Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)

Tactic:
this
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
this :
  Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
h₁ : f = f' ∘ₗ (↑e : M →ₗ[R] M)
⊢ Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)

Tactic:
convert! this using 2
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
this :
  Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
h₁ : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' ∘ₗ (↑e : M →ₗ[R] M) : (a : M) → M) x : M)
⊢ f = f' ∘ₗ (↑e : M →ₗ[R] M)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
this :
  Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
x : M
⊢ Eq (α := M) ((f : (a : M) → M) x : M) ((f' ∘ₗ (↑e : M →ₗ[R] M) : (a : M) → M) x : M)

Tactic:
h x
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
this :
  Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
x : M
⊢ Eq (α := M) ((f : (a : M) → M) x : M) ((f' ∘ₗ (↑e : M →ₗ[R] M) : (a : M) → M) x : M)

Tactic:
exact h x
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
suffices :
  Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
⊢ Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)

Tactic:
suffices Associated (LinearMap.det (f' ∘ₗ ↑e)) (LinearMap.det f') by
    convert! this using 2
    ext x
    exact h x
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
rw :
  Associated
    (HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
      ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑e : M →ₗ[R] M) : R))
    (HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R) (1 : R))
⊢ Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f' ∘ₗ (↑e : M →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)

Tactic:
rw [← mul_one (LinearMap.det f'), LinearMap.det_comp]

Premises used: LinearMap.det, LinearMap.det_comp, mul_one, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
⊢ Associated
    (HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
      ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑e : M →ₗ[R] M) : R))
    (HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R) (1 : R))

Tactic:
Associated.mul_left _ (associated_one_iff_isUnit.mpr e.isUnit_det')

Premises used: Iff.mpr, associated_one_iff_isUnit, LinearEquiv.isUnit_det', Associated.mul_left
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
e : M ≃ₗ[R] M
f f' : M →ₗ[R] M
h : ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((f' : (a : M) → M) ((e : (a : M) → M) x : M) : M)
⊢ Associated
    (HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R)
      ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑e : M →ₗ[R] M) : R))
    (HMul.hMul (α := R) (β := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f' : R) (1 : R))

Tactic:
exact Associated.mul_left _ (associated_one_iff_isUnit.mpr e.isUnit_det')

Premises used: Iff.mpr, associated_one_iff_isUnit, LinearEquiv.isUnit_det', Associated.mul_left
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
⊢ Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f ∘ₗ (↑e : M →ₗ[R] N)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (f ∘ₗ (↑e' : M →ₗ[R] N)) : R)

Tactic:
LinearMap.associated_det_of_eq_comp (e.trans e'.symm) _ _ ?_

Premises used: LinearEquiv.symm, LinearMap.associated_det_of_eq_comp, LinearEquiv.trans
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
refine :
  ∀ (x : M),
    Eq (α := M) ((f ∘ₗ (↑e : M →ₗ[R] N) : (a : M) → M) x : M)
      ((f ∘ₗ (↑e' : M →ₗ[R] N) : (a : M) → M) ((e ≪≫ₗ e'.symm : (a : M) → M) x : M) : M)
⊢ Associated.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (f ∘ₗ (↑e : M →ₗ[R] N)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (f ∘ₗ (↑e' : M →ₗ[R] N)) : R)

Tactic:
refine LinearMap.associated_det_of_eq_comp (e.trans e'.symm) _ _ ?_

Premises used: LinearEquiv.symm, LinearMap.associated_det_of_eq_comp, LinearEquiv.trans
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_5
inst_3 : AddCommGroup N
inst_4 : Module R N
f : N →ₗ[R] M
e e' : M ≃ₗ[R] N
x : M
⊢ Eq (α := M) ((f ∘ₗ (↑e : M →ₗ[R] N) : (a : M) → M) x : M)
    ((f ∘ₗ (↑e' : M →ₗ[R] N) : (a : M) → M) ((e ≪≫ₗ e'.symm : (a : M) → M) x : M) : M)

Tactic:
simp only [LinearMap.comp_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply,
    LinearEquiv.apply_symm_apply]

Premises used: LinearMap.comp_apply, LinearEquiv.trans_apply, LinearEquiv.apply_symm_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
v : (i : ι) → M
i : ι
x y : M
⊢ (fun (v : (i : ι) → M) ↦ (e.toMatrix v).det) (update (β := fun (x : ι) ↦ M) v i (x + y)) =
    HAdd.hAdd (α := R) ((fun (v : (i : ι) → M) ↦ (e.toMatrix v).det) (update (β := fun (x : ι) ↦ M) v i x))
      ((fun (v : (i : ι) → M) ↦ (e.toMatrix v).det) (update (β := fun (x : ι) ↦ M) v i y))

Tactic:
simp only [e.toMatrix_update, map_add, Finsupp.coe_add, det_updateCol_add]

Premises used: Matrix.det_updateCol_add, map_add, Finsupp.coe_add, Module.Basis.toMatrix_update
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
u : (i : ι) → M
i : ι
c : R
x : M
simp :
  ((e.toMatrix u).updateCol i
        (⇑(HSMul.hSMul (β := ι →₀ R) c ((e.repr : (a : M) → ι →₀ R) x : ι →₀ R)) : (a : ι) → R)).det =
    c * ((e.toMatrix u).updateCol i (⇑((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)).det
⊢ (fun (v : (i : ι) → M) ↦ (e.toMatrix v).det) (update (β := fun (x : ι) ↦ M) u i (c • x)) =
    HSMul.hSMul (β := R) c ((fun (v : (i : ι) → M) ↦ (e.toMatrix v).det) (update (β := fun (x : ι) ↦ M) u i x))

Tactic:
simp only [e.toMatrix_update, smul_eq_mul, map_smul]

Premises used: Module.Basis.toMatrix_update, smul_eq_mul, map_smul
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
u : (i : ι) → M
i : ι
c : R
x : M
⊢ ((e.toMatrix u).updateCol i
        (⇑(HSMul.hSMul (β := ι →₀ R) c ((e.repr : (a : M) → ι →₀ R) x : ι →₀ R)) : (a : ι) → R)).det =
    c * ((e.toMatrix u).updateCol i (⇑((e.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R)).det

Tactic:
apply det_updateCol_smul

Premises used: Matrix.det_updateCol_smul
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
dsimp : (e.toMatrix v).det = 0
⊢ Eq.{u_1 + 1} (α := R)
    (MultilinearMap.toFun (R := R) (M₁ := fun (x : ι) ↦ M)
      (MultilinearMap.mk' (M₁ := fun (x : ι) ↦ M) (fun (v : (i : ι) → M) ↦ (e.toMatrix v).det) ⋯ ⋯) v)
    0

Tactic:
dsimp
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
rw : ((e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j)).det = 0
⊢ (e.toMatrix v).det = 0

Tactic:
rw [← Function.update_eq_self i v, h, ← det_transpose, e.toMatrix_update, ← updateRow_transpose,
      ← e.toMatrix_transpose_apply]

Premises used: Function.update_eq_self, Matrix.det_transpose, Matrix.updateRow_transpose, Module.Basis.toMatrix_update, Module.Basis.toMatrix_transpose_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
apply : (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) i = (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) j
⊢ ((e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j)).det = 0

Tactic:
apply det_zero_of_row_eq hij

Premises used: Matrix.det_zero_of_row_eq
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
v : ι → M
i j : ι
h : v i = v j
hij : i ≠ j
rw : (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) i = (e.toMatrix v)ᵀ j
rw₁ rw₂ : (e.toMatrix v)ᵀ j = (e.toMatrix v)ᵀ j
⊢ (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) i = (e.toMatrix v)ᵀ.updateRow i ((e.toMatrix v)ᵀ j) j

Tactic:
rw [updateRow_ne hij.symm, updateRow_self]

Premises used: Ne.symm, Matrix.updateRow_ne, Matrix.updateRow_self
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
⊢ (e.det : (a : ι → M) → R) v = (e.toMatrix v).det

Tactic:
rfl

Premises used: Matrix.det, rfl
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
⊢ Eq.{u_1 + 1} (α := R) ((e.det : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) (1 : R)

Tactic:
simp [e.det_apply]

Premises used: Module.Basis.det_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
inst_5 : IsEmpty ι
H :
  ∀ (v : ι → M),
    Eq.{u_1 + 1} (α := R) ((e.det : (a : ι → M) → R) v : R)
      ((AlternatingMap.constOfIsEmpty R M ι 1 : (a : ι → M) → R) v : R)
⊢ e.det = AlternatingMap.constOfIsEmpty R M ι 1

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
inst_5 : IsEmpty ι
v : ι → M
⊢ Eq.{u_1 + 1} (α := R) ((e.det : (a : ι → M) → R) v : R)
    ((AlternatingMap.constOfIsEmpty R M ι 1 : (a : ι → M) → R) v : R)

Tactic:
Matrix.det_isEmpty

Premises used: Matrix.det_isEmpty, Matrix.det
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
inst_5 : IsEmpty ι
v : ι → M
⊢ Eq.{u_1 + 1} (α := R) ((e.det : (a : ι → M) → R) v : R)
    ((AlternatingMap.constOfIsEmpty R M ι 1 : (a : ι → M) → R) v : R)

Tactic:
exact Matrix.det_isEmpty

Premises used: Matrix.det_isEmpty
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
inst_5 : Nontrivial R
h : e.det = 0
⊢ False

Tactic:
simpa [h] using e.det_self

Premises used: Module.Basis.det_self
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
G : Type u_5
inst_5 : Group G
inst_6 : DistribMulAction G M
inst_7 : SMulCommClass G R M
g : G
v : ι → M
simp_rw : ((g • e).toMatrix v).det = (e.toMatrix (g⁻¹ • v)).det
⊢ Eq.{u_1 + 1} (α := R) (((g • e).det : (a : ι → M) → R) v : R) ((e.det : (a : ι → M) → R) (g⁻¹ • v) : R)

Tactic:
simp_rw [det_apply, toMatrix_smul_left]

Premises used: Module.Basis.toMatrix_smul_left, Module.Basis.det_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
mp :
  LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ →
    IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R)
mpr :
  IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R) →
    LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤
⊢ LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤ ↔
    IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R)

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
v' : Basis ι R M := Basis.mk hli ⋯
mp : IsUnit (e.toMatrix v).det
⊢ IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R)

Tactic:
rw [e.det_apply]

Premises used: Module.Basis.det_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
v' : Basis ι R M := Basis.mk hli ⋯
⊢ IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix v' e : (a : M →ₗ[R] M) → Matrix ι ι R) (↑(LinearEquiv.refl R M) : M →ₗ[R] M)))

Tactic:
LinearEquiv.isUnit_det (LinearEquiv.refl R M) v' e

Premises used: LinearEquiv.isUnit_det, LinearEquiv.refl
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
v' : Basis ι R M := Basis.mk hli ⋯
h : e.toMatrix v = (LinearMap.toMatrix v' e : (a : M →ₗ[R] M) → Matrix ι ι R) (↑(LinearEquiv.refl R M) : M →ₗ[R] M)
⊢ IsUnit (e.toMatrix v).det

Tactic:
convert! LinearEquiv.isUnit_det (LinearEquiv.refl R M) v' e using 2

Premises used: LinearEquiv.isUnit_det, LinearEquiv.refl