awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
h :
  ∀ (x : M →ₗ[A] M),
    Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) x : A)
      ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1 : (a : M →ₗ[A] M) → A)
          x :
        A)
⊢ Eq (α := (a : M →ₗ[A] M) → A) (⇑LinearMap.det : (a : M →ₗ[A] M) → A)
    (⇑(if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1) : (a : M →ₗ[A] M) → A)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
x : M →ₗ[A] M
h :
  Eq.{u_5 + 1} (α := A)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1 : (a : M →ₗ[A] M) → A) x :
      A)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1 : (a : M →ₗ[A] M) → A) x :
      A)
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) x : A)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1 : (a : M →ₗ[A] M) → A) x :
      A)

Tactic:
rw [LinearMap.det_def]

Premises used: LinearMap.det_def
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
x : M →ₗ[A] M
pos :
  ∀ (h : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)),
    Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk ⋯.some) : (a : M →ₗ[A] M) → A) x : A)
      ((detAux (Trunc.mk ⋯.some) : (a : M →ₗ[A] M) → A) x : A)
neg :
  (¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)) →
    Eq.{u_5 + 1} (α := A) ((1 : (a : M →ₗ[A] M) → A) x : A) ((1 : (a : M →ₗ[A] M) → A) x : A)
⊢ Eq.{u_5 + 1} (α := A)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1 : (a : M →ₗ[A] M) → A) x :
      A)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1 : (a : M →ₗ[A] M) → A) x :
      A)

Tactic:
split_ifs
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
x : M →ₗ[A] M
h : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
⊢ Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk ⋯.some) : (a : M →ₗ[A] M) → A) x : A)
    ((detAux (Trunc.mk ⋯.some) : (a : M →ₗ[A] M) → A) x : A)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
x : M →ₗ[A] M
h : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)
⊢ Eq.{u_5 + 1} (α := A) ((1 : (a : M →ₗ[A] M) → A) x : A) ((1 : (a : M →ₗ[A] M) → A) x : A)

Tactic:
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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
pos : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Free R M
neg : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Free R M
⊢ Free R M

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (Module.Basis s R M)

Premises used: Finset
-- 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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)
pos : ∀ (s : Finset M) (hs : Basis (↥s) R M), Free R M
⊢ Free R M

Tactic:
rcases H with ⟨s, ⟨hs⟩⟩
-- 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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
s : Finset M
hs : Basis (↥s) R M
⊢ Free R M

Tactic:
Module.Free.of_basis hs

Premises used: Module.Free.of_basis
-- 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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
s : Finset M
hs : Basis (↥s) R M
⊢ Free R M

Tactic:
exact Module.Free.of_basis hs

Premises used: Module.Free.of_basis
-- 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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
⊢ Free R M

Tactic:
simp [LinearMap.coe_det, H] at hf

Premises used: LinearMap.coe_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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
⊢ Free R M

Tactic:
classical simp [LinearMap.coe_det, H] at hf

Premises used: LinearMap.coe_det
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
s : Finset M
b : Basis (↥s) A M
f : M →ₗ[A] M
⊢ ∃ (s : Finset M), Nonempty (Basis (↥s) A M)

Tactic:
have : ∃ s : Finset M, Nonempty (Basis s A M) := ⟨s, ⟨b⟩⟩
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
s : Finset M
b : Basis (↥s) A M
f : M →ₗ[A] M
this : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
rw :
  Eq.{u_5 + 1} (α := A)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1 : (a : M →ₗ[A] M) → A) f :
      A)
    (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f) : A)
rw₁ :
  Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk ⋯.some) : (a : M →ₗ[A] M) → A) f : A)
    (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f) : A)
