awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ 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)
have 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))
Tactic: rw [det_eq_det_toMatrix_of_finset b.reindexFinsetRange,
    det_toMatrix_eq_det_toMatrix b b.reindexFinsetRange]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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))
⊢ 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)
have 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))
Tactic: rw [det_eq_det_toMatrix_of_finset b.reindexFinsetRange,
    det_toMatrix_eq_det_toMatrix b b.reindexFinsetRange]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ (LinearMap.det : (a : M →ₗ[R] M) → R) ((toLin b b : (a : Matrix ι ι R) → M →ₗ[R] M) f : M →ₗ[R] M) = f.det
have 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
Tactic: rw [← LinearMap.det_toMatrix b, LinearMap.toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ (LinearMap.det : (a : M →ₗ[R] M) → R) ((toLin b b : (a : Matrix ι ι R) → M →ₗ[R] M) f : M →ₗ[R] M) = f.det
have rw₁ : f.det = f.det
Tactic: rw [← LinearMap.det_toMatrix b, LinearMap.toMatrix_toLin]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
have obtain : ∀ (s : Finset M) (b : Basis (↥s) A M), P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
Tactic: obtain ⟨s, ⟨b⟩⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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 ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
have rw : P (det.{u_5, u_2} (n := ↥s) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix (↥s) (↥s) A) f))
Tactic: rw [← det_toMatrix b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
have rwa : P ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk sorry.some) else 1 : (a : M →ₗ[A] M) → A) f)
Tactic: rwa [LinearMap.det_def, dif_neg H]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
have rwa₁ : P ((1 : (a : M →ₗ[A] M) → A) f)
Tactic: rwa [LinearMap.det_def, dif_neg H]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
have if : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)), 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
have if₁ : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)), 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
have if : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)), 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ P ((LinearMap.det : (a : M →ₗ[A] M) → A) f)
have if₁ : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) A M)), 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (hypothesis)
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
⊢ (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)
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ (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)
have 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)
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ (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)
have 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)
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
have rcases : ∀ (s : Finset M) (hs : Basis (↥s) A M), Module.Finite A M
Tactic: rcases H with ⟨s, ⟨hs⟩⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (hypothesis)
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)
⊢ (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)
have this : Module.Finite A M
Tactic: have : Module.Finite A M := by
      rcases H with ⟨s, ⟨hs⟩⟩
      exact Module.Finite.of_basis hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (hypothesis)
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)
⊢ (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)
have this : finrank A M = 0
Tactic: have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ (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)
have 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)
Tactic: classical
      have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H
      simp [coe_det, H, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)
have haveI : ∀ (this : DecidableEq ι), Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)
Tactic: haveI := Classical.decEq ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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 ι
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)
have intro : ∀ (val : Fintype ι), Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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 ι
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)
have intro : Eq.{u_5 + 1} (α := A) (det.{u_5, u_7} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) 0)) 0
Tactic: rwa [← det_toMatrix b, map_zero, det_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)
have intro₁ : Eq.{u_5 + 1} (α := A) (det.{u_5, u_7} (n := ι) 0) 0
Tactic: rwa [← det_toMatrix b, map_zero, det_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) 0 : A) (0 : A)
have intro₂ : Eq.{u_5 + 1} (α := A) 0 0
Tactic: rwa [← det_toMatrix b, map_zero, det_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
have hnc : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
Tactic: rw [LinearMap.det, dif_neg, MonoidHom.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
have have : ∀ (b : Basis (Fin 0) R M), 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
have 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
Tactic: rw [← f.det_toMatrix b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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 : 𝕜)
have 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))
Tactic: refine @LinearMap.det_cases M _ 𝕜 _ _ _ (fun t => t = 1) f ?_ rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
have rw : Fintype.card.{u_8} ↥s = 0
Tactic: rw [← Fintype.card_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (hypothesis)
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
⊢ Eq.{u_7 + 1} (α := 𝕜) (det.{u_7, u_8} (n := ↥s) ((toMatrix b b : (a : M →ₗ[𝕜] M) → Matrix (↥s) (↥s) 𝕜) f)) 1
have this : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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 : 𝕜)
have 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))
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ Eq.{u_7 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) f : 𝕜) (1 : 𝕜)
have 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
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ 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)
have 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)
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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)
⊢ 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)
have 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)
Tactic: rcases H with ⟨s, ⟨b⟩⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
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
⊢ 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)
have 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
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]