awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
pos : ∀ (hik : i = k), M' i.succ j = N i.succ j + 0 * M' i.castSucc j
neg : ∀ (hik : ¬i = k), M' i.succ j = N i.succ j + c i * M' i.castSucc j
⊢ M' i.succ j = N i.succ j + (if i = k then 0 else c i) * M' i.castSucc j

Tactic:
split_ifs with hik
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : i = k
pos : M' i.succ j = N i.succ j + 0
pos₁ : M' i.succ j = N i.succ j
pos₂ : M.updateRow k.succ (N k.succ) i.succ j = N i.succ j
pos₃ : M.updateRow k.succ (N k.succ) k.succ j = N k.succ j
pos₄ pos₅ : N k.succ j = N k.succ j
⊢ M' i.succ j = N i.succ j + 0 * M' i.castSucc j

Tactic:
rw [zero_mul, add_zero, hM', hik, updateRow_self]

Premises used: MulZeroClass.zero_mul, Matrix.updateRow_self, add_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
neg : N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j
⊢ M' i.succ j = N i.succ j + c i * M' i.castSucc j

Tactic:
rw [hM', updateRow_ne ((Fin.succ_injective _).ne hik), hsucc]

Premises used: Function.Injective.ne, Fin.succ_injective, Matrix.updateRow_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
pos :
  ∀ (hik2 : k < i), N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j
neg :
  ∀ (hik2 : ¬k < i), N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j
⊢ N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j

Tactic:
by_cases hik2 : k < i
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : k < i
⊢ N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j

Tactic:
simp [hc i (Fin.succ_lt_succ_iff.mpr hik2)]

Premises used: Iff.mpr, Fin.succ_lt_succ_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
neg : i.castSucc ≠ k.succ
⊢ N i.succ j + c i * M i.castSucc j = N i.succ j + c i * M.updateRow k.succ (N k.succ) i.castSucc j

Tactic:
rw [updateRow_ne]

Premises used: Matrix.updateRow_ne
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
neg : i.castSucc < k.succ
⊢ i.castSucc ≠ k.succ

Tactic:
apply ne_of_lt

Premises used: ne_of_lt
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
k_1 : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R) (_hc : ∀ (i : Fin n), k.castSucc < i.succ → c i = 0) {M N : Matrix (Fin n.succ) (Fin n.succ) R}
    (_h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j)
    (_hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j), M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
neg : (↑i.castSucc : ℕ) < (↑k.succ : ℕ)
neg₁ : (↑i : ℕ) < (↑k.succ : ℕ)
neg₂ : (↑i : ℕ) < (↑k : ℕ) + 1
neg₃ : (↑i : ℕ) ≤ (↑k : ℕ)
neg₄ neg₅ neg₆ neg₇ : ¬(↑k : ℕ) < (↑i : ℕ)
⊢ i.castSucc < k.succ

Tactic:
rwa [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]

Premises used: Fin.val_succ, Fin.lt_def, not_lt, Nat.lt_succ_iff, Fin.val_castSucc
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (j : Fin (n + 1)), A 0 j = B 0 j
A_succ : ∀ (i : Fin n) (j : Fin (n + 1)), A i.succ j = B i.succ j + c i * A i.castSucc j
⊢ A.det = B.det

Tactic:
det_eq_of_forall_row_eq_smul_add_pred_aux (Fin.last _) c
    (fun _ hi => absurd hi (not_lt_of_ge (Fin.le_last _))) A_zero A_succ

Premises used: Matrix.det_eq_of_forall_row_eq_smul_add_pred_aux, Fin.succ, absurd, Fin.last, not_lt_of_ge, Fin.le_last
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
rw : Aᵀ.det = Bᵀ.det
⊢ A.det = B.det

Tactic:
rw [← det_transpose A, ← det_transpose B]

Premises used: Matrix.det_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ Aᵀ.det = Bᵀ.det

Tactic:
det_eq_of_forall_row_eq_smul_add_pred c A_zero fun i j => A_succ j i

Premises used: Matrix.det_eq_of_forall_row_eq_smul_add_pred
-- Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Goal:
R : Type v
inst : CommRing R
n : ℕ
A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R
c : Fin n → R
A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0
A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc
⊢ Aᵀ.det = Bᵀ.det

Tactic:
exact det_eq_of_forall_row_eq_smul_add_pred c A_zero fun i j => A_succ j i

Premises used: Matrix.det_eq_of_forall_row_eq_smul_add_pred
-- 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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
simp_rw :
  Eq.{v + 1} (α := R)
    (∑ σ : Perm (n × o),
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i))
    (∏ x : o,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M x ((σ : (a : n) → n) i) i))
⊢ (blockDiagonal M).det = ∏ k : o, (M k).det

Tactic:
simp_rw [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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
rw :
  Eq.{v + 1} (α := R)
    (∑ σ : Perm (n × o),
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i))
    (∑ p ∈ pi (β := fun (i : o) ↦ Perm n) univ fun (x : o) ↦ univ,
      ∏ x ∈ attach univ,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (p (↑x : o) ⋯)) : ℤ) : R)
          (∏ i : n, M (↑x : o) ((p (↑x : o) ⋯ : (a : n) → n) i) i))
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm (n × o),
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i))
    (∏ x : o,
      ∑ σ : Perm n,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) σ) : ℤ) : R)
          (∏ i : n, M x ((σ : (a : n) → n) i) i))

