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
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
⊢ Eq (α := Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
    ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (j : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (j : ι) ↦ M) i) :
      Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
    (blockDiagonal fun (i : ι) ↦
        (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i) :
      Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)

Tactic:
have : ((LinearMap.toMatrix B B) (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)) =
      Matrix.blockDiagonal (fun i ↦ LinearMap.toMatrix b b (f i)) := by
    ext ⟨i₁, i₂⟩ ⟨j₁, j₂⟩
    unfold B
    simp_rw [LinearMap.toMatrix_apply', Matrix.blockDiagonal_apply, Basis.coe_reindex,
      Function.comp_apply, Basis.repr_reindex_apply, Equiv.symm_trans_apply, Equiv.prodComm_symm,
      Equiv.prodComm_apply, Equiv.sigmaEquivProd_symm_apply, Prod.swap_prod_mk, Pi.basis_apply,
      Pi.basis_repr, LinearMap.pi_apply, LinearMap.coe_comp, Function.comp_apply,
      LinearMap.toMatrix_apply', LinearMap.coe_proj, Function.eval, Pi.single_apply]
    split_ifs with h
    · rw [h]
    · simp only [map_zero, Finsupp.coe_zero, Pi.zero_apply]
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : Fintype ι
inst_4 : Free R M
inst_5 : Module.Finite R M
f : ι → M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
B : Basis (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R ((j : ι) → M) :=
  Basis.reindex (Pi.basis (ιs := fun (x : ι) ↦ Free.ChooseBasisIndex R M) (Ms := fun (x : ι) ↦ M) fun (x : ι) ↦ b)
    (Equiv.trans (Equiv.sigmaEquivProd ι (Free.ChooseBasisIndex R M)) (Equiv.prodComm ι (Free.ChooseBasisIndex R M)))
this :
  Eq (α := Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
    ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (j : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (j : ι) ↦ M) i) :
      Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
    (blockDiagonal fun (i : ι) ↦
        (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i) :
      Matrix (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) (Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι) R)
rw :
  Eq.{u_1 + 1} (α := R)
    (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
      (blockDiagonal fun (i : ι) ↦
        (toMatrix b b : (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R) (f i)))
    (∏ x : ι,
      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 x)))
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R)
    (∏ k : ι,
      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 k)))
    (∏ x : ι,
      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 x)))
⊢ Eq.{u_1 + 1} (α := R)
    (det (n := Prod.{u_2, u_4} (Free.ChooseBasisIndex R M) ι)
      ((toMatrix B B :
          (a : ((j : ι) → M) →ₗ[R] (j : ι) → M) →
            Matrix (Free.ChooseBasisIndex R M × ι) (Free.ChooseBasisIndex R M × ι) R)
        (pi (φ := fun (i : ι) ↦ M) fun (i : ι) ↦ f i ∘ₗ proj (φ := fun (i : ι) ↦ M) i)))
    (∏ x : ι,
      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 x)))

Tactic:
rw [this, Matrix.det_blockDiagonal]

Premises used: Matrix.det_blockDiagonal
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_5
S : Type u_6
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Free R S
x : R
rw :
  ((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      (HSMul.hSMul (β := End R S) x 1) =
    x ^ finrank R S
rw₁ :
  HMul.hMul (β := R) (x ^ finrank R S)
      (((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R) 1 :
        R) =
    x ^ finrank R S
rw₂ : x ^ finrank R S * 1 = x ^ finrank R S
rw₃ rw₄ : x ^ finrank R S = x ^ finrank R S
⊢ ((LinearMap.det.{u_6, u_5} (M := S) (A := R) : MonoidHom.{u_6, u_5} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      ((lsmul R R S : (a : R) → End R S) x : End R S) =
    x ^ finrank R S

Tactic:
rw [lsmul_eq_smul_one, LinearMap.det_smul, map_one, mul_one]

Premises used: map_one, LinearMap.det_smul, Algebra.lsmul_eq_smul_one, mul_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
f : M ≃ₗ[R] M
⊢ Eq.{u_1 + 1} (α := R) ((↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M ≃ₗ[R] M
⊢ Eq.{u_1 + 1} (α := R) ((↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f)⁻¹ : R) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f.symm : M →ₗ[R] M) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) (refl R M) : Rˣ) (1 : Rˣ)

Tactic:
Units.ext <| LinearMap.det_id

Premises used: Units.ext, LinearMap.det_id
-- 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 g : M ≃ₗ[R] M
⊢ (LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) (f ≪≫ₗ g) =
    HMul.hMul (α := Rˣ) (β := Rˣ) ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) g : Rˣ)
      ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ)

Tactic:
map_mul _ g f

Premises used: map_mul
-- 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
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f.symm : Rˣ)
    ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f⁻¹ : Rˣ)

