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
inst_3 : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
rw : Eq.{u_1 + 1} (α := R) (det (n := Fin 0) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin 0) (Fin 0) R) f)) 1
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)

Tactic:
rw [← f.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
inst_3 : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin 0) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin 0) (Fin 0) R) f)) 1

Tactic:
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
inst_3 : Subsingleton M
f : M →ₗ[R] M
b : Basis (Fin 0) R M
⊢ Eq.{u_1 + 1} (α := R) (det (n := Fin 0) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Fin 0) (Fin 0) R) f)) 1

Tactic:
exact Matrix.det_isEmpty

Premises used: Matrix.det_isEmpty
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
𝕜 : Type u_7
inst : Field 𝕜
M : Type u_8
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
⊢ Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (1 : 𝕜)

Tactic:
@LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl

Premises used: LinearMap.det_cases, rfl
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
𝕜 : Type u_7
inst : Field 𝕜
M : Type u_8
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
refine :
  ∀ (s : Finset M) (b : Basis (↥s) 𝕜 M),
    (fun (t : 𝕜) ↦ t = 1) (det.{u_7, u_8} (n := ↥s) ((toMatrix b b : (a : M →ₗ[𝕜] M) → Matrix (↥s) (↥s) 𝕜) f))
⊢ Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (1 : 𝕜)

Tactic:
refine @LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl

Premises used: LinearMap.det_cases, rfl
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
𝕜 : Type u_7
inst : Field 𝕜
M : Type u_8
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis (↥s) 𝕜 M
rw : Fintype.card.{u_8} ↥s = 0
⊢ IsEmpty.{u_8 + 1} ↥s

Tactic:
rw [← Fintype.card_eq_zero_iff]

Premises used: Fintype.card_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
𝕜 : Type u_7
inst : Field 𝕜
M : Type u_8
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis (↥s) 𝕜 M
⊢ Fintype.card.{u_8} ↥s = 0

Tactic:
(Module.finrank_eq_card_basis b).symm.trans h

Premises used: Module.finrank_eq_card_basis, Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
𝕜 : Type u_7
inst : Field 𝕜
M : Type u_8
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis (↥s) 𝕜 M
⊢ Fintype.card.{u_8} ↥s = 0

Tactic:
exact (Module.finrank_eq_card_basis b).symm.trans h

Premises used: Module.finrank_eq_card_basis, Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
𝕜 : Type u_7
inst : Field 𝕜
M : Type u_8
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis (↥s) 𝕜 M
⊢ IsEmpty.{u_8 + 1} ↥s

Tactic:
have : IsEmpty s := by
      rw [← Fintype.card_eq_zero_iff]
      exact (Module.finrank_eq_card_basis b).symm.trans h
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
𝕜 : Type u_7
inst : Field 𝕜
M : Type u_8
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis (↥s) 𝕜 M
this : IsEmpty.{u_8 + 1} ↥s
⊢ Eq.{u_7 + 1} (α := 𝕜) (det.{u_7, u_8} (n := ↥s) ((toMatrix b b : (a : M →ₗ[𝕜] M) → Matrix (↥s) (↥s) 𝕜) f)) 1

Tactic:
Matrix.det_isEmpty

Premises used: Matrix.det_isEmpty
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
𝕜 : Type u_7
inst : Field 𝕜
M : Type u_8
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
s : Finset M
b : Basis (↥s) 𝕜 M
this : IsEmpty.{u_8 + 1} ↥s
⊢ Eq.{u_7 + 1} (α := 𝕜) (det.{u_7, u_8} (n := ↥s) ((toMatrix b b : (a : M →ₗ[𝕜] M) → Matrix (↥s) (↥s) 𝕜) f)) 1

Tactic:
exact Matrix.det_isEmpty

Premises used: Matrix.det_isEmpty
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
𝕜 : Type u_7
inst : Field 𝕜
M : Type u_8
inst_1 : AddCommGroup M
inst_2 : Module 𝕜 M
h : finrank 𝕜 M = 0
f : M →ₗ[𝕜] M
refine :
  ∀ (s : Finset M) (b : Basis (↥s) 𝕜 M),
    (fun (t : 𝕜) ↦ t = 1) (det.{u_7, u_8} (n := ↥s) ((toMatrix b b : (a : M →ₗ[𝕜] M) → Matrix (↥s) (↥s) 𝕜) f))