rw₂ rw₃ :
  Eq.{u_5 + 1} (α := A) (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
    (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
    (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f) : A)

Tactic:
rw [LinearMap.coe_det, dif_pos this, detAux_def'' _ b]

Premises used: LinearMap.detAux_def'', dif_pos, LinearMap.coe_det
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
b : Basis ι A M
f : M →ₗ[A] M
haveI :
  ∀ (this : DecidableEq M),
    Eq.{u_5 + 1} (α := A) (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
⊢ Eq.{u_5 + 1} (α := A) (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f) : A)
    ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
haveI := Classical.decEq M
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Type u_5
inst_3 : CommRing A
inst_4 : Module A M
b : Basis ι A M
f : M →ₗ[A] M
this : DecidableEq M
rw :
  Eq.{u_5 + 1} (α := A) (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f))
    (det.{u_5, u_2} (n := ↥(Finset.image.{u_4, u_2} (α := ι) (⇑b : (a : ι) → M) Finset.univ))
      ((toMatrix b.reindexFinsetRange b.reindexFinsetRange :
          (a : M →ₗ[A] M) →
            Matrix (↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) (↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) A)
        f))
rw₁ rw₂ :
  Eq.{u_5 + 1} (α := A)
    (det.{u_5, u_2} (n := ↥(Finset.image.{u_4, u_2} (α := ι) (⇑b : (a : ι) → M) Finset.univ))
      ((toMatrix b.reindexFinsetRange b.reindexFinsetRange :
          (a : M →ₗ[A] M) →
            Matrix (↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) (↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) A)
        f))
    (det.{u_5, u_2} (n := ↥(Finset.image.{u_4, u_2} (α := ι) (⇑b : (a : ι) → M) Finset.univ))
      ((toMatrix b.reindexFinsetRange b.reindexFinsetRange :
          (a : M →ₗ[A] M) →
            Matrix (↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) (↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) A)
        f))
⊢ Eq.{u_5 + 1} (α := A) (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f) : A)
    ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
rw [det_eq_det_toMatrix_of_finset b.reindexFinsetRange,
    det_toMatrix_eq_det_toMatrix b b.reindexFinsetRange]

Premises used: Module.Basis.reindexFinsetRange, LinearMap.det_eq_det_toMatrix_of_finset, LinearMap.det_toMatrix_eq_det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
A : Type u_5
inst : CommRing A
ι : Type u_7
inst_1 : Fintype ι
inst_2 : DecidableEq ι
f : (ι → A) →ₗ[A] ι → A
⊢ Eq.{u_5 + 1} (α := A) (det.{u_5, u_7} (n := ι) ((toMatrix' : (a : (ι → A) →ₗ[A] ι → A) → Matrix ι ι A) f) : A)
    (((LinearMap.det (M := ι → A) (A := A) : ((ι → A) →ₗ[A] ι → A) →* A) : (a : (ι → A) →ₗ[A] ι → A) → A) f : A)

Tactic:
simp [← toMatrix_eq_toMatrix']

Premises used: LinearMap.toMatrix_eq_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
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
b : Basis ι R M
f : Matrix ι ι R
rw :
  det.{u_1, u_4} (n := ι)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) ((toLin b b : (a : Matrix ι ι R) → M →ₗ[R] M) f)) =
    f.det
rw₁ rw₂ : f.det = f.det
⊢ (LinearMap.det : (a : M →ₗ[R] M) → R) ((toLin b b : (a : Matrix ι ι R) → M →ₗ[R] M) f : M →ₗ[R] M) = f.det

Tactic:
rw [← LinearMap.det_toMatrix b, LinearMap.toMatrix_toLin]

Premises used: LinearMap.det_toMatrix, LinearMap.toMatrix_toLin
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
f : Matrix ι ι R
⊢ ((LinearMap.det (M := ι → R) (A := R) : ((ι → R) →ₗ[R] ι → R) →* R) : (a : (ι → R) →ₗ[R] ι → R) → R)
      ((toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) f : (ι → R) →ₗ[R] ι → R) =
    f.det

Tactic:
simp only [← toLin_eq_toLin', det_toLin]

Premises used: Matrix.toLin_eq_toLin', LinearMap.det_toLin
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb :
  ∀ (s : Finset M) (b : Basis (↥s) A M),
    P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
h1 : P 1
H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
obtain : ∀ (s : Finset M) (b : Basis (↥s) A M), P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)

Tactic:
obtain ⟨s, ⟨b⟩⟩ := H
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb :
  ∀ (s : Finset M) (b : Basis (↥s) A M),
    P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
h1 : P 1
s : Finset M
b : Basis (↥s) A M
rw : P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)

Tactic:
rw [← det_toMatrix b]

Premises used: LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb :
  ∀ (s : Finset M) (b : Basis (↥s) A M),
    P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
h1 : P 1
s : Finset M
b : Basis (↥s) A M
⊢ P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))

