awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
inst : DecidableEq m
inst_1 : Fintype m
R : Type v
inst_2 : CommRing R
M N : Matrix m m R
rw : M.det * N.det = (N * M).det
rw₁ : M.det * N.det = N.det * M.det
rw₂ rw₃ : N.det * M.det = N.det * M.det
⊢ (M * N).det = (N * M).det

Tactic:
rw [det_mul, det_mul, mul_comm]

Premises used: Matrix.det_mul, mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
inst : DecidableEq m
inst_1 : Fintype m
R : Type v
inst_2 : CommRing R
M N P : Matrix m m R
rw : (M * N * P).det = (N * (M * P)).det
rw₁ : (M * N * P).det = (N * M * P).det
rw₂ : (M * N).det * P.det = (N * M * P).det
rw₃ : (N * M).det * P.det = (N * M * P).det
rw₄ rw₅ : (N * M * P).det = (N * M * P).det
⊢ (M * (N * P)).det = (N * (M * P)).det

Tactic:
rw [← Matrix.mul_assoc, ← Matrix.mul_assoc, det_mul, det_mul_comm M N, ← det_mul]

Premises used: Matrix.mul_assoc, Matrix.det_mul, Matrix.det_mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
inst : DecidableEq m
inst_1 : Fintype m
R : Type v
inst_2 : CommRing R
M N P : Matrix m m R
rw : (M * (N * P)).det = (M * P * N).det
rw₁ : (M * (N * P)).det = (M * (P * N)).det
rw₂ : M.det * (N * P).det = (M * (P * N)).det
rw₃ : M.det * (P * N).det = (M * (P * N)).det
rw₄ rw₅ : (M * (P * N)).det = (M * (P * N)).det
⊢ (M * N * P).det = (M * P * N).det

Tactic:
rw [Matrix.mul_assoc, Matrix.mul_assoc, det_mul, det_mul_comm N P, ← det_mul]

Premises used: Matrix.mul_assoc, Matrix.det_mul, Matrix.det_mul_comm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
inst : DecidableEq m
inst_1 : Fintype m
R : Type v
inst_2 : CommRing R
M : (Matrix m m R)ˣ
N : Matrix m m R
rw : ((↑M : Matrix m m R) * (↑M⁻¹ : Matrix m m R) * N).det = N.det
rw₁ : (1 * N).det = N.det
rw₂ rw₃ : N.det = N.det
⊢ ((↑M : Matrix m m R) * N * (↑M⁻¹ : Matrix m m R)).det = N.det

Tactic:
rw [det_mul_right_comm, Units.mul_inv, one_mul]

Premises used: Units.mul_inv, Matrix.det_mul_right_comm, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
inst : DecidableEq m
inst_1 : Fintype m
R : Type v
inst_2 : CommRing R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ ((↑M⁻¹ : Matrix m m R) * N * (↑M : Matrix m m R)).det = N.det

Tactic:
det_units_conj M⁻¹ N

Premises used: Inv.inv, Matrix.det_units_conj
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
rw :
  Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i))
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, M ((σ : (a : n) → n) i) i))
⊢ Mᵀ.det = M.det

Tactic:
rw [det_apply', det_apply']

Premises used: Matrix.det_apply'
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i))
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, M ((σ : (a : n) → n) i) i))

Tactic:
Fintype.sum_bijective _ inv_involutive.bijective _ _ ?_

Premises used: Fintype.sum_bijective, inv_involutive, Function.Involutive.bijective
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
refine :
  ∀ (x : Perm n),
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x) : ℤ) : R)
        (∏ i : n, Mᵀ ((x : (a : n) → n) i) i) =
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x⁻¹) : ℤ) : R)
        (∏ i : n, M ((x⁻¹ : (a : n) → n) i) i)
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i))
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, M ((σ : (a : n) → n) i) i))

Tactic:
refine Fintype.sum_bijective _ inv_involutive.bijective _ _ ?_