Tactic:
map_inv _ f

Premises used: map_inv
-- 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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f : M ≃ₗ[R] M
e : M ≃ₗ[R] M'
rw :
  Eq.{u_1 + 1} (α := R) (↑((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e)) : R)
    (↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
    ((↑((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) : R) : R)
rw₂ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M' →ₗ[R] M') → R) (↑(e.symm ≪≫ₗ f ≪≫ₗ e) : M' →ₗ[R] M') : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
rw₃ :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : M' →ₗ[R] M') → R) ((↑e : M →ₗ[R] M') ∘ₗ (↑(e.symm ≪≫ₗ f) : M' →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
rw₄ :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : M' →ₗ[R] M') → R) ((↑e : M →ₗ[R] M') ∘ₗ (↑f : M →ₗ[R] M) ∘ₗ (↑e.symm : M' →ₗ[R] M)) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
rw₅ rw₆ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) (↑f : M →ₗ[R] M) : R)
⊢ Eq.{u_1 + 1} (α := Rˣ) ((LinearEquiv.det : (a : M' ≃ₗ[R] M') → Rˣ) (e.symm ≪≫ₗ f ≪≫ₗ e) : Rˣ)
    ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f : Rˣ)

Tactic:
rw [← Units.val_inj, coe_det, coe_det, ← comp_coe, ← comp_coe, LinearMap.det_conj]

Premises used: Units.val_inj, LinearEquiv.comp_coe, LinearMap.det_conj, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
K : Type u_5
V : Type u_6
W : Type u_7
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup W
inst_4 : Module K W
F : Type u_8
inst_5 : EquivLike.{u_8 + 1, u_6 + 1, u_7 + 1} F (End K V) (End K W)
inst_6 : AlgEquivClass F K (End K V) (End K W)
f : F
x : End K V
w : V ≃ₗ[K] W
h : Eq (α := AlgEquiv.{u_5, u_6, u_7} K (End K V) (End K W)) (↑f : End K V ≃ₐ[K] End K W) (LinearEquiv.conjAlgEquiv K w)
⊢ Eq.{u_7 + 1} (α := End K W) ((f : (a : End K V) → End K W) x : End K W)
    (((LinearEquiv.conjAlgEquiv K w : AlgEquiv.{u_5, u_6, u_7} K (End K V) (End K W)) : (a : End K V) → End K W) x :
      End K W)

Tactic:
simpa using congr($h x)
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
K : Type u_5
m : Type u_6
n : Type u_7
inst : Field K
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
F : Type u_8
inst_5 : EquivLike F (Matrix m m K) (Matrix n n K)
inst_6 : AlgEquivClass F K (Matrix m m K) (Matrix n n K)
f : F
x : Matrix m m K
⊢ det.{u_5, u_7} (n := n) ((f : (a : Matrix m m K) → Matrix n n K) x) = x.det

