awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
have neg : i.castSucc ≠ k.succ
Tactic: rw [updateRow_ne]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ i.castSucc ≠ k.succ
have neg : i.castSucc < k.succ
Tactic: apply ne_of_lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ i.castSucc < k.succ
have neg : (↑i.castSucc : ℕ) < (↑k.succ : ℕ)
Tactic: rwa [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
have neg₁ : (↑i : ℕ) < (↑k.succ : ℕ)
Tactic: rwa [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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 : ℕ)
⊢ i.castSucc < k.succ
have neg₂ : (↑i : ℕ) < (↑k : ℕ) + 1
Tactic: rwa [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
⊢ i.castSucc < k.succ
have neg₃ : (↑i : ℕ) ≤ (↑k : ℕ)
Tactic: rwa [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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 : ℕ)
⊢ i.castSucc < k.succ
have neg₄ : ¬(↑k : ℕ) < (↑i : ℕ)
Tactic: rwa [Fin.lt_def, Fin.val_castSucc, Fin.val_succ, Nat.lt_succ_iff, ← not_lt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Determinant.Basic (goal)
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
have rw : Aᵀ.det = Bᵀ.det
Tactic: rw [← det_transpose A, ← det_transpose B]
-- 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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
⊢ (blockDiagonal M).det = ∏ k : o, (M k).det
have 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))
Tactic: simp_rw [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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
⊢ 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))
have 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) sorry)) : ℤ) : R)
        (∏ i : n, M (↑x : o) ((p (↑x : o) sorry : (a : n) → n) i) i))
Tactic: rw [Finset.prod_sum]
-- 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
o : Type u_3
inst_3 : Fintype o
inst_4 : DecidableEq o
M : o → Matrix n n R
⊢ 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))
have 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 sorry)) : ℤ) : R)
        (∏ x_2 : n, M x_1 ((x x_1 sorry : (a : n) → n) x_2) x_2))
Tactic: simp_rw [Finset.prod_attach_univ, Finset.univ_pi_univ]
-- 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
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}
⊢ 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))
have mem_preserving_snd : ∀ {σ : 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⟩⟩
-- 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
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)
    (∑ σ : 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))
have 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 sorry)) : ℤ) : R)
        (∏ x_2 : n, M x_1 ((x x_1 sorry : (a : n) → n) x_2) x_2))
Tactic: rw [← Finset.sum_subset (Finset.subset_univ preserving_snd) _]
-- 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
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))
⊢ 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))
have 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
Tactic: rw [← Finset.sum_subset (Finset.subset_univ preserving_snd) _]
-- 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
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))
have refine_1 : ∀ (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),
  (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 sorry : n × o ≃ n × o))
      a ha ∈
    preserving_snd
Tactic: refine (Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).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
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
refine_1 :
  ∀ (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),
    (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 ∈
      preserving_snd
⊢ 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))
have refine_2 : ∀ (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₁)
  (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 sorry : n × o ≃ n × o))
        a₁ 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 sorry : n × o ≃ n × o))
        a₂ ha₂) →
    a₁ = a₂
Tactic: refine (Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).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
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
refine_1 :
  ∀ (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),
    (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 ∈
      preserving_snd
refine_2 :
  ∀ (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₁)
    (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))
          a₁ 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₁ = a₂
⊢ 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))
have refine_3 : ∀ b ∈ preserving_snd,
  ∃ (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),
    (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 sorry : n × o ≃ n × o))
        a ha =
      b
Tactic: refine (Finset.sum_bij (fun σ _ => prodCongrLeft fun k ↦ σ k (mem_univ k)) ?_ ?_ ?_ ?_).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
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 σ
⊢ (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
have 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 sorry : n × o ≃ n × o))
            σ ha :
          (a : n × o) → n × o)
        x).2 =
    x.2
Tactic: rw [mem_preserving_snd]