Premises used: Fintype.sum_bijective, inv_involutive, Function.Involutive.bijective
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
σ : Perm n
rw :
  HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i) =
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, M ((σ⁻¹ : (a : n) → n) i) i)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i) =
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ⁻¹) : ℤ) : R)
      (∏ i : n, M ((σ⁻¹ : (a : n) → n) i) i)

Tactic:
rw [sign_inv]

Premises used: Equiv.Perm.sign_inv
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
σ : Perm n
e_a : Eq.{v + 1} (α := R) (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i) (∏ i : n, M ((σ⁻¹ : (a : n) → n) i) i)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i) =
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n, M ((σ⁻¹ : (a : n) → n) i) i)

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
σ : Perm n
e_a : ∀ (x : n), Mᵀ ((σ : (a : n) → n) x) x = M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) x : n)) ((σ : (a : n) → n) x)
⊢ Eq.{v + 1} (α := R) (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i) (∏ i : n, M ((σ⁻¹ : (a : n) → n) i) i)

Tactic:
apply Fintype.prod_equiv σ

Premises used: Fintype.prod_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
σ : Perm n
⊢ ∀ (x : n), Mᵀ ((σ : (a : n) → n) x) x = M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) x : n)) ((σ : (a : n) → n) x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
σ : Perm n
M : Matrix n n R
⊢ HSMul.hSMul (α := ℤˣ) (β := R) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)
      ((detRowAlternating : (a : n → n → R) → R) M : R) =
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det

Tactic:
simp [Units.smul_def, det]

Premises used: Units.smul_def, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
σ : Perm n
M : Matrix n n R
rw : det (M.submatrix id (⇑σ : (a : n) → n))ᵀ = (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
rw₁ : det (Mᵀ.submatrix (⇑σ : (a : n) → n) id) = (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
rw₂ :
  (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * Mᵀ.det =
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
rw₃ rw₄ :
  (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det =
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
⊢ det (M.submatrix id (⇑σ : (a : n) → n)) = (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det

Tactic:
rw [← det_transpose, transpose_submatrix, det_permute, det_transpose]

Premises used: Matrix.det_permute, Matrix.det_transpose, Matrix.transpose_submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : n ≃ m
A : Matrix m m R
rw :
  Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n,
          A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i))
    (∑ σ : Perm m,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ) : ℤ) : R)
        (∏ i : m, A ((σ : (a : m) → m) i) i))
⊢ det.{v, u_2} (n := n) (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) = A.det

Tactic:
rw [det_apply', det_apply']

Premises used: Matrix.det_apply'
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : n ≃ m
A : Matrix m m R
h :
  ∀ (x : Perm n),
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x) : ℤ) : R)
        (∏ i : n,
          A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((x : (a : n) → n) i : n) i) =
      HMul.hMul (α := R)
        (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) ((e.permCongr : (a : Perm n) → Perm m) x)) : ℤ) : R)
        (∏ i : m, A ((((e.permCongr : (a : Perm n) → Perm m) x : Perm m) : (a : m) → m) i) i)
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n,
          A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i))
    (∑ σ : Perm m,
      HMul.hMul (α := R) (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) σ) : ℤ) : R)
        (∏ i : m, A ((σ : (a : m) → m) i) i))

Tactic:
apply Fintype.sum_equiv (Equiv.permCongr e)

Premises used: Equiv.permCongr, Fintype.sum_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
h :
  HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n,
        A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i) =
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m, A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) i) i)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n,
        A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i) =
    HMul.hMul (α := R)
      (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) ((e.permCongr : (a : Perm n) → Perm m) σ)) : ℤ) : R)
      (∏ i : m, A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) i) i)

Tactic:
rw [Equiv.Perm.sign_permCongr e σ]

Premises used: Equiv.Perm.sign_permCongr
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
h :
  Eq.{v + 1} (α := R)
    (∏ i : n, A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i)
    (∏ i : m, A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) i) i)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : n,
        A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i) =
    HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (∏ i : m, A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) i) i)

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
h :
  ∀ (x : n),
    A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) x : n) x =
      A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) ((e : (a : n) → m) x : m))
        ((e : (a : n) → m) x)
