awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
n : Type u_7
inst_1 : Fintype n
inst_2 : DecidableEq n
M N : Matrix n n A
rw : M.det * N.det = (N * M).det
rw₁ : M.det * N.det = N.det * M.det
⊢ (M * N).det = (N * M).det
have rw₂ : N.det * M.det = N.det * M.det
Tactic: rw [det_mul, det_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (hypothesis)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M * N).det = (N * M).det
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
h : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
⊢ (M * N).det = (N * M).det
have rw : (M * N).det = det.{u_5, u_7} (n := n) ((N * M).submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m))
Tactic: rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
    submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
h : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
rw : (M * N).det = det.{u_5, u_7} (n := n) ((N * M).submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m))
⊢ (M * N).det = (N * M).det
have rw₁ : (M * N).det =
  (HMul.hMul (α := Matrix n n A) (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
      (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))).det
Tactic: rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
    submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
h : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
rw : (M * N).det = det.{u_5, u_7} (n := n) ((N * M).submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m))
rw₁ :
  (M * N).det =
    (HMul.hMul (α := Matrix n n A) (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
        (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))).det
⊢ (M * N).det = (N * M).det
have rw₂ : (M * N).det =
  (HMul.hMul (α := Matrix n n A) (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))
      (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))).det
Tactic: rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
    submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
h : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
rw : (M * N).det = det.{u_5, u_7} (n := n) ((N * M).submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m))
rw₁ :
  (M * N).det =
    (HMul.hMul (α := Matrix n n A) (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
        (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))).det
rw₂ :
  (M * N).det =
    (HMul.hMul (α := Matrix n n A) (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))
        (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))).det
⊢ (M * N).det = (N * M).det
have rw₃ : (M * N).det = det (n := n) ((M * N).submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑(Equiv.refl n) : (a : n) → n))
Tactic: rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
    submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
h : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
rw : (M * N).det = det.{u_5, u_7} (n := n) ((N * M).submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m))
rw₁ :
  (M * N).det =
    (HMul.hMul (α := Matrix n n A) (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
        (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))).det
rw₂ :
  (M * N).det =
    (HMul.hMul (α := Matrix n n A) (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))
        (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))).det
rw₃ : (M * N).det = det (n := n) ((M * N).submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑(Equiv.refl n) : (a : n) → n))
⊢ (M * N).det = (N * M).det
have rw₄ : (M * N).det = ((M * N).submatrix _root_.id _root_.id).det
Tactic: rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
    submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
h : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
rw : (M * N).det = det.{u_5, u_7} (n := n) ((N * M).submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m))
rw₁ :
  (M * N).det =
    (HMul.hMul (α := Matrix n n A) (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))
        (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))).det
rw₂ :
  (M * N).det =
    (HMul.hMul (α := Matrix n n A) (M.submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑e : (a : n) → m))
        (N.submatrix (⇑e : (a : n) → m) (⇑(Equiv.refl n) : (a : n) → n))).det
rw₃ : (M * N).det = det (n := n) ((M * N).submatrix (⇑(Equiv.refl n) : (a : n) → n) (⇑(Equiv.refl n) : (a : n) → n))
rw₄ : (M * N).det = ((M * N).submatrix _root_.id _root_.id).det
⊢ (M * N).det = (N * M).det
have rw₅ : (M * N).det = (M * N).det
Tactic: rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
    submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M * N * M').det = N.det