Tactic:
hb s b
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb :
  ∀ (s : Finset M) (b : Basis (↥s) A M),
    P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
h1 : P 1
s : Finset M
b : Basis (↥s) A M
⊢ P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))

Tactic:
exact hb s b
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb :
  ∀ (s : Finset M) (b : Basis (↥s) A M),
    P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
h1 : P 1
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)
rwa :
  P ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk ⋯.some) else 1 : (a : M →ₗ[A] M) → A) f)
rwa₁ rwa₂ rwa₃ rwa₄ : P ((1 : (a : M →ₗ[A] M) → A) f)
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)

Tactic:
rwa [LinearMap.det_def, dif_neg H]

Premises used: LinearMap.det_def, dif_neg
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb :
  ∀ (s : Finset M) (b : Basis (↥s) A M),
    P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
h1 : P 1
if : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)), P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
if₁ : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)), P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
if₂ : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)), P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
if₃ if₄ : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)), P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)

Tactic:
if H : ∃ s : Finset M, Nonempty (Basis s A M) then
    obtain ⟨s, ⟨b⟩⟩ := H
    rw [← det_toMatrix b]
    exact hb s b
  else
    rwa [LinearMap.det_def, dif_neg H]

Premises used: Finset, LinearMap.det_def
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : DecidableEq M
P : A → Prop
f : M →ₗ[A] M
hb :
  ∀ (s : Finset M) (b : Basis (↥s) A M),
    P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
h1 : P 1
if : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)), P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
if₁ : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)), P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
if₂ : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)), P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
if₃ if₄ : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)), P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)

Tactic:
classical
  if H : ∃ s : Finset M, Nonempty (Basis s A M) then
    obtain ⟨s, ⟨b⟩⟩ := H
    rw [← det_toMatrix b]
    exact hb s b
  else
    rwa [LinearMap.det_def, dif_neg H]

Premises used: Finset, LinearMap.det_def
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
f g : M →ₗ[A] M
⊢ (LinearMap.det : (a : M →ₗ[A] M) → A) (f ∘ₗ g) =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) g : A)

Tactic:
LinearMap.det.map_mul f g

Premises used: LinearMap.det, MonoidHom.map_mul
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) id : A) (1 : A)

Tactic:
LinearMap.det.map_one

Premises used: LinearMap.det, MonoidHom.map_one
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
c : A
f : M →ₗ[A] M
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
c : A
f : M →ₗ[A] M
h : Nontrivial A
pos :
  ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)),
    (LinearMap.det : (a : M →ₗ[A] M) → A) (c • f) =
      HMul.hMul (β := A) (c ^ finrank A M) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
neg :
  ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)),
    (LinearMap.det : (a : M →ₗ[A] M) → A) (c • f) =
      HMul.hMul (β := A) (c ^ finrank A M) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
⊢ (LinearMap.det : (a : M →ₗ[A] M) → A) (c • f) =
    HMul.hMul (β := A) (c ^ finrank A M) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)

Premises used: Finset
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
c : A
f : M →ₗ[A] M
h : Nontrivial A
H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
rcases : ∀ (s : Finset M) (hs : Basis (↥s) A M), Module.Finite A M
⊢ Module.Finite A M

Tactic:
rcases H with ⟨s, ⟨hs⟩⟩
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
c : A
f : M →ₗ[A] M
h : Nontrivial A
s : Finset M
hs : Basis (↥s) A M
⊢ Module.Finite A M

Tactic:
Module.Finite.of_basis hs

Premises used: Module.Finite.of_basis
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
c : A
f : M →ₗ[A] M
h : Nontrivial A
s : Finset M
hs : Basis (↥s) A M
⊢ Module.Finite A M

Tactic:
exact Module.Finite.of_basis hs

Premises used: Module.Finite.of_basis
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
c : A
f : M →ₗ[A] M
h : Nontrivial A
H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
⊢ Module.Finite A M

