-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_succ_row {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) R) (i : Fin n.succ) :
    det A =
      ∑ j : Fin n.succ, (-1) ^ (i + j : ℕ) * A i j * det (A.submatrix i.succAbove j.succAbove)

Proof state:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ ∑ j : Fin n.succ,
      (-1) ^ ↑j * A.submatrix (⇑i.cycleRange⁻¹) id 0 j *
        ((A.submatrix (⇑i.cycleRange⁻¹) id).submatrix Fin.succ j.succAbove).det =
    ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Tactic:
refine Finset.sum_congr rfl fun j _ => ?_

Result:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * A.submatrix (⇑i.cycleRange⁻¹) id 0 j *
      ((A.submatrix (⇑i.cycleRange⁻¹) id).submatrix Fin.succ j.succAbove).det =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)

Proof state:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * A.submatrix (⇑i.cycleRange⁻¹) id 0 j *
      ((A.submatrix (⇑i.cycleRange⁻¹) id).submatrix Fin.succ j.succAbove).det =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)

Tactic:
rw [mul_assoc, Matrix.submatrix_apply, submatrix_submatrix, id_comp, Function.comp_def, id]

Result:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * (A (i.cycleRange⁻¹ 0) j * (A.submatrix (fun x => i.cycleRange⁻¹ x.succ) j.succAbove).det) =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det

Tactic:
calc
  det A = ↑((-1 : ℤˣ) ^ (i : ℕ) * (-1 : ℤˣ) ^ (i : ℕ) : ℤˣ) * det A := by simp
  _ = (-1 : R) ^ (i : ℕ) * (Perm.sign i.cycleRange⁻¹) * det A := by simp [-Int.units_mul_self]

Result:
no goals

Proof state:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ (-1) ^ ↑j * (A (i.cycleRange⁻¹ 0) j * (A.submatrix (fun x => i.cycleRange⁻¹ x.succ) j.succAbove).det) =
    (-1) ^ ↑j * (A i j * (A.submatrix i.succAbove j.succAbove).det)

Tactic:
congr

Result:
case e_a.e_a.e_a.e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ i.cycleRange⁻¹ 0 = i

case e_a.e_a.e_a.e_M
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ A.submatrix (fun x => i.cycleRange⁻¹ x.succ) j.succAbove = A.submatrix i.succAbove j.succAbove

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ A.det = (-1) ^ ↑i * ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Tactic:
rw [this, mul_assoc]

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ (-1) ^ ↑i * (↑↑(sign i.cycleRange⁻¹) * A.det) =
    (-1) ^ ↑i * ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = ↑↑((-1) ^ ↑i * (-1) ^ ↑i) * A.det

Tactic:
simp

Result:
no goals

Proof state:
case e_a.e_a.e_a.e_M
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ A.submatrix (fun x => i.cycleRange⁻¹ x.succ) j.succAbove = A.submatrix i.succAbove j.succAbove

Tactic:
ext i' j'

Result:
case e_a.e_a.e_a.e_M.a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
i' j' : Fin n
⊢ A.submatrix (fun x => i.cycleRange⁻¹ x.succ) j.succAbove i' j' = A.submatrix i.succAbove j.succAbove i' j'

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = ∑ j : Fin n.succ, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det

Tactic:
simp_rw [pow_add, mul_assoc, ← mul_sum]

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ A.det = (-1) ^ ↑i * ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Proof state:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ ↑↑(sign i.cycleRange⁻¹) * A.det =
    ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Tactic:
rw [← det_permute, det_succ_row_zero]

Result:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ ∑ j : Fin n.succ,
      (-1) ^ ↑j * A.submatrix (⇑i.cycleRange⁻¹) id 0 j *
        ((A.submatrix (⇑i.cycleRange⁻¹) id).submatrix Fin.succ j.succAbove).det =
    ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
⊢ ↑↑((-1) ^ ↑i * (-1) ^ ↑i) * A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det

Tactic:
simp [-Int.units_mul_self]

Result:
no goals

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ (-1) ^ ↑i * (↑↑(sign i.cycleRange⁻¹) * A.det) =
    (-1) ^ ↑i * ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Tactic:
congr

Result:
case e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ ↑↑(sign i.cycleRange⁻¹) * A.det =
    ∑ i_1 : Fin n.succ, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Proof state:
case e_a.e_a.e_a.e_a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
⊢ i.cycleRange⁻¹ 0 = i

Tactic:
rw [Equiv.Perm.inv_def, Fin.cycleRange_symm_zero]

Result:
no goals

Proof state:
case e_a.e_a.e_a.e_M.a
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
j : Fin n.succ
x✝ : j ∈ univ
i' j' : Fin n
⊢ A.submatrix (fun x => i.cycleRange⁻¹ x.succ) j.succAbove i' j' = A.submatrix i.succAbove j.succAbove i' j'

Tactic:
rw [Equiv.Perm.inv_def, Matrix.submatrix_apply, Matrix.submatrix_apply,
  Fin.cycleRange_symm_succ]

Result:
no goals