refine₁ :
  ∀ (s : Finset M) (b : Basis (↥s) 𝕜 M),
    Eq.{u_7 + 1} (α := 𝕜) (det.{u_7, u_8} (n := ↥s) ((toMatrix b b : (a : M →ₗ[𝕜] M) → Matrix (↥s) (↥s) 𝕜) f)) 1
refine₂ :
  ∀ (s : Finset M) (b : Basis (↥s) 𝕜 M) (this : IsEmpty.{u_8 + 1} ↥s),
    Eq.{u_7 + 1} (α := 𝕜) (det.{u_7, u_8} (n := ↥s) ((toMatrix b b : (a : M →ₗ[𝕜] M) → Matrix (↥s) (↥s) 𝕜) f)) 1
⊢ Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (1 : 𝕜)

Tactic:
classical
    refine @LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl
    intro s b
    have : IsEmpty s := by
      rw [← Fintype.card_eq_zero_iff]
      exact (Module.finrank_eq_card_basis b).symm.trans h
    exact Matrix.det_isEmpty

Premises used: Matrix.det_isEmpty
-- 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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
pos :
  ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)),
    Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : N →ₗ[A] N) → A) ((↑e : M →ₗ[A] N) ∘ₗ f ∘ₗ (↑e.symm : N →ₗ[A] M)) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
neg :
  ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)),
    Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : N →ₗ[A] N) → A) ((↑e : M →ₗ[A] N) ∘ₗ f ∘ₗ (↑e.symm : N →ₗ[A] M)) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : N →ₗ[A] N) → A) ((↑e : M →ₗ[A] N) ∘ₗ f ∘ₗ (↑e.symm : N →ₗ[A] M)) : A)
    ((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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
pos :
  ∀ (s : Finset M) (b : Basis (↥s) A M),
    Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : N →ₗ[A] N) → A) ((↑e : M →ₗ[A] N) ∘ₗ f ∘ₗ (↑e.symm : N →ₗ[A] M)) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : N →ₗ[A] N) → A) ((↑e : M →ₗ[A] N) ∘ₗ f ∘ₗ (↑e.symm : N →ₗ[A] M)) : A)
    ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
