awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
⊢ Eq.{v + 1} (α := R)
    (∑ x : Perm n,
      ∑ i : (a : n) → n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x) : ℤ) : R)
          (∏ i_1 : n, M ((x : (a : n) → n) i_1) (i i_1) * N (i i_1) i_1))
    (∑ p : n → n,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))
have rw : Eq.{v + 1} (α := R)
  (∑ y : (a : n) → n,
    ∑ x : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) x) : ℤ) : R)
        (∏ i : n, M ((x : (a : n) → n) i) (y i) * N (y i) i))
  (∑ p : n → n,
    ∑ σ : Perm n,
      HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
⊢ Eq.{v + 1} (α := R)
    (∑ p : n → n,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))
    (∑ p : n → n with Bijective p,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M ((σ : (a : n) → n) i) (p i) * N (p i) i))
have refine : ∀ (f : n → n), Membership.mem (γ := Finset (n → n)) univ f → ∀ (hbij : f ∉ {p : n → n | Bijective p}), ¬Bijective f
Tactic: refine (sum_subset (filter_subset _ _) fun f _ hbij ↦ det_mul_aux ?_).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
⊢ Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
have rw : Eq.{v + 1} (α := R)
  (∏ i : n, M ((τ : (a : n) → n) ((σ⁻¹ : (a : n) → n) i : n)) ((σ : (a : n) → n) ((σ⁻¹ : (a : n) → n) i : n)))
  (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
Tactic: rw [← (σ⁻¹ : _ ≃ _).prod_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
⊢ HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
      ∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j) =
    (∏ i : n, N ((σ : (a : n) → n) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.mulRight σ⁻¹ : (a : Perm n) → Perm n) τ)) : ℤ) : R) *
      ∏ i : n, M ((((Equiv.mulRight σ⁻¹ : (a : Perm n) → Perm n) τ : Perm n) : (a : n) → n) i) i
have this : Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j)) (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
Tactic: have : (∏ j, M (τ j) (σ j)) = ∏ j, M ((τ * σ⁻¹) j) j := by
            rw [← (σ⁻¹ : _ ≃ _).prod_comp]
            simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
this :
  Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
⊢ HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹)) : ℤ) : R) =
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹ * σ)) : ℤ) : R)
have rw : HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹)) : ℤ) : R)
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) =
  (↑(↑(HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹) : ℤˣ)
            (((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ : ℤˣ)) :
        ℤ) :
    R)
Tactic: rw [mul_comm, sign_mul (τ * σ⁻¹)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (hypothesis)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
σ : Perm n
h : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
this :
  Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
⊢ HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
      ∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j) =
    (∏ i : n, N ((σ : (a : n) → n) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.mulRight σ⁻¹ : (a : Perm n) → Perm n) τ)) : ℤ) : R) *
      ∏ i : n, M ((((Equiv.mulRight σ⁻¹ : (a : Perm n) → Perm n) τ : Perm n) : (a : n) → n) i) i
have h : HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹)) : ℤ) : R) =
  (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R)
Tactic: have h : ε σ * ε (τ * σ⁻¹) = ε τ :=
            calc
              ε σ * ε (τ * σ⁻¹) = ε (τ * σ⁻¹ * σ) := by
                rw [mul_comm, sign_mul (τ * σ⁻¹)]
                simp only [Int.cast_mul, Units.val_mul]
              _ = ε τ := by simp only [inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M N : Matrix n n R
σ : Perm n
h_1 : Membership.mem (γ := Finset (Perm n)) univ σ
τ : Perm n
this :
  Eq.{v + 1} (α := R) (∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j))
    (∏ j : n, M ((τ * σ⁻¹ : (a : n) → n) j) j)
h :
  HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (τ * σ⁻¹)) : ℤ) : R) =
    (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R)
⊢ HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i)
        (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
      ∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j) =
    (∏ i : n, N ((σ : (a : n) → n) i) i) *
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) ((Equiv.mulRight σ⁻¹ : (a : Perm n) → Perm n) τ)) : ℤ) : R) *
      ∏ i : n, M ((((Equiv.mulRight σ⁻¹ : (a : Perm n) → Perm n) τ : Perm n) : (a : n) → n) i) i
have simp_rw : HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
    ∏ j : n, M ((τ : (a : n) → n) j) ((σ : (a : n) → n) j) =
  HMul.hMul (α := R) (∏ i : n, N ((σ : (a : n) → n) i) i)
      (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) τ) : ℤ) : R) *
    ∏ x : n, M ((τ * σ⁻¹ : (a : n) → n) x) x