Tactic:
simpa [toMatrixAlgEquiv', Matrix.toLinAlgEquiv'] using
    LinearMap.det_map ((Matrix.toLinAlgEquiv'.symm.trans
      (AlgEquivClass.toAlgEquiv f)).trans Matrix.toLinAlgEquiv') x.toLin'

Premises used: AlgEquiv.symm, Matrix.toLin', LinearMap.toMatrixAlgEquiv', AlgEquivClass.toAlgEquiv, LinearMap.det_map, AlgEquiv.trans, Matrix.toLinAlgEquiv', DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
A : Type u_5
inst_1 : CommRing A
inst_2 : Module A M
f : M ≃ₗ[A] M
⊢ HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑f : M →ₗ[A] M) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑f.symm : M →ₗ[A] M) : A) =
    1

Tactic:
simp [← LinearMap.det_comp]

Premises used: LinearMap.det_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
f : M ≃ₗ[A] M
⊢ HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑f.symm : M →ₗ[A] M) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑f : M →ₗ[A] M) : A) =
    1

Tactic:
simp [← LinearMap.det_comp]

Premises used: LinearMap.det_comp
-- 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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h :
  HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
      ((toMatrix v' v : (a : M' →ₗ[R] M) → Matrix ι ι R) (↑f.symm : M' →ₗ[R] M) : Matrix ι ι R)
      ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) (↑f : M →ₗ[R] M') : Matrix ι ι R) =
    1
B : Matrix ι ι R
⊢ IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) (↑f : M →ₗ[R] M')))

Tactic:
apply isUnit_det_of_left_inverse

Premises used: Matrix.isUnit_det_of_left_inverse
-- 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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
f : M ≃ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
⊢ Matrix ι ι R

Tactic:
simpa using (LinearMap.toMatrix_comp v v' v f.symm f).symm

Premises used: LinearEquiv.symm, LinearEquiv.toLinearMap, LinearMap.toMatrix_comp, Eq.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
f : M ≃ₗ[A] M
⊢ IsUnit.{u_5} (M := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑f : M →ₗ[A] M) : A)

Tactic:
.of_mul_eq_one _ f.det_mul_det_symm

Premises used: IsUnit.of_mul_eq_one, LinearEquiv.det_mul_det_symm
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
𝕜 : Type u_5
inst_1 : Field 𝕜
inst_2 : Module 𝕜 M
f : M ≃ₗ[𝕜] M
⊢ Eq.{u_5 + 1} (α := 𝕜) ((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) (↑f.symm : M →ₗ[𝕜] M) : 𝕜)
    (((LinearMap.det : (a : M →ₗ[𝕜] M) → 𝕜) (↑f : M →ₗ[𝕜] M))⁻¹ : 𝕜)

Tactic:
simp [field, IsUnit.ne_zero f.isUnit_det']

Premises used: LinearEquiv.isUnit_det', IsUnit.ne_zero
-- 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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M
rw :
  Eq.{u_2 + 1} (α := M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
    (((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ ∘ₗ
            (toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) :
          (a : M) → M)
        x :
      M)
rw₁ :
  Eq.{u_2 + 1} (α := M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
    (((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ ∘ₗ f :
          (a : M) → M)
        x :
      M)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
⊢ Eq.{u_2 + 1} (α := M)
    ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
            M' →ₗ[R] M) :
          (a : M') → M)
        ((f : (a : M) → M') x : M') :
      M)
    ((((toLin v v : (a : Matrix ι ι R) → M →ₗ[R] M)
              (HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
                (((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ : Matrix ι ι R)
                ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f : Matrix ι ι R)) :
            M →ₗ[R] M) :
          (a : M) → M)
        x :
      M)

Tactic:
rw [toLin_mul v v' v, toLin_toMatrix, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, Matrix.toLin_mul, Matrix.toLin_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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M
⊢ (((toLin v v : (a : Matrix ι ι R) → M →ₗ[R] M)
            (HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
              (((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ : Matrix ι ι R)
              ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f : Matrix ι ι R)) :
          M →ₗ[R] M) :
        (a : M) → M)
      x =
    x

Tactic:
simp [h]
-- 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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M'
rw :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
    (((toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) ∘ₗ
            (toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
          (a : M') → M')
        x :
      M')
rw₁ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
    ((((toLin v v' : (a : Matrix ι ι R) → M →ₗ[R] M') ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f) :
            M →ₗ[R] M') :
          (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
⊢ Eq.{u_3 + 1} (α := M')
    ((f : (a : M) → M')
        ((((toLin v' v : (a : Matrix ι ι R) → M' →ₗ[R] M) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ :
                M' →ₗ[R] M) :
              (a : M') → M)
            x :
          M) :
      M')
    ((((toLin v' v' : (a : Matrix ι ι R) → M' →ₗ[R] M')
              (HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
                ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f : Matrix ι ι R)
                (((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ : Matrix ι ι R)) :
            M' →ₗ[R] M') :
          (a : M') → M')
        x :
      M')

Tactic:
rw [toLin_mul v' v v', LinearMap.comp_apply, toLin_toMatrix v v']

Premises used: LinearMap.comp_apply, Matrix.toLin_mul, Matrix.toLin_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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M'
⊢ (((toLin v' v' : (a : Matrix ι ι R) → M' →ₗ[R] M')
            (HMul.hMul (α := Matrix ι ι R) (β := Matrix ι ι R)
              ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f : Matrix ι ι R)
              (((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f)⁻¹ : Matrix ι ι R)) :
          M' →ₗ[R] M') :
        (a : M') → M')
      x =
    x

Tactic:
simp [h]
-- 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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
h₁ :
  ∀ (x : M),
    Eq.{u_3 + 1} (α := M') (((↑(ofIsUnitDet h) : M →ₗ[R] M') : (a : M) → M') x : M') ((f : (a : M) → M') x : M')
⊢ (↑(ofIsUnitDet h) : M →ₗ[R] M') = f

Tactic:
ext x
-- 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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
f : M →ₗ[R] M'
v : Basis ι R M
v' : Basis ι R M'
h : IsUnit.{u_1} (M := R) (det.{u_1, u_4} (n := ι) ((toMatrix v v' : (a : M →ₗ[R] M') → Matrix ι ι R) f))
x : M
⊢ Eq.{u_3 + 1} (α := M') (((↑(ofIsUnitDet h) : M →ₗ[R] M') : (a : M) → M') x : M') ((f : (a : M) → M') x : M')

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
pos : (hR : Nontrivial R) → M ≃ₗ[R] M
neg : (hR : ¬Nontrivial R) → M ≃ₗ[R] M
⊢ M ≃ₗ[R] M

Tactic:
by_cases hR : Nontrivial R

Premises used: Nontrivial
-- 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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
e : Basis ι R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : Nontrivial R
pos : (ι : Type u_2) → (b : Basis ι R M) → M ≃ₗ[R] M
⊢ M ≃ₗ[R] M

Tactic:
let ⟨ι, b⟩ := (Module.Free.exists_basis R M).some
-- 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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι_1 : Type u_4
inst_5 : DecidableEq ι_1
inst_6 : Fintype ι_1
e : Basis ι_1 R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
⊢ Finite ι

Tactic:
have : Finite ι := Module.Finite.finite_basis b
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι_1 : Type u_4
inst_5 : DecidableEq ι_1
inst_6 : Fintype ι_1
e : Basis ι_1 R M
inst_7 : Free R M
inst_8 : Module.Finite R M
f : M →ₗ[R] M
h : IsUnit.{u_1} (M := R) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
hR : Nontrivial R
ι : Type u_2
b : Basis ι R M
this : Finite ι
pos : (this : Fintype ι) → M ≃ₗ[R] M
⊢ M ≃ₗ[R] M

Tactic:
have : Fintype ι := Fintype.ofFinite ι