rcases H with ⟨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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
pos :
  HMul.hMul (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) (β := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
      ((toMatrix b (b.map e) : (a : M →ₗ[A] N) → Matrix (↥s) (↥s) A) (↑e : M →ₗ[A] N) :
        Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
      ((toMatrix (b.map e) b : (a : N →ₗ[A] M) → Matrix (↥s) (↥s) A) (↑e.symm : N →ₗ[A] M) :
        Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) =
    1
pos₁ :
  HMul.hMul (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) (β := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
      ((toMatrix (b.map e) b : (a : N →ₗ[A] M) → Matrix (↥s) (↥s) A) (↑e.symm : N →ₗ[A] M) :
        Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
      ((toMatrix b (b.map e) : (a : M →ₗ[A] N) → Matrix (↥s) (↥s) A) (↑e : M →ₗ[A] N) :
        Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) =
    1
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : N →ₗ[A] N) → A) ((↑e : M →ₗ[A] N) ∘ₗ f ∘ₗ (↑e.symm : N →ₗ[A] M)) : A)
    ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
rw [← det_toMatrix b f, ← det_toMatrix (b.map e), toMatrix_comp (b.map e) b (b.map e),
        toMatrix_comp (b.map e) b b, ← Matrix.mul_assoc, Matrix.det_conj_of_mul_eq_one]

Premises used: Matrix.mul_assoc, Module.Basis.map, LinearMap.toMatrix_comp, LinearMap.det_toMatrix, Matrix.det_conj_of_mul_eq_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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
pos :
  Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    ((toMatrix (b.map e) (b.map e) : (a : N →ₗ[A] N) → Matrix (↥s) (↥s) A) ((↑e : M →ₗ[A] N) ∘ₗ (↑e.symm : N →ₗ[A] M)) :
      Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    (1 : Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
pos₁ :
  Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    ((toMatrix (b.map e) (b.map e) : (a : N →ₗ[A] N) → Matrix (↥s) (↥s) A) (↑(e.symm ≪≫ₗ e) : N →ₗ[A] N) :
      Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    (1 : Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
pos₂ :
  Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    ((toMatrix (b.map e) (b.map e) : (a : N →ₗ[A] N) → Matrix (↥s) (↥s) A) (↑(LinearEquiv.refl A N) : N →ₗ[A] N) :
      Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    (1 : Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
pos₃ :
  Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    ((toMatrix (b.map e) (b.map e) : (a : N →ₗ[A] N) → Matrix (↥s) (↥s) A) id : Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    (1 : Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
pos₄ pos₅ : Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) 1 1
⊢ HMul.hMul (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) (β := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
      ((toMatrix b (b.map e) : (a : M →ₗ[A] N) → Matrix (↥s) (↥s) A) (↑e : M →ₗ[A] N) :
        Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
      ((toMatrix (b.map e) b : (a : N →ₗ[A] M) → Matrix (↥s) (↥s) A) (↑e.symm : N →ₗ[A] M) :
        Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) =
    1

Tactic:
rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]

Premises used: LinearMap.toMatrix_id, LinearEquiv.refl_toLinearMap, LinearEquiv.symm_trans_self, LinearEquiv.comp_coe, LinearMap.toMatrix_comp
-- 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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset M
b : Basis (↥s) A M
pos :
  Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) ((↑e.symm : N →ₗ[A] M) ∘ₗ (↑e : M →ₗ[A] N)) :
      Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    (1 : Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
pos₁ :
  Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) (↑(e ≪≫ₗ e.symm) : M →ₗ[A] M) :
      Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    (1 : Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
pos₂ :
  Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) (↑(LinearEquiv.refl A M) : M →ₗ[A] M) :
      Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    (1 : Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
pos₃ :
  Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) id : Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
    (1 : Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
pos₄ pos₅ : Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) 1 1
⊢ HMul.hMul (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) (β := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
      ((toMatrix (b.map e) b : (a : N →ₗ[A] M) → Matrix (↥s) (↥s) A) (↑e.symm : N →ₗ[A] M) :
        Matrix.{u_2, u_2, u_5} (↥s) (↥s) A)
      ((toMatrix b (b.map e) : (a : M →ₗ[A] N) → Matrix (↥s) (↥s) A) (↑e : M →ₗ[A] N) :
        Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) =
    1

Tactic:
rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
          toMatrix_id]

Premises used: LinearMap.toMatrix_id, LinearEquiv.refl_toLinearMap, LinearEquiv.comp_coe, LinearMap.toMatrix_comp, LinearEquiv.self_trans_symm
-- 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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)
contrapose : ∀ (H : ∃ (t : Finset N), Nonempty (Basis (↥t) A N)), ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
⊢ ¬∃ (t : Finset N), Nonempty (Basis (↥t) A N)

Tactic:
contrapose 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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ∃ (t : Finset N), Nonempty (Basis (↥t) A N)
rcases : ∀ (s : Finset N) (b : Basis (↥s) A N), ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
⊢ ∃ (s : Finset M), Nonempty (Basis (↥s) A M)

Tactic:
rcases H with ⟨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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset N
b : Basis (↥s) A N
⊢ ∃ (s : Finset M), Nonempty (Basis (↥s) A M)

Tactic:
⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩

Premises used: LinearEquiv.symm, Module.Basis.reindexFinsetRange, Module.Basis.map, Nonempty.intro, Exists.intro
-- 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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
s : Finset N
b : Basis (↥s) A N
⊢ ∃ (s : Finset M), Nonempty (Basis (↥s) A M)

Tactic:
exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩
-- 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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)
⊢ ¬∃ (t : Finset N), Nonempty (Basis (↥t) A N)

Tactic:
have H' : ¬∃ t : Finset N, Nonempty (Basis t A N) := by
        contrapose H
        rcases H with ⟨s, ⟨b⟩⟩
        exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩
-- 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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)
H' : ¬∃ (t : Finset N), Nonempty (Basis (↥t) A N)
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : N →ₗ[A] N) → A) ((↑e : M →ₗ[A] N) ∘ₗ f ∘ₗ (↑e.symm : N →ₗ[A] M)) : A)
    ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg, not_false_eq_true]

Premises used: dif_neg, MonoidHom.one_apply, LinearMap.coe_det, not_false_eq_true
-- 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
N : Type u_7
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] M
e : M ≃ₗ[A] N
pos :
  ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)),
    Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : N →ₗ[A] N) → A) ((↑e : M →ₗ[A] N) ∘ₗ f ∘ₗ (↑e.symm : N →ₗ[A] M)) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