Tactic:
have : Module.Finite A M := by
      rcases H with ⟨s, ⟨hs⟩⟩
      exact Module.Finite.of_basis hs
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
c : A
f : M →ₗ[A] M
h : Nontrivial A
H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
this : Module.Finite A M
⊢ (LinearMap.det : (a : M →ₗ[A] M) → A) (c • f) =
    HMul.hMul (β := A) (c ^ finrank A M) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
simp only [← det_toMatrix (Module.finBasis A M), map_smul, Fintype.card_fin, Matrix.det_smul]

Premises used: Fintype.card_fin, Matrix.det_smul, Module.finBasis, LinearMap.det_toMatrix, map_smul
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
c : A
f : M →ₗ[A] M
h : Nontrivial A
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)
⊢ finrank A M = 0

Tactic:
have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
c : A
f : M →ₗ[A] M
h : Nontrivial A
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)
this : finrank A M = 0
⊢ (LinearMap.det : (a : M →ₗ[A] M) → A) (c • f) =
    HMul.hMul (β := A) (c ^ finrank A M) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
simp [coe_det, H, this]

Premises used: LinearMap.coe_det
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
c : A
f : M →ₗ[A] M
h : Nontrivial A
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)
neg neg₁ neg₂ :
  ∀ (this : finrank A M = 0),
    (LinearMap.det : (a : M →ₗ[A] M) → A) (c • f) =
      HMul.hMul (β := A) (c ^ finrank A M) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
⊢ (LinearMap.det : (a : M →ₗ[A] M) → A) (c • f) =
    HMul.hMul (β := A) (c ^ finrank A M) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
classical
      have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H
      simp [coe_det, H, this]

Premises used: LinearMap.coe_det
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
ι : Type u_7
inst_3 : Finite ι
inst_4 : Nonempty ι
b : Basis ι A M
haveI : ∀ (this : DecidableEq ι), Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)

Tactic:
haveI := Classical.decEq ι
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
ι : Type u_7
inst_3 : Finite ι
inst_4 : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
intro : ∀ (val : Fintype ι), Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
ι : Type u_7
inst_3 : Finite ι
inst_4 : Nonempty ι
b : Basis ι A M
this : DecidableEq ι
val : Fintype ι
intro : Eq.{u_5 + 1} (α := A) (det.{u_5, u_7} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) 0)) 0
intro₁ : Eq.{u_5 + 1} (α := A) (det.{u_5, u_7} (n := ι) 0) 0
intro₂ : Eq.{u_5 + 1} (α := A) 0 0
intro₃ : Nonempty ι
intro₄ : Eq.{u_5 + 1} (α := A) 0 0
intro₅ intro₆ intro₇ : Nonempty ι
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)

Tactic:
rwa [← det_toMatrix b, map_zero, det_zero]

Premises used: Matrix.det_zero, map_zero, LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
inst_3 : Free A M
⊢ (LinearMap.det : (a : M →ₗ[A] M) → A) 0 = HPow.hPow (α := A) 0 (finrank A M)

Tactic:
simp only [← zero_smul A (1 : M →ₗ[A] M), det_smul, mul_one, map_one]

Premises used: zero_smul, map_one, LinearMap.det_smul, mul_one, OfNat.ofNat
-- 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
h : ¬Module.Finite R M
f : M →ₗ[R] M
hnc : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)

Tactic:
rw [LinearMap.det, dif_neg, MonoidHom.one_apply]

Premises used: LinearMap.det, dif_neg, MonoidHom.one_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
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)

Tactic:
fun ⟨_, ⟨b⟩⟩ ↦ h (Module.Finite.of_basis b)

Premises used: False, _private.0.LinearMap.det_eq_one_of_not_module_finite.match_1, Module.Finite.of_basis, Not
-- 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
h : ¬Module.Finite R M
f : M →ₗ[R] M
⊢ ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)

Tactic:
exact fun ⟨_, ⟨b⟩⟩ ↦ h (Module.Finite.of_basis b)
-- 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 : Subsingleton M
f : M →ₗ[R] M
have : ∀ (b : Basis (Fin 0) R M), Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)

Tactic:
have b : Basis (Fin 0) R M := Basis.empty M