⊢ Eq.{v + 1} (α := R)
    (∏ i : n, A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i)
    (∏ i : m, A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) i) i)

Tactic:
apply Fintype.prod_equiv e

Premises used: Fintype.prod_equiv
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : n ≃ m
A : Matrix m m R
σ : Perm n
i : n
h :
  A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
    A ((e : (a : n) → m) ((σ : (a : n) → n) ((e.symm : (a : m) → n) ((e : (a : n) → m) i : m) : n) : n))
      ((e : (a : n) → m) i)
h₁ :
  A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
    A ((e : (a : n) → m) ((σ : (a : n) → n) i : n)) ((e : (a : n) → m) i)
h₂ h₃ :
  A ((e : (a : n) → m) ((σ : (a : n) → n) i : n)) ((e : (a : n) → m) i) =
    A ((e : (a : n) → m) ((σ : (a : n) → n) i : n)) ((e : (a : n) → m) i)
⊢ A.submatrix (l := n) ((⇑e : (a : n) → m) : (a : n) → m) (⇑e : (a : n) → m) ((σ : (a : n) → n) i : n) i =
    A ((((e.permCongr : (a : Perm n) → Perm m) σ : Perm m) : (a : m) → m) ((e : (a : n) → m) i : m))
      ((e : (a : n) → m) i)

Tactic:
rw [Equiv.permCongr_apply, Equiv.symm_apply_apply, submatrix_apply]

Premises used: Equiv.symm_apply_apply, Equiv.permCongr_apply, Matrix.submatrix_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
H : ∀ (x : n), Eq.{u_1 + 1} (α := m) ((e₂ : (a : n) → m) x : m) ((e₁.trans (e₁.symm.trans e₂) : (a : n) → m) x : m)
⊢ e₂ = e₁.trans (e₁.symm.trans e₂)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
x : n
⊢ Eq.{u_1 + 1} (α := m) ((e₂ : (a : n) → m) x : m) ((e₁.trans (e₁.symm.trans e₂) : (a : n) → m) x : m)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
⊢ e₂ = e₁.trans (e₁.symm.trans e₂)

Tactic:
have hee : e₂ = e₁.trans (e₁.symm.trans e₂) := by ext; simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
rw :
  |det.{u_3, u_2} (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑(e₁.trans (e₁.symm.trans e₂)) : (a : n) → m))| = |A.det|
⊢ |det.{u_3, u_2} (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑e₂ : (a : n) → m))| = |A.det|

Tactic:
rw [hee]
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
change :
  |det.{u_3, u_2} (n := n)
        (submatrix (n := m) (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m)) (⇑e₁ : (a : n) → m)
          (⇑e₁ : (a : n) → m))| =
    |A.det|
⊢ |det.{u_3, u_2} (n := n) (A.submatrix (⇑e₁ : (a : n) → m) (⇑(e₁.trans (e₁.symm.trans e₂)) : (a : n) → m))| = |A.det|

Tactic:
change |((A.submatrix id (e₁.symm.trans e₂)).submatrix e₁ e₁).det| = |A.det|

Premises used: Matrix.submatrix, Equiv.trans, id, Equiv.symm, DFunLike.coe, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
rw : |det (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m))| = |A.det|
rw₁ : |(↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e₁.symm.trans e₂)) : ℤ) : R) * A.det| = |A.det|
rw₂ : |(↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e₁.symm.trans e₂)) : ℤ) : R)| * |A.det| = |A.det|
rw₃ : 1 * |A.det| = |A.det|
rw₄ rw₅ : |A.det| = |A.det|
⊢ |det.{u_3, u_2} (n := n)
        (submatrix (n := m) (A.submatrix id (⇑(e₁.symm.trans e₂) : (a : m) → m)) (⇑e₁ : (a : n) → m)
          (⇑e₁ : (a : n) → m))| =
    |A.det|

Tactic:
rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]

