awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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.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 [← 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]
-- 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
⊢ 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
have 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)
Tactic: rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
-- 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
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)
⊢ 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
have 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)
Tactic: rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
-- 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
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)
⊢ 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
have 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)
Tactic: rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
-- 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
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)
⊢ 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
have 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)
Tactic: rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
-- 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
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)
⊢ 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
have pos₄ : Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) 1 1
Tactic: rw [← toMatrix_comp, LinearEquiv.comp_coe, e.symm_trans_self, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
-- 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
⊢ 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
have 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)
Tactic: rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
-- 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
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)
⊢ 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
have 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)
Tactic: rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
-- 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
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)
⊢ 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
have 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)
Tactic: rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
-- 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
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)
⊢ 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
have 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)
Tactic: rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
-- 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
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)
⊢ 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
have pos₄ : Eq (α := Matrix.{u_2, u_2, u_5} (↥s) (↥s) A) 1 1
Tactic: rw [← toMatrix_comp, LinearEquiv.comp_coe, e.self_trans_symm, LinearEquiv.refl_toLinearMap,
          toMatrix_id]
-- 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)
⊢ ¬∃ (t : Finset N), Nonempty (Basis (↥t) A N)
have contrapose : ∀ (H : ∃ (t : Finset N), Nonempty (Basis (↥t) A N)), ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
Tactic: contrapose 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
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)
⊢ ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
have rcases : ∀ (s : Finset N) (b : Basis (↥s) A N), ∃ (s : Finset M), Nonempty (Basis (↥s) A M)
Tactic: rcases H with ⟨s, ⟨b⟩⟩
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
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 H' : ¬∃ (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⟩⟩
-- 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: 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]
-- 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: 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]
-- 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 : 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
⊢ IsUnit f ↔ IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: rw [← isUnit_toMatrix_iff b, ← det_toMatrix b, Matrix.isUnit_iff_isUnit_det (toMatrix b b f)]
-- 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 : 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)
⊢ IsUnit f ↔ IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
have 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))
Tactic: rw [← isUnit_toMatrix_iff b, ← det_toMatrix b, Matrix.isUnit_iff_isUnit_det (toMatrix b b f)]