Tactic:
rw [Finset.prod_sum]

Premises used: Finset.prod_sum
-- 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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
simp_rw :
  Eq.{v + 1} (α := R)
    (∑ σ : Perm (n × o),
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i))
    (∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (x x_1 ⋯)) : ℤ) : R)
          (∏ x_2 : n, M x_1 ((x x_1 ⋯ : (a : n) → n) x_2) x_2))
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm (n × o),
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i))
    (∑ p ∈ pi (β := fun (i : o) ↦ Perm n) univ fun (x : o) ↦ univ,
      ∏ x ∈ attach univ,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (p (↑x : o) ⋯)) : ℤ) : R)
          (∏ i : n, M (↑x : o) ((p (↑x : o) ⋯ : (a : n) → n) i) i))

Tactic:
simp_rw [Finset.prod_attach_univ, Finset.univ_pi_univ]

Premises used: Finset.univ_pi_univ, Finset.prod_attach_univ
-- 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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
⊢ ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2

Tactic:
have mem_preserving_snd :
    ∀ {σ : Equiv.Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ x, (σ x).snd = x.snd := fun {σ} =>
    Finset.mem_filter.trans ⟨fun h => h.2, fun h => ⟨Finset.mem_univ _, h⟩⟩
-- 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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
rw :
  Eq.{v + 1} (α := R)
    (∑ x ∈ preserving_snd,
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) x) : ℤ) : R)
        (∏ i : n × o, blockDiagonal M ((x : (a : n × o) → n × o) i) i))
    (∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (x x_1 ⋯)) : ℤ) : R)
          (∏ x_2 : n, M x_1 ((x x_1 ⋯ : (a : n) → n) x_2) x_2))
rw₁ :
  ∀ (x : Perm (n × o)),
    Membership.mem (γ := Finset (Perm (n × o))) univ x →
      x ∉ preserving_snd →
        HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) x) : ℤ) : R)
            (∏ i : n × o, blockDiagonal M ((x : (a : n × o) → n × o) i) i) =
          0
⊢ Eq.{v + 1} (α := R)
    (∑ σ : Perm (n × o),
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) σ) : ℤ) : R)
        (∏ i : n × o, blockDiagonal M ((σ : (a : n × o) → n × o) i) i))
    (∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (x x_1 ⋯)) : ℤ) : R)
          (∏ x_2 : n, M x_1 ((x x_1 ⋯ : (a : n) → n) x_2) x_2))

Tactic:
rw [← Finset.sum_subset (Finset.subset_univ preserving_snd) _]

Premises used: Finset.sum_subset, Finset.subset_univ
-- 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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
⊢ Eq.{v + 1} (α := R)
    (∑ x ∈ preserving_snd,
      HMul.hMul (α := R) (↑(↑(((sign : Perm (n × o) →* ℤˣ) : (a : Perm (n × o)) → ℤˣ) x) : ℤ) : R)
        (∏ i : n × o, blockDiagonal M ((x : (a : n × o) → n × o) i) i))
    (∑ x : (a : o) → a ∈ univ → Perm n,
      ∏ x_1 : o,
        HMul.hMul (α := R) (↑(↑(((sign : Perm n →* ℤˣ) : (a : Perm n) → ℤˣ) (x x_1 ⋯)) : ℤ) : R)
          (∏ x_2 : n, M x_1 ((x x_1 ⋯ : (a : n) → n) x_2) x_2))

Tactic:
(Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).symm

Premises used: Finset.sum_bij, Equiv.prodCongrLeft, Eq.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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n
refine_1 :
  ∀ (ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ),
    (fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
            (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
          (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
        σ ha ∈
      preserving_snd
⊢ ∀ (ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ),
    (fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
            (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
          (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
        σ ha ∈
      preserving_snd

Tactic:
_
-- 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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n
ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ
refine_1 :
  ∀ (x : n × o),
    (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                  (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
                (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
              σ ha :
            (a : n × o) → n × o)
          x).2 =
      x.2
⊢ (fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
          (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
        (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
      σ ha ∈
    preserving_snd

Tactic:
rw [mem_preserving_snd]
-- 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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n
ha : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ
fst : n
x : o
⊢ (((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
                (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
              (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
            σ ha :
          (a : n × o) → n × o)
        (fst, x)).2 =
    (fst, x).2

Tactic:
simp only [prodCongrLeft_apply]

Premises used: Equiv.prodCongrLeft_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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := {σ : Perm (n × o) | ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2}
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), ((σ : (a : n × o) → n × o) x).2 = x.2
σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n
refine_2 :
  ∀ (ha₁ : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ)
    (a₂ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
    (ha₂ : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ a₂),
    Eq (α := n × o ≃ n × o)
        ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
              (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
            (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
          σ ha₁)
        ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
              (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
            (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
          a₂ ha₂) →
      σ = a₂
⊢ ∀ (ha₁ : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ)
    (a₂ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
    (ha₂ : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ a₂),
    Eq (α := n × o ≃ n × o)
        ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
              (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
            (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
          σ ha₁)
        ((fun (σ : (a : o) → Membership.mem (γ := Finset o) univ a → Perm n)
              (x : Membership.mem (γ := Finset ((a : o) → Membership.mem (γ := Finset o) univ a → Perm n)) univ σ) ↦
            (prodCongrLeft fun (k : o) ↦ σ k ⋯ : n × o ≃ n × o))
          a₂ ha₂) →
      σ = a₂

Tactic:
_