Premises used: abs_mul, abs_unit_intCast, Matrix.det_permute', Matrix.det_submatrix_equiv_self, one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e : m ≃ n
A : Matrix m m R
⊢ det.{v, u_2} (n := n) ((reindex e e : (a : Matrix m m R) → Matrix n n R) A) = A.det

Tactic:
det_submatrix_equiv_self e.symm A

Premises used: Matrix.submatrix, Matrix.det_submatrix_equiv_self, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
trans :
  Eq.{v + 1} (α := R) (det.{v, u_2} (n := n) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M))
    (det.{v, u_2} (n := n)
      ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M)))
trans₁ :
  det.{v, u_2} (n := n)
      ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M)) =
    (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e'.trans e.symm)) : ℤ) : R) * M.det
⊢ det.{v, u_2} (n := n) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M) =
    (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e'.trans e.symm)) : ℤ) : R) * M.det

Tactic:
trans ((M.reindex (e.trans e'.symm) (.refl _)).reindex e' e').det

Premises used: Equiv.trans, Matrix.reindex, Equiv.symm, Equiv.refl, DFunLike.coe, Matrix.det
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
e_M :
  Eq (α := Matrix n n R) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M : Matrix n n R)
    ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M) :
      Matrix n n R)
⊢ Eq.{v + 1} (α := R) (det.{v, u_2} (n := n) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M))
    (det.{v, u_2} (n := n)
      ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M)))

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
e_M :
  ∀ (i j : n),
    Eq.{v + 1} (α := R) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M i j : R)
      ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
          ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M) i j :
        R)
⊢ Eq (α := Matrix n n R) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M : Matrix n n R)
    ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M) :
      Matrix n n R)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
i j : n
⊢ Eq.{v + 1} (α := R) ((reindex e e' : (a : Matrix m m R) → Matrix n n R) M i j : R)
    ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M) i j :
      R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
simp_rw :
  (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e.trans e'.symm).symm) : ℤ) : R) * M.det =
    (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e'.trans e.symm)) : ℤ) : R) * M.det
⊢ det.{v, u_2} (n := n)
      ((reindex e' e' : (a : Matrix m m R) → Matrix n n R)
        ((reindex (e.trans e'.symm) (Equiv.refl m) : (a : Matrix m m R) → Matrix m m R) M)) =
    (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e'.trans e.symm)) : ℤ) : R) * M.det

Tactic:
simp_rw [det_reindex_self, reindex_apply, Equiv.refl_symm, Equiv.coe_refl, det_permute]

Premises used: Matrix.det_permute, Matrix.reindex_apply, Equiv.refl_symm, Equiv.coe_refl, Matrix.det_reindex_self
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type v
inst_4 : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e.trans e'.symm).symm) : ℤ) : R) * M.det =
    (↑(↑(((sign : Perm m →* ℤˣ) : (a : Perm m) → ℤˣ) (e'.trans e.symm)) : ℤ) : R) * M.det

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
m : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : DecidableEq m
inst_3 : Fintype m
R : Type u_3
inst_4 : CommRing R
inst_5 : LinearOrder R
inst_6 : IsStrictOrderedRing R
e₁ e₂ : m ≃ n
A : Matrix m m R
⊢ |det.{u_3, u_2} (n := n) ((reindex e₁ e₂ : (a : Matrix m m R) → Matrix n n R) A)| = |A.det|

Tactic:
abs_det_submatrix_equiv_equiv e₁.symm e₂.symm A

Premises used: Matrix.abs_det_submatrix_equiv_equiv, Matrix.submatrix, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
c : R
rw rw₁ : ((diagonal fun (x : n) ↦ c) * A).det = ((diagonal fun (x : n) ↦ c) * A).det
⊢ (c • A).det = ((diagonal fun (x : n) ↦ c) * A).det

Tactic:
rw [smul_eq_diagonal_mul]

Premises used: Matrix.smul_eq_diagonal_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
c : R
⊢ det.{v, u_2} (n := n) (diagonal fun (x : n) ↦ c) * A.det = c ^ Fintype.card n * A.det

Tactic:
simp