have rw : (M' * (M * N)).det = N.det
Tactic: rw [← det_comm' hM'M hMM', ← Matrix.mul_assoc, hM'M, Matrix.one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
rw : (M' * (M * N)).det = N.det
⊢ (M * N * M').det = N.det
have rw₁ : (M' * M * N).det = N.det
Tactic: rw [← det_comm' hM'M hMM', ← Matrix.mul_assoc, hM'M, Matrix.one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
rw : (M' * (M * N)).det = N.det
rw₁ : (M' * M * N).det = N.det
⊢ (M * N * M').det = N.det
have rw₂ : (1 * N).det = N.det
Tactic: rw [← det_comm' hM'M hMM', ← Matrix.mul_assoc, hM'M, Matrix.one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
m : Type u_6
n : Type u_7
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
M : Matrix m n A
M' : Matrix n m A
N : Matrix n n A
hMM' : M * M' = 1
hM'M : M' * M = 1
rw : (M' * (M * N)).det = N.det
rw₁ : (M' * M * N).det = N.det
rw₂ : (1 * N).det = N.det
⊢ (M * N * M').det = N.det
have rw₃ : N.det = N.det
Tactic: rw [← det_comm' hM'M hMM', ← Matrix.mul_assoc, hM'M, Matrix.one_mul]
-- 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
κ : Type u_6
inst_5 : Fintype κ
inst_6 : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ 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_6} (n := κ) ((toMatrix c c : (a : M →ₗ[A] M) → Matrix κ κ A) f))
have hMM' : HMul.hMul (α := Matrix κ ι A) (β := Matrix ι κ A) (c.toMatrix (⇑b : (a : ι) → M)) (b.toMatrix (⇑c : (a : κ) → M)) = 1
Tactic: rw [← linearMap_toMatrix_mul_basis_toMatrix c b c, ← basis_toMatrix_mul_linearMap_toMatrix b c b,
      Matrix.det_conj_of_mul_eq_one]
-- 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
κ : Type u_6
inst_5 : Fintype κ
inst_6 : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
hMM' :
  HMul.hMul (α := Matrix κ ι A) (β := Matrix ι κ A) (c.toMatrix (⇑b : (a : ι) → M)) (b.toMatrix (⇑c : (a : κ) → M)) = 1
⊢ 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_6} (n := κ) ((toMatrix c c : (a : M →ₗ[A] M) → Matrix κ κ A) f))
have hM'M : HMul.hMul (α := Matrix ι κ A) (β := Matrix κ ι A) (b.toMatrix (⇑c : (a : κ) → M)) (c.toMatrix (⇑b : (a : ι) → M)) = 1
Tactic: rw [← linearMap_toMatrix_mul_basis_toMatrix c b c, ← basis_toMatrix_mul_linearMap_toMatrix b c b,
      Matrix.det_conj_of_mul_eq_one]
-- 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
κ : Type u_6
inst_5 : Fintype κ
inst_6 : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ HMul.hMul (α := Matrix κ ι A) (β := Matrix ι κ A) (c.toMatrix (⇑b : (a : ι) → M)) (b.toMatrix (⇑c : (a : κ) → M)) = 1
have hMM' : Eq (α := Matrix κ κ A) (c.toMatrix (⇑c : (a : κ) → M)) 1
Tactic: rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]
-- 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
κ : Type u_6
inst_5 : Fintype κ
inst_6 : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
hMM' : Eq (α := Matrix κ κ A) (c.toMatrix (⇑c : (a : κ) → M)) 1
⊢ HMul.hMul (α := Matrix κ ι A) (β := Matrix ι κ A) (c.toMatrix (⇑b : (a : ι) → M)) (b.toMatrix (⇑c : (a : κ) → M)) = 1
have hMM'₁ : Eq (α := Matrix κ κ A) 1 1
Tactic: rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]
-- 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
κ : Type u_6
inst_5 : Fintype κ
inst_6 : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
⊢ HMul.hMul (α := Matrix ι κ A) (β := Matrix κ ι A) (b.toMatrix (⇑c : (a : κ) → M)) (c.toMatrix (⇑b : (a : ι) → M)) = 1
have hM'M : Eq (α := Matrix ι ι A) (b.toMatrix (⇑b : (a : ι) → M)) 1
Tactic: rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]
-- 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
κ : Type u_6
inst_5 : Fintype κ
inst_6 : DecidableEq κ
b : Basis ι A M
c : Basis κ A M
f : M →ₗ[A] M
hM'M : Eq (α := Matrix ι ι A) (b.toMatrix (⇑b : (a : ι) → M)) 1
⊢ HMul.hMul (α := Matrix ι κ A) (β := Matrix κ ι A) (b.toMatrix (⇑c : (a : κ) → M)) (c.toMatrix (⇑b : (a : ι) → M)) = 1
have hM'M₁ : Eq (α := Matrix ι ι A) 1 1
Tactic: rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]
-- 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
⊢ Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk b) : (a : M →ₗ[A] M) → A) f : A)
    (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f) : A)
have rw : Eq.{u_5 + 1} (α := A)
  ((Trunc.lift
          (fun (b : Basis ι A M) ↦ MonoidHom.comp detMonoidHom (↑(toMatrixAlgEquiv b) : (M →ₗ[A] M) →* Matrix ι ι A)) sorry
          (Trunc.mk b) :
        (a : M →ₗ[A] M) → A)
      f :
    A)
  (det.{u_5, u_4} (n := ι) ((toMatrix b b : (a : M →ₗ[A] M) → Matrix ι ι A) f) : A)
Tactic: rw [detAux]
-- 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
ι' : Type u_7
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b' : Basis ι' A M
f : M →ₗ[A] M
b : Basis ι A M
⊢ Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk b) : (a : M →ₗ[A] M) → A) f : A)
    (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f) : A)
