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 ι
e : Basis ι R M
v : ι → M
hli : LinearIndependent R v
hspan : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
v' : Basis ι R M := Basis.mk hli ⋯
h :
  ∀ (i j : ι),
    e.toMatrix v i j =
      (LinearMap.toMatrix v' e : (a : M →ₗ[R] M) → Matrix ι ι R) (↑(LinearEquiv.refl R M) : M →ₗ[R] M) i j
⊢ e.toMatrix v = (LinearMap.toMatrix v' e : (a : M →ₗ[R] M) → Matrix ι ι R) (↑(LinearEquiv.refl R M) : M →ₗ[R] M)

Tactic:
ext i j
-- 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
hspan : Eq (α := Submodule R M) (span R (Set.range v)) ⊤
v' : Basis ι R M := Basis.mk hli ⋯
i j : ι
⊢ e.toMatrix v i j =
    (LinearMap.toMatrix v' e : (a : M →ₗ[R] M) → Matrix ι ι R) (↑(LinearEquiv.refl R M) : M →ₗ[R] M) i j

Tactic:
simp [v']
-- 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
h : IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) v : R)
⊢ IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))

Tactic:
rw [Basis.det_apply, Basis.toMatrix_eq_toMatrix_constr] at h

Premises used: Module.Basis.toMatrix_eq_toMatrix_constr, 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
v : ι → M
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
⊢ let v' := e.map (LinearEquiv.ofIsUnitDet h);
  v' = e.map (LinearEquiv.ofIsUnitDet h)

Tactic:
set v' := Basis.map e (LinearEquiv.ofIsUnitDet h) with v'_def