neg neg₁ :
  ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)),
    Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : N →ₗ[A] N) → A) ((↑e : M →ₗ[A] N) ∘ₗ f ∘ₗ (↑e.symm : N →ₗ[A] M)) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : N →ₗ[A] N) → A) ((↑e : M →ₗ[A] N) ∘ₗ f ∘ₗ (↑e.symm : N →ₗ[A] M)) : A)
    ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
classical
    by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
    · rcases H with ⟨s, ⟨b⟩⟩
      rw [← det_toMatrix b f, ← det_toMatrix (b.map e), toMatrix_comp (b.map e) b (b.map e),
        toMatrix_comp (b.map e) b b, ← Matrix.mul_assoc, Matrix.det_conj_of_mul_eq_one]
      · rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
      · rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
    · have H' : ¬∃ t : Finset N, Nonempty (Basis t A N) := by
        contrapose H
        rcases H with ⟨s, ⟨b⟩⟩
        exact ⟨_, ⟨(b.map e.symm).reindexFinsetRange⟩⟩
      simp only [coe_det, H, H', MonoidHom.one_apply, dif_neg, not_false_eq_true]

Premises used: Finset, LinearMap.toMatrix_id, Matrix.mul_assoc, LinearEquiv.refl_toLinearMap, LinearEquiv.symm_trans_self, dif_neg, LinearEquiv.comp_coe, LinearMap.toMatrix_comp, MonoidHom.one_apply, LinearMap.coe_det, not_false_eq_true, LinearEquiv.self_trans_symm, Matrix.det_conj_of_mul_eq_one
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_7
inst_1 : CommRing A
inst_2 : Module A M
f : M →ₗ[A] M
hf : IsUnit f
⊢ IsUnit.{u_7} (M := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A)

Tactic:
IsUnit.map LinearMap.det hf

Premises used: LinearMap.det, IsUnit.map
-- 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 : Module.Finite R M
inst_4 : Free R M
f : M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
rw :
  IsUnit (M := Matrix.{u_2, u_2, u_1} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) f :
        Matrix.{u_2, u_2, u_1} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) ↔
    IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
rw₁ :
  IsUnit (M := Matrix.{u_2, u_2, u_1} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R)
      ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) f :
        Matrix.{u_2, u_2, u_1} (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) ↔
    IsUnit.{u_1} (M := R)
      (det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) f))
rw₂ rw₃ :
  IsUnit.{u_1} (M := R)
      (det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) f)) ↔
    IsUnit.{u_1} (M := R)
      (det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) f))
⊢ IsUnit f ↔ IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)

Tactic:
rw [← isUnit_toMatrix_iff b, ← det_toMatrix b, Matrix.isUnit_iff_isUnit_det (toMatrix b b f)]

Premises used: Matrix.isUnit_iff_isUnit_det, LinearMap.isUnit_toMatrix_iff, DFunLike.coe, LinearMap.det_toMatrix, LinearMap.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
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 (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)
pos : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Module.Finite R M
neg : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Module.Finite R M
⊢ Module.Finite R M

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (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), Module.Finite R M
⊢ Module.Finite 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
⊢ Module.Finite R M

Tactic:
Module.Finite.of_basis hs

Premises used: Module.Finite.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
⊢ Module.Finite R M

Tactic:
exact Module.Finite.of_basis hs

Premises used: Module.Finite.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)
⊢ Module.Finite 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)
⊢ Module.Finite R M

Tactic:
classical 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
inst_3 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
⊢ Module.Finite R M

Tactic:
simp [finite_of_det_ne_one (f := f), hf]

Premises used: LinearMap.finite_of_det_ne_one
-- 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 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
⊢ Module.Finite R M

Tactic:
have : Module.Finite R M := by simp [finite_of_det_ne_one (f := f), hf]
-- 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 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this_1 : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
this : ∃ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) (0 : M) ∧ x ≠ 0
⊢ ⊥ < f.ker

Tactic:
simpa [bot_lt_iff_ne_bot, ker_eq_bot']

Premises used: bot_lt_iff_ne_bot, LinearMap.ker_eq_bot'
-- 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 : IsDomain R
inst_4 : Free R M
f : M →ₗ[R] M
hf : Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (0 : R)
this : Module.Finite R M
b : Basis (Fin (finrank R M)) R M := finBasis R M
suffices : ∃ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) (0 : M) ∧ x ≠ 0
⊢ ⊥ < f.ker

Tactic:
suffices ∃ x, f x = 0 ∧ x ≠ 0 by simpa [bot_lt_iff_ne_bot, ker_eq_bot']