have h : 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_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f))
Tactic: rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']
-- 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
ι' : Type u_7
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b' : Basis ι' A M
f : M →ₗ[A] M
b : Basis ι A M
h :
  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_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f))
⊢ Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk b) : (a : M →ₗ[A] M) → A) f : A)
    (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f) : A)
have h₁ : Eq.{u_5 + 1} (α := A) (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f))
  (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f))
Tactic: rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']
-- 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
ι' : Type u_7
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
tb : Trunc (Basis ι A M)
b' : Basis ι' A M
f : M →ₗ[A] M
⊢ Eq.{u_5 + 1} (α := A) ((detAux tb : (a : M →ₗ[A] M) → A) f : A)
    (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f) : A)
have h : ∀ (b : Basis ι A M),
  Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk b) : (a : M →ₗ[A] M) → A) f : A)
    (det.{u_5, u_7} (n := ι') ((toMatrix b' b' : (a : M →ₗ[A] M) → Matrix ι' ι' A) f) : A)
Tactic: induction tb using Trunc.induction_on with
  | h b => rw [detAux_def', det_toMatrix_eq_det_toMatrix b b']
Cleared hypotheses: tb
-- 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
⊢ 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)
have 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 sorry.some) else 1 : (a : M →ₗ[A] M) → A) x :
      A)
Tactic: ext
-- 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
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)
have h : Eq.{u_5 + 1} (α := A)
  ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk sorry.some) else 1 : (a : M →ₗ[A] M) → A) x :
    A)
  ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk sorry.some) else 1 : (a : M →ₗ[A] M) → A) x :
    A)
Tactic: rw [LinearMap.det_def]
-- 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
x : M →ₗ[A] M
⊢ 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)
have pos : ∀ (h : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)),
  Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk sorry.some) : (a : M →ₗ[A] M) → A) x : A)
    ((detAux (Trunc.mk sorry.some) : (a : M →ₗ[A] M) → A) x : A)
Tactic: split_ifs
-- 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
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)
⊢ 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)
have 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)
Tactic: split_ifs
-- 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
f : M →ₗ[R] M
hf : Ne.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) (1 : R)
⊢ Free R M
have pos : ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Free R M
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Module.Basis s R 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
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
⊢ Free R M
have neg : ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)), Free R M
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Module.Basis s R 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
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
have pos : ∀ (s : Finset M) (hs : Basis (↥s) R M), Free R 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 : DecidableEq M
s : Finset M
b : Basis (↥s) A M
f : M →ₗ[A] M
⊢ 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)
have this : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
Tactic: have : ∃ s : Finset M, Nonempty (Basis s A M) := ⟨s, ⟨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
s : Finset M
b : Basis (↥s) A M
f : M →ₗ[A] M
this : ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
⊢ 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)
have rw : Eq.{u_5 + 1} (α := A)
  ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) A M) then detAux (Trunc.mk sorry.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)
Tactic: rw [LinearMap.coe_det, dif_pos this, detAux_def'' _ 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
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)
⊢ 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)
have rw₁ : Eq.{u_5 + 1} (α := A) ((detAux (Trunc.mk sorry.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)
Tactic: rw [LinearMap.coe_det, dif_pos this, detAux_def'' _ 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
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)
⊢ 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)
have 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))
Tactic: rw [LinearMap.coe_det, dif_pos this, detAux_def'' _ b]
-- 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
⊢ 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 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)
Tactic: haveI := Classical.decEq M