Tactic: simp_rw [Equiv.coe_mulRight, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * N).det = (N * M).det
have rw : M.det * N.det = (N * M).det
Tactic: rw [det_mul, det_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * N).det = (N * M).det
have rw₁ : M.det * N.det = N.det * M.det
Tactic: rw [det_mul, det_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * N).det = (N * M).det
have rw₂ : N.det * M.det = N.det * M.det
Tactic: rw [det_mul, det_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * (N * P)).det = (N * (M * P)).det
have rw : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * (N * P)).det = (N * (M * P)).det
have rw₁ : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * (N * P)).det = (N * (M * P)).det
have rw₂ : (M * N).det * P.det = (N * M * P).det
Tactic: rw [← Matrix.mul_assoc, ← Matrix.mul_assoc, det_mul, det_mul_comm M N, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * (N * P)).det = (N * (M * P)).det
have rw₃ : (N * M).det * P.det = (N * M * P).det
Tactic: rw [← Matrix.mul_assoc, ← Matrix.mul_assoc, det_mul, det_mul_comm M N, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * (N * P)).det = (N * (M * P)).det
have rw₄ : (N * M * P).det = (N * M * P).det
Tactic: rw [← Matrix.mul_assoc, ← Matrix.mul_assoc, det_mul, det_mul_comm M N, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * N * P).det = (M * P * N).det
have rw : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * N * P).det = (M * P * N).det
have rw₁ : (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * N * P).det = (M * P * N).det
have rw₂ : M.det * (N * P).det = (M * (P * N)).det
Tactic: rw [Matrix.mul_assoc, Matrix.mul_assoc, det_mul, det_mul_comm N P, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * N * P).det = (M * P * N).det
have rw₃ : M.det * (P * N).det = (M * (P * N)).det
Tactic: rw [Matrix.mul_assoc, Matrix.mul_assoc, det_mul, det_mul_comm N P, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ (M * N * P).det = (M * P * N).det
have rw₄ : (M * (P * N)).det = (M * (P * N)).det
Tactic: rw [Matrix.mul_assoc, Matrix.mul_assoc, det_mul, det_mul_comm N P, ← det_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
have rw : ((↑M : Matrix m m R) * (↑M⁻¹ : Matrix m m R) * N).det = N.det
Tactic: rw [det_mul_right_comm, Units.mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ ((↑M : Matrix m m R) * N * (↑M⁻¹ : Matrix m m R)).det = N.det
have rw₁ : (1 * N).det = N.det
Tactic: rw [det_mul_right_comm, Units.mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ ((↑M : Matrix m m R) * N * (↑M⁻¹ : Matrix m m R)).det = N.det
have rw₂ : N.det = N.det
Tactic: rw [det_mul_right_comm, Units.mul_inv, one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
Goal:
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
M : Matrix n n R
⊢ Mᵀ.det = M.det
have 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))
Tactic: rw [det_apply', det_apply']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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))
have 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)
Tactic: refine Fintype.sum_bijective _ inv_involutive.bijective _ _ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [sign_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ 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)
have e_a : Eq.{v + 1} (α := R) (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i) (∏ i : n, M ((σ⁻¹ : (a : n) → n) i) i)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ Eq.{v + 1} (α := R) (∏ i : n, Mᵀ ((σ : (a : n) → n) i) i) (∏ i : n, M ((σ⁻¹ : (a : n) → n) i) i)
have e_a : ∀ (x : n), Mᵀ ((σ : (a : n) → n) x) x = M ((σ⁻¹ : (a : n) → n) ((σ : (a : n) → n) x : n)) ((σ : (a : n) → n) x)
Tactic: apply Fintype.prod_equiv σ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ det (M.submatrix id (⇑σ : (a : n) → n)) = (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
have rw : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ det (M.submatrix id (⇑σ : (a : n) → n)) = (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
have rw₁ : det (Mᵀ.submatrix (⇑σ : (a : n) → n) id) = (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
Tactic: rw [← det_transpose, transpose_submatrix, det_permute, det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ det (M.submatrix id (⇑σ : (a : n) → n)) = (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
have rw₂ : (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * Mᵀ.det =
  (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
Tactic: rw [← det_transpose, transpose_submatrix, det_permute, det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ det (M.submatrix id (⇑σ : (a : n) → n)) = (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
have rw₃ : (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det =
  (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R) * M.det
Tactic: rw [← det_transpose, transpose_submatrix, det_permute, det_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ det.{v, u_2} (n := n) (A.submatrix (⇑e : (a : n) → m) (⇑e : (a : n) → m)) = A.det
have 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))
Tactic: rw [det_apply', det_apply']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ 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))
have 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)
Tactic: apply Fintype.sum_equiv (Equiv.permCongr e)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [Equiv.Perm.sign_permCongr e σ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ 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)
have 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)
Tactic: congr 1