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 : DecidableEq ι
inst_4 : Fintype ι
ι' : Type u_6
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
rw : ((b.reindex e).toMatrix v).det = (b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι'))
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (Matrix.det.{u_1, u_6} (n := ι')
        ((reindexAlgEquiv R R e : (a : Matrix ι ι R) → Matrix ι' ι' R) (b.toMatrix (v ∘ (⇑e : (a : ι) → ι')))) :
      R)
    ((b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι')) : R)
rw₂ : Matrix.det (b.toMatrix (v ∘ (⇑e : (a : ι) → ι'))) = (b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι'))
rw₃ rw₄ : Matrix.det (b.toMatrix (v ∘ (⇑e : (a : ι) → ι'))) = Matrix.det (b.toMatrix (v ∘ (⇑e : (a : ι) → ι')))
⊢ Eq.{u_1 + 1} (α := R) (((b.reindex e).det : (a : ι' → M) → R) v : R)
    ((b.det : (a : ι → M) → R) (v ∘ (⇑e : (a : ι) → ι')) : R)

Tactic:
rw [det_apply, toMatrix_reindex', det_reindexAlgEquiv, det_apply]

Premises used: Matrix.det_reindexAlgEquiv, Module.Basis.toMatrix_reindex', Module.Basis.det_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 : DecidableEq ι
inst_4 : Fintype ι
ι' : Type u_6
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b : Basis ι R M
e : ι ≃ ι'
⊢ (b.reindex e).det = AlternatingMap.domDomCongr e b.det

Tactic:
AlternatingMap.ext fun _ => det_reindex _ _ _

Premises used: Module.Basis.det_reindex, AlternatingMap.ext
-- 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 : DecidableEq ι
inst_4 : Fintype ι
ι' : Type u_6
inst_5 : Fintype ι'
inst_6 : DecidableEq ι'
b : Basis ι R M
v : ι → M
e : ι' ≃ ι
rw :
  Eq.{u_1 + 1} (α := R)
    ((b.det : (a : ι → M) → R)
        (Function.comp.{u_4 + 1, u_6 + 1, u_2 + 1} (β := ι') (v ∘ (⇑e : (a : ι') → ι)) (⇑e.symm : (a : ι) → ι')) :
      R)
    ((b.det : (a : ι → M) → R) v : R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    ((b.det : (a : ι → M) → R)
        (v ∘ Function.comp.{u_4 + 1, u_6 + 1, u_4 + 1} (β := ι') (⇑e : (a : ι') → ι) (⇑e.symm : (a : ι) → ι')) :
      R)
    ((b.det : (a : ι → M) → R) v : R)
rw₂ : Eq.{u_1 + 1} (α := R) ((b.det : (a : ι → M) → R) (v ∘ _root_.id) : R) ((b.det : (a : ι → M) → R) v : R)
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) ((b.det : (a : ι → M) → R) v : R) ((b.det : (a : ι → M) → R) v : R)
⊢ Eq.{u_1 + 1} (α := R) (((b.reindex e.symm).det : (a : ι' → M) → R) (v ∘ (⇑e : (a : ι') → ι)) : R)
    ((b.det : (a : ι → M) → R) v : R)

Tactic:
rw [det_reindex, Function.comp_assoc, e.self_comp_symm, Function.comp_id]

Premises used: Function.comp_id, Module.Basis.det_reindex, Equiv.self_comp_symm, Function.comp_assoc
-- 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 ι
b : Basis ι R M
f : M ≃ₗ[R] M'
v : ι → M'
rw : ((b.map f).toMatrix v).det = (b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v)
rw₁ : (b.toMatrix ((⇑f.symm : (a : M') → M) ∘ v)).det = (b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v)
rw₂ rw₃ : (b.toMatrix ((⇑f.symm : (a : M') → M) ∘ v)).det = (b.toMatrix ((⇑f.symm : (a : M') → M) ∘ v)).det
⊢ Eq.{u_1 + 1} (α := R) (((b.map f).det : (a : ι → M') → R) v : R)
    ((b.det : (a : ι → M) → R) ((⇑f.symm : (a : M') → M) ∘ v) : R)

Tactic:
rw [det_apply, toMatrix_map, det_apply]

Premises used: Module.Basis.toMatrix_map, Module.Basis.det_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
M' : Type u_3
inst_3 : AddCommGroup M'
inst_4 : Module R M'
ι : Type u_4
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
f : M ≃ₗ[R] M'
⊢ (b.map f).det = b.det.compLinearMap (↑f.symm : M' →ₗ[R] M)

Tactic:
AlternatingMap.ext <| b.det_map f

Premises used: AlternatingMap.ext, Module.Basis.det_map
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
H :
  ∀ (M : ι → ι → R),
    Eq.{u_1 + 1} (α := R)
      (((Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R) : (a : ι → ι → R) → R) M : R)
      ((detRowAlternating : (a : ι → ι → R) → R) M : R)
⊢ Eq (α := (ι → R) [⋀^ι]→ₗ[R] R) (Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R)
    (detRowAlternating : (ι → R) [⋀^ι]→ₗ[R] R)

Tactic:
ext M
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
M : ι → ι → R
H : (Basis.toMatrix (basisFun R ι) M).det = (detRowAlternating : (a : ι → ι → R) → R) M
H₁ : Mᵀ.det = (detRowAlternating : (a : ι → ι → R) → R) M
H₂ : det M = (detRowAlternating : (a : ι → ι → R) → R) M
H₃ H₄ :
  Eq.{u_1 + 1} (α := R) ((detRowAlternating : (a : ι → ι → R) → R) M : R)
    ((detRowAlternating : (a : ι → ι → R) → R) M : R)
⊢ Eq.{u_1 + 1} (α := R)
    (((Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R) : (a : ι → ι → R) → R) M : R)
    ((detRowAlternating : (a : ι → ι → R) → R) M : R)

Tactic:
rw [Basis.det_apply, Basis.coePiBasisFun.toMatrix_eq_transpose, det_transpose, det]

Premises used: Matrix.det_transpose, Module.Basis.coePiBasisFun.toMatrix_eq_transpose, Matrix.det, Module.Basis.det_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
v : ι → ι → R
rw :
  Eq.{u_1 + 1} (α := R) ((detRowAlternating : (a : ι → ι → R) → R) v : R)
    (det.{u_1, u_4} (n := ι) ((of : (a : ι → ι → R) → Matrix ι ι R) v) : R)
⊢ Eq.{u_1 + 1} (α := R)
    (((Basis.det (R := R) (M := ι → R) (ι := ι) (basisFun R ι) : (ι → R) [⋀^ι]→ₗ[R] R) : (a : ι → ι → R) → R) v : R)
    (det.{u_1, u_4} (n := ι) ((of : (a : ι → ι → R) → Matrix ι ι R) v) : R)

Tactic:
rw [Pi.basisFun_det]

Premises used: Pi.basisFun_det
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : Fintype ι
v : ι → ι → R
⊢ Eq.{u_1 + 1} (α := R) ((detRowAlternating : (a : ι → ι → R) → R) v : R)
    (det.{u_1, u_4} (n := ι) ((of : (a : ι → ι → R) → Matrix ι ι R) v) : R)

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
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i : ι
apply :
  ∀ (i_1 : ι),
    Eq.{u_1 + 1} (α := R)
      ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) : (a : M) → R)
          ((Basis.mk hli hsp : (a : ι) → M) i_1 : M) :
        R)
      (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i : (a : M) → R)
          ((Basis.mk hli hsp : (a : ι) → M) i_1 : M) :
        R)
⊢ HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) =
    (↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i

Tactic:
apply (Basis.mk hli hsp).ext

Premises used: Module.Basis.mk, Module.Basis.ext
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i k : ι
inl :
  Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord k) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v k : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
inr :
  ∀ (hik : k ≠ i),
    Eq.{u_1 + 1} (α := R)
      ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) : (a : M) → R)
          ((Basis.mk hli hsp : (a : ι) → M) k : M) :
        R)
      (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i : (a : M) → R)
          ((Basis.mk hli hsp : (a : ι) → M) k : M) :
        R)
⊢ Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)

Tactic:
rcases eq_or_ne k i with (rfl | hik)

Premises used: eq_or_ne, 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
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
k : ι
inl :
  HMul.hMul (α := R) (β := R) ((e.det : (a : ι → M) → R) v : R) (((Basis.mk hli hsp).coord k : (a : M) → R) (v k) : R) =
    ((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) (update (β := fun (x : ι) ↦ M) v k (v k))
⊢ Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord k) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v k : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)

Tactic:
simp only [smul_eq_mul, coe_mk, LinearMap.smul_apply,
      MultilinearMap.toLinearMap_apply]

Premises used: LinearMap.smul_apply, Module.Basis.coe_mk, smul_eq_mul, MultilinearMap.toLinearMap_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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i k : ι
hik : k ≠ i
inr :
  HMul.hMul (α := R) (β := R) ((e.det : (a : ι → M) → R) v : R) (((Basis.mk hli hsp).coord i : (a : M) → R) (v k) : R) =
    ((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) (update (β := fun (x : ι) ↦ M) v i (v k))
⊢ Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((e.det : (a : ι → M) → R) v : R) ((Basis.mk hli hsp).coord i) : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R).toLinearMap (M₁ := fun (x : ι) ↦ M) v i : (a : M) → R)
        ((Basis.mk hli hsp : (a : ι) → M) k : M) :
      R)

Tactic:
simp only [smul_eq_mul, coe_mk, LinearMap.smul_apply,
      MultilinearMap.toLinearMap_apply]

Premises used: LinearMap.smul_apply, Module.Basis.coe_mk, smul_eq_mul, MultilinearMap.toLinearMap_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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
k : ι
inl :
  Eq.{u_1 + 1} (α := R) ((e.det : (a : ι → M) → R) v : R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) v : R)
⊢ HMul.hMul (α := R) (β := R) ((e.det : (a : ι → M) → R) v : R) (((Basis.mk hli hsp).coord k : (a : M) → R) (v k) : R) =
    ((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) (update (β := fun (x : ι) ↦ M) v k (v k))

Tactic:
rw [mk_coord_apply_eq, mul_one, update_eq_self]

Premises used: Function.update_eq_self, Module.Basis.mk_coord_apply_eq, 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
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
k : ι
⊢ Eq.{u_1 + 1} (α := R) ((e.det : (a : ι → M) → R) v : R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) v : R)

Tactic:
congr
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i k : ι
hik : k ≠ i
inr :
  Eq.{u_1 + 1} (α := R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R)
        (update (β := fun (x : ι) ↦ M) v i (v k)) :
      R)
    (0 : R)
⊢ HMul.hMul (α := R) (β := R) ((e.det : (a : ι → M) → R) v : R) (((Basis.mk hli hsp).coord i : (a : M) → R) (v k) : R) =
    ((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R) (update (β := fun (x : ι) ↦ M) v i (v k))

Tactic:
rw [mk_coord_apply_ne hik, mul_zero, eq_comm]

Premises used: Module.Basis.mk_coord_apply_ne, eq_comm, MulZeroClass.mul_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
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i k : ι
hik : k ≠ i
⊢ update (β := fun (x : ι) ↦ M) v i (v k) k = update (β := fun (x : ι) ↦ M) v i (v k) i

Tactic:
simp [hik]
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hsp : LE.le (α := Submodule R M) ⊤ (span R (Set.range v))
i k : ι
hik : k ≠ i
⊢ Eq.{u_1 + 1} (α := R)
    (((↑e.det : MultilinearMap R (fun (x : ι) ↦ M) R) : (a : (i : ι) → M) → R)
        (update (β := fun (x : ι) ↦ M) v i (v k)) :
      R)
    (0 : R)

Tactic:
exact e.det.map_eq_zero_of_eq _ (by simp [hik]) hik

Premises used: Module.Basis.det, AlternatingMap.map_eq_zero_of_eq
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
H :
  ∀ (f : ι → M),
    Eq.{u_1 + 1} (α := R) (((e.unitsSMul w).det : (a : ι → M) → R) f : R)
      ((HSMul.hSMul (α := R) (↑(∏ i : ι, w i)⁻¹ : R) e.det : (a : ι → M) → R) f : R)
⊢ (e.unitsSMul w).det = HSMul.hSMul (α := R) (↑(∏ i : ι, w i)⁻¹ : R) e.det

Tactic:
ext f
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
H :
  (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦
      ((((e.unitsSMul w).repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i) =
    HSMul.hSMul (α := R) (β := R) (↑(∏ i : ι, w i)⁻¹ : R)
      (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i)
⊢ Eq.{u_1 + 1} (α := R) (((e.unitsSMul w).det : (a : ι → M) → R) f : R)
    ((HSMul.hSMul (α := R) (↑(∏ i : ι, w i)⁻¹ : R) e.det : (a : ι → M) → R) f : R)

Tactic:
change
    (Matrix.det fun i j => (e.unitsSMul w).repr (f j) i) =
      (↑(∏ i, w i)⁻¹ : R) • Matrix.det fun i j => e.repr (f j) i

Premises used: Units.val, Finset.univ, Module.Basis.unitsSMul, Module.Basis.repr, Finset.prod, Inv.inv, DFunLike.coe, Matrix.det
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
ι : Type u_4
inst_3 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
H :
  (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦
      HSMul.hSMul (β := R) (w i)⁻¹ ((((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i : R)) =
    HSMul.hSMul (α := R) (β := R) (↑(∏ i : ι, w i)⁻¹ : R)
      (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i)
⊢ (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦
      ((((e.unitsSMul w).repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i) =
    HSMul.hSMul (α := R) (β := R) (↑(∏ i : ι, w i)⁻¹ : R)
      (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i)

Tactic:
simp only [e.repr_unitsSMul]

Premises used: Module.Basis.repr_unitsSMul
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ Matrix.det.{u_1, u_4} (n := ι)
      ((of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦
        HMul.hMul (β := R) (↑(w i)⁻¹ : R) ((((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i : R)) =
    HMul.hMul (α := R) (∏ i : ι, (↑(w i)⁻¹ : R))
      (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i)

Tactic:
Matrix.det_mul_column (fun i => (↑(w i)⁻¹ : R)) fun i j => e.repr (f j) i

Premises used: Units.val, Module.Basis.repr, Inv.inv, Matrix.det_mul_column, DFunLike.coe
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
h : Eq.{u_1 + 1} (α := R) (↑(∏ i : ι, w i)⁻¹ : R) (∏ i : ι, (↑(w i)⁻¹ : R))
⊢ (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦
      HSMul.hSMul (β := R) (w i)⁻¹ ((((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i : R)) =
    HSMul.hSMul (α := R) (β := R) (↑(∏ i : ι, w i)⁻¹ : R)
      (Matrix.det.{u_1, u_4} (n := ι) fun (i j : ι) ↦ (((e.repr : (a : M) → ι →₀ R) (f j) : ι →₀ R) : (a : ι) → R) i)

Tactic:
convert! Matrix.det_mul_column (fun i => (↑(w i)⁻¹ : R)) fun i j => e.repr (f j) i

Premises used: Units.val, Module.Basis.repr, Inv.inv, Matrix.det_mul_column, DFunLike.coe
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ Eq.{u_1 + 1} (α := R) (↑(∏ i : ι, w i)⁻¹ : R) (∏ i : ι, (↑(w i)⁻¹ : R))

Tactic:
simp [← Finset.prod_inv_distrib]

Premises used: Finset.prod_inv_distrib
-- 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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → Rˣ
⊢ Eq.{u_1 + 1} (α := R) ((e.det : (a : ι → M) → R) (⇑(e.unitsSMul w) : (a : ι) → M) : R) (∏ i : ι, (↑(w i) : R) : R)

Tactic:
simp [det_apply]

Premises used: Module.Basis.det_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 : DecidableEq ι
inst_4 : Fintype ι
e : Basis ι R M
w : ι → R
hw : ∀ (i : ι), IsUnit (w i)
⊢ Eq.{u_1 + 1} (α := R) ((e.det : (a : ι → M) → R) (⇑(e.isUnitSMul hw) : (a : ι) → M) : R) (∏ i : ι, w i : R)

Tactic:
e.det_unitsSMul_self _

Premises used: Module.Basis.det_unitsSMul_self
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
have :
  ∀ (this : Fintype (Free.ChooseBasisIndex R M)),
    Eq.{u_1 + 1} (α := R)
      (((LinearMap.det (M := Dual R M) (A := R) : (Dual R M →ₗ[R] Dual R M) →* R) : (a : Dual R M →ₗ[R] Dual R M) → R)
          f.dualMap :
        R)
      ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.det (M := Dual R M) (A := R) : (Dual R M →ₗ[R] Dual R M) →* R) : (a : Dual R M →ₗ[R] Dual R M) → R)
        f.dualMap :
      R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)

Tactic:
have : Fintype (Module.Free.ChooseBasisIndex R M) :=
    Module.Free.ChooseBasisIndex.fintype R M
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
this : Fintype (Free.ChooseBasisIndex R M)
rw :
  Eq.{u_1 + 1} (α := R)
    (det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
      ((toMatrix b.dualBasis b.dualBasis :
          (a : Dual R M →ₗ[R] Dual R M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R)
        f.dualMap))
    (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))
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.det (M := Dual R M) (A := R) : (Dual R M →ₗ[R] Dual R M) →* R) : (a : Dual R M →ₗ[R] Dual R M) → R)
        f.dualMap :
      R)
    ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R)

Tactic:
rw [← LinearMap.det_toMatrix b, ← LinearMap.det_toMatrix b.dualBasis]

Premises used: Module.Basis.dualBasis, LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
this : Fintype (Free.ChooseBasisIndex R M)
⊢ Eq.{u_1 + 1} (α := R)
    (det.{u_1, u_2} (n := Free.ChooseBasisIndex R M)
      ((toMatrix b.dualBasis b.dualBasis :
          (a : Dual R M →ₗ[R] Dual R M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R)
        f.dualMap))
    (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:
simp [LinearMap.dualMap_def, LinearMap.toMatrix_transpose]

Premises used: LinearMap.toMatrix_transpose, LinearMap.dualMap_def