Premises used: Module.Basis.map, LinearEquiv.ofIsUnitDet
-- 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
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
h₁ : ∀ (i : ι), (v' : (a : ι) → M) i = v i
⊢ (⇑v' : (a : ι) → M) = v

Tactic:
ext i
-- 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
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
i : ι
h₁ : (e.map (LinearEquiv.ofIsUnitDet h) : (a : ι) → M) i = v i
h₂ : (LinearEquiv.ofIsUnitDet h : (a : M) → M) ((e : (a : ι) → M) i : M) = v i
h₃ : (((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v : M →ₗ[R] M) : (a : M) → M) ((e : (a : ι) → M) i : M) = v i
h₄ h₅ : v i = v i
⊢ (v' : (a : ι) → M) i = v i

Tactic:
rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]

Premises used: Module.Basis.map_apply, Module.Basis.constr_basis, LinearEquiv.ofIsUnitDet_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
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
⊢ (⇑v' : (a : ι) → M) = v

Tactic:
have : ⇑v' = v := by
      ext i
      rw [v'_def, Basis.map_apply, LinearEquiv.ofIsUnitDet_apply, e.constr_basis]
-- 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
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
this : (⇑v' : (a : ι) → M) = v
mpr :
  LinearIndependent.{u_4, u_1, u_2} (ι := ι) R (M := M) (⇑v' : (a : ι) → M) ∧
    Eq.{u_2 + 1} (α := Submodule R M) (span R (Set.range.{u_2, u_4 + 1} (ι := ι) (⇑v' : (a : ι) → M))) ⊤
⊢ LinearIndependent R v ∧ Eq (α := Submodule R M) (span R (Set.range v)) ⊤

Tactic:
rw [← this]
-- 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
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
this : (⇑v' : (a : ι) → M) = v
⊢ LinearIndependent.{u_4, u_1, u_2} (ι := ι) R (M := M) (⇑v' : (a : ι) → M) ∧
    Eq.{u_2 + 1} (α := Submodule R M) (span R (Set.range.{u_2, u_4 + 1} (ι := ι) (⇑v' : (a : ι) → M))) ⊤

Tactic:
⟨v'.linearIndependent, v'.span_eq⟩

Premises used: Module.Basis.linearIndependent, And.intro, Module.Basis.span_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
v : ι → M
h :
  IsUnit.{u_1} (M := R)
    (Matrix.det.{u_1, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[R] M) → Matrix ι ι R) ((e.constr ℕ : (a : ι → M) → M →ₗ[R] M) v)))
v' : Basis ι R M := e.map (LinearEquiv.ofIsUnitDet h)
v'_def : v' = e.map (LinearEquiv.ofIsUnitDet h)
this : (⇑v' : (a : ι) → M) = v
⊢ LinearIndependent.{u_4, u_1, u_2} (ι := ι) R (M := M) (⇑v' : (a : ι) → M) ∧
    Eq.{u_2 + 1} (α := Submodule R M) (span R (Set.range.{u_2, u_4 + 1} (ι := ι) (⇑v' : (a : ι) → M))) ⊤

Tactic:
exact ⟨v'.linearIndependent, v'.span_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 e' : Basis ι R M
⊢ IsUnit.{u_1} (M := R) ((e.det : (a : ι → M) → R) (⇑e' : (a : ι) → M) : R)

Tactic:
(is_basis_iff_det e).mp ⟨e'.linearIndependent, e'.span_eq⟩

Premises used: Module.Basis.linearIndependent, And.intro, Iff.mp, Module.Basis.span_eq, Module.Basis.is_basis_iff_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
f : M [⋀^ι]→ₗ[R] R
⊢ f = HSMul.hSMul (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det

Tactic:
Basis.ext_alternating e fun i h => ?_

Premises used: Module.Basis.ext_alternating
-- 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
f : M [⋀^ι]→ₗ[R] R
refine :
  ∀ (i : ι → ι) (h : Injective i),
    Eq.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) fun (i_1 : ι) ↦ (e : (a : ι) → M) (i i_1) : R)
      ((HSMul.hSMul (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det : (a : ι → M) → R) fun (i_1 : ι) ↦
          (e : (a : ι) → M) (i i_1) :
        R)
⊢ f = HSMul.hSMul (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det

Tactic:
refine Basis.ext_alternating e fun i h => ?_

Premises used: Module.Basis.ext_alternating
-- 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
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i ⋯
change :
  Eq.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) (Function.comp (β := ι) (⇑e : (a : ι) → M) (⇑σ : (a : ι) → ι)) : R)
    ((HSMul.hSMul (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det : (a : ι → M) → R)
        (Function.comp (β := ι) (⇑e : (a : ι) → M) (⇑σ : (a : ι) → ι)) :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) fun (i_1 : ι) ↦ (e : (a : ι) → M) (i i_1) : R)
    ((HSMul.hSMul (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det : (a : ι → M) → R) fun (i_1 : ι) ↦
        (e : (a : ι) → M) (i i_1) :
      R)

Tactic:
change f (e ∘ σ) = (f e • e.det) (e ∘ σ)

Premises used: Function.comp, Module.Basis.det, HSMul.hSMul, 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
f : M [⋀^ι]→ₗ[R] R
i : ι → ι
h : Injective i
σ : Equiv.Perm ι := Equiv.ofBijective i ⋯
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) (Function.comp (β := ι) (⇑e : (a : ι) → M) (⇑σ : (a : ι) → ι)) : R)
    ((HSMul.hSMul (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) e.det : (a : ι → M) → R)
        (Function.comp (β := ι) (⇑e : (a : ι) → M) (⇑σ : (a : ι) → ι)) :
      R)

Tactic:
simp [AlternatingMap.map_perm, Basis.det_self]

Premises used: AlternatingMap.map_perm, Module.Basis.det_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
ι : Type u_5
inst_3 : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : Eq.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) (0 : R)
intro : ∀ (val : Fintype ι), f = 0
⊢ f = 0

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- 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_5
inst_3 : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
h : Eq.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) (0 : R)
val : Fintype ι
this : DecidableEq ι := Classical.decEq ι
⊢ f = 0

Tactic:
simpa [h] using f.eq_smul_basis_det e

Premises used: AlternatingMap.eq_smul_basis_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_5
inst_3 : Finite ι
e : Basis ι R M
f : M [⋀^ι]→ₗ[R] R
⊢ Ne.{u_1 + 1} (α := R) ((f : (a : ι → M) → R) (⇑e : (a : ι) → M) : R) (0 : R) ↔ f ≠ 0

Tactic:
not_congr <| f.map_basis_eq_zero_iff e

Premises used: AlternatingMap.map_basis_eq_zero_iff, not_congr
-- Module: Mathlib.LinearAlgebra.Determinant
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
e : Basis ι A M
f : M →ₗ[A] M
v : ι → M
rw :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)
rw₁ :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    HMul.hMul (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) (e.toMatrix v).det
rw₂ :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    Matrix.det.{u_5, u_4} (n := ι) ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f) * (e.toMatrix v).det
rw₃ :
  (e.toMatrix ((⇑f : (a : M) → M) ∘ v)).det =
    (HMul.hMul (α := Matrix ι ι A) ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f : Matrix ι ι A)
        (e.toMatrix v)).det
rw₄ :
  Matrix.det.{u_5, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A)
        ((e.constr ℕ : (a : ι → M) → M →ₗ[A] M) ((⇑f : (a : M) → M) ∘ v))) =
    (HMul.hMul (α := Matrix ι ι A) ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f : Matrix ι ι A)
        (e.toMatrix v)).det
rw₅ :
  Matrix.det.{u_5, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A)
        ((e.constr ℕ : (a : ι → M) → M →ₗ[A] M) ((⇑f : (a : M) → M) ∘ v))) =
    (HMul.hMul (α := Matrix ι ι A) (β := Matrix ι ι A)
        ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) f : Matrix ι ι A)
        ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) ((e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v) :
          Matrix ι ι A)).det
rw₆ :
  Eq.{u_5 + 1} (α := A)
    (Matrix.det.{u_5, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A)
        ((e.constr ℕ : (a : ι → M) → M →ₗ[A] M) ((⇑f : (a : M) → M) ∘ v))))
    (Matrix.det.{u_5, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) (f ∘ₗ (e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v)))
rw₇ rw₈ :
  Eq.{u_5 + 1} (α := A)
    (Matrix.det.{u_5, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) (f ∘ₗ (e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v)))
    (Matrix.det.{u_5, u_4} (n := ι)
      ((LinearMap.toMatrix e e : (a : M →ₗ[A] M) → Matrix ι ι A) (f ∘ₗ (e.constr ℕ : (a : ι → M) → M →ₗ[A] M) v)))
⊢ (e.det : (a : ι → M) → A) ((⇑f : (a : M) → M) ∘ v) =
    HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) f : A) ((e.det : (a : ι → M) → A) v : A)

Tactic:
rw [det_apply, det_apply, ← f.det_toMatrix e, ← Matrix.det_mul,
    e.toMatrix_eq_toMatrix_constr (f ∘ v), e.toMatrix_eq_toMatrix_constr v, ← toMatrix_comp,
    e.constr_comp]

Premises used: Module.Basis.constr_comp, Function.comp, Matrix.det_mul, LinearMap.toMatrix_comp, Module.Basis.toMatrix_eq_toMatrix_constr, DFunLike.coe, LinearMap.det_toMatrix, Module.Basis.det_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
M' : Type u_3
inst_1 : AddCommGroup M'
ι : Type u_4
inst_2 : DecidableEq ι
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommRing A
inst_5 : Module A M
inst_6 : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
rw :
  Matrix.det (b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M))) =
    Matrix.det.{u_5, u_4} (n := ι) ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f)
⊢ Eq.{u_5 + 1} (α := A)
    ((b'.det : (a : ι → M') → A)
        (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)) :
      A)
    ((LinearMap.det : (a : M' →ₗ[A] M') → A) (f ∘ₗ (↑(b'.equiv b (Equiv.refl ι)) : M' →ₗ[A] M)) : A)

Tactic:
rw [det_apply, ← LinearMap.det_toMatrix b', LinearMap.toMatrix_comp _ b, Matrix.det_mul,
    LinearMap.toMatrix_basis_equiv, Matrix.det_one, mul_one]

Premises used: Matrix.det_mul, LinearMap.toMatrix_comp, Matrix.det_one, mul_one, LinearMap.toMatrix_basis_equiv, LinearMap.det_toMatrix, Module.Basis.det_apply
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
M' : Type u_3
inst_1 : AddCommGroup M'
ι : Type u_4
inst_2 : DecidableEq ι
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommRing A
inst_5 : Module A M
inst_6 : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
e_M :
  Eq (α := Matrix ι ι A)
    (b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)))
    ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f)
⊢ Matrix.det (b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M))) =
    Matrix.det.{u_5, u_4} (n := ι) ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f)

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
M' : Type u_3
inst_1 : AddCommGroup M'
ι : Type u_4
inst_2 : DecidableEq ι
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommRing A
inst_5 : Module A M
inst_6 : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
e_M :
  ∀ (i j : ι),
    b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)) i j =
      (LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f i j
⊢ Eq (α := Matrix ι ι A)
    (b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)))
    ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Determinant
Goal:
M : Type u_2
inst : AddCommGroup M
M' : Type u_3
inst_1 : AddCommGroup M'
ι : Type u_4
inst_2 : DecidableEq ι
inst_3 : Fintype ι
A : Type u_5
inst_4 : CommRing A
inst_5 : Module A M
inst_6 : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
i j : ι
e_M :
  Eq.{u_5 + 1} (α := A)
    (((b'.repr : (a : M') → ι →₀ A)
            (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M) j) :
          (a : ι) → A)
        i :
      A)
    ((LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f i j : A)
e_M₁ :
  Eq.{u_5 + 1} (α := A)
    (((b'.repr : (a : M') → ι →₀ A)
            (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M) j) :
          (a : ι) → A)
        i :
      A)
    ((((b'.repr : (a : M') → ι →₀ A) ((f : (a : M) → M') ((b : (a : ι) → M) j : M)) : ι →₀ A) : (a : ι) → A) i : A)
e_M₂ e_M₃ :
  Eq.{u_5 + 1} (α := A)
    ((((b'.repr : (a : M') → ι →₀ A) ((f : (a : M) → M') ((b : (a : ι) → M) j : M)) : ι →₀ A) : (a : ι) → A) i : A)
    ((((b'.repr : (a : M') → ι →₀ A) ((f : (a : M) → M') ((b : (a : ι) → M) j : M)) : ι →₀ A) : (a : ι) → A) i : A)
⊢ b'.toMatrix (Function.comp.{u_4 + 1, u_2 + 1, u_3 + 1} (β := M) (⇑f : (a : M) → M') (⇑b : (a : ι) → M)) i j =
    (LinearMap.toMatrix b b' : (a : M →ₗ[A] M') → Matrix ι ι A) f i j

Tactic:
rw [toMatrix_apply, LinearMap.toMatrix_apply, Function.comp_apply]

Premises used: Module.Basis.toMatrix_apply, Function.comp_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Determinant
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 b' : Basis ι A M
⊢ Eq.{u_5 + 1} (α := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑(b'.equiv b (Equiv.refl ι)) : M →ₗ[A] M) : A)
    ((b'.det : (a : ι → M) → A) (⇑b : (a : ι) → M) : A)

Tactic:
(b.det_comp_basis b' (LinearMap.id)).symm

Premises used: Module.Basis.det_comp_basis, LinearMap.id, Eq.symm
-- Module: Mathlib.LinearAlgebra.Determinant
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 b' b'' : Basis ι A M
h :
  ∀ (x : ι),
    Eq (α := M) ((b'' : (a : ι) → M) x : M)
      (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M) x : M)
⊢ Eq (α := (a : ι) → M) (⇑b'' : (a : ι) → M)
    (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Determinant
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 b' b'' : Basis ι A M
x : ι
⊢ Eq (α := M) ((b'' : (a : ι) → M) x : M)
    (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M) x : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Determinant
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 b' b'' : Basis ι A M
⊢ Eq (α := (a : ι) → M) (⇑b'' : (a : ι) → M)
    (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M))

Tactic:
have : b'' = (b'.equiv b'' (Equiv.refl ι)).toLinearMap ∘ b' := by
    ext; simp
-- Module: Mathlib.LinearAlgebra.Determinant
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 b' b'' : Basis ι A M
this :
  Eq (α := (a : ι) → M) (⇑b'' : (a : ι) → M)
    (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M))
rw :
  HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
    ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A)
| (b.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M)

Tactic:
rw [this, Basis.det_comp, det_basis, mul_comm]

Premises used: Module.Basis.det_comp, Module.Basis.det_basis, mul_comm
-- Module: Mathlib.LinearAlgebra.Determinant
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 b' b'' : Basis ι A M
this :
  Eq (α := (a : ι) → M) (⇑b'' : (a : ι) → M)
    (Function.comp (β := M) (⇑(↑(b'.equiv b'' (Equiv.refl ι)) : M →ₗ[A] M) : (a : M) → M) (⇑b' : (a : ι) → M))
conv_rhs :
  HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
      ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A) =
    (b.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M)
conv_rhs₁ :
  HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
      ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A) =
    HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
      ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A)
⊢ HMul.hMul (α := A) (β := A) ((b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M) : A)
      ((b'.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M) : A) =
    (b.det : (a : ι → M) → A) (⇑b'' : (a : ι) → M)

Tactic:
conv_rhs =>
    rw [this, Basis.det_comp, det_basis, mul_comm]

Premises used: Module.Basis.det_comp, Module.Basis.det_basis, mul_comm
-- Module: Mathlib.LinearAlgebra.Determinant
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 b' : Basis ι A M
rw :
  HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑(b.equiv b' (Equiv.refl ι)) : M →ₗ[A] M) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑(b'.equiv b (Equiv.refl ι)) : M →ₗ[A] M) : A) =
    1
⊢ (↑(IsUnit.unit (a := (b.det : (a : ι → M) → A) (⇑b' : (a : ι) → M)) ⋯)⁻¹ : A) =
    (b'.det : (a : ι → M) → A) (⇑b : (a : ι) → M)

Tactic:
rw [← Units.mul_eq_one_iff_inv_eq, IsUnit.unit_spec, ← det_basis, ← det_basis]

Premises used: Module.Basis.det_basis, IsUnit.unit_spec, Units.mul_eq_one_iff_inv_eq
-- Module: Mathlib.LinearAlgebra.Determinant
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 b' : Basis ι A M
⊢ HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑(b.equiv b' (Equiv.refl ι)) : M →ₗ[A] M) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑(b'.equiv b (Equiv.refl ι)) : M →ₗ[A] M) : A) =
    1

Tactic:
LinearEquiv.det_mul_det_symm _

Premises used: Finsupp.equivMapDomain, LinearEquiv.det_mul_det_symm, Equiv.symm, Equiv.refl
-- Module: Mathlib.LinearAlgebra.Determinant
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 b' : Basis ι A M
⊢ HMul.hMul (α := A) (β := A) ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑(b.equiv b' (Equiv.refl ι)) : M →ₗ[A] M) : A)
      ((LinearMap.det : (a : M →ₗ[A] M) → A) (↑(b'.equiv b (Equiv.refl ι)) : M →ₗ[A] M) : A) =
    1

Tactic:
exact LinearEquiv.det_mul_det_symm _

Premises used: LinearEquiv.det_mul_det_symm