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

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

Tactic:
rw [Matrix.det_apply, Finset.univ_perm_fin_succ, ← Finset.univ_product_univ]

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ ∑ σ ∈ Finset.map decomposeFin.symm.toEmbedding (univ ×ˢ univ), sign σ • ∏ i : Fin n.succ, A (σ i) i =
    ∑ i : Fin n.succ, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ (-1 * ↑(sign σ)) • (A i.succ 0 * ∏ i' : Fin n, A (i.succ.succAbove (i.cycleRange (σ i'))) i'.succ) =
    -1 * (A i.succ 0 * ↑(sign σ) • ∏ i' : Fin n, A (i.succ.succAbove (i.cycleRange (σ i'))) i'.succ)

Tactic:
simp [mul_assoc, mul_comm, _root_.neg_mul, one_mul, zsmul_eq_mul, neg_inj, neg_smul,
  Fin.succAbove_cycleRange, mul_left_comm]

Result:
no goals

Proof state:
case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
x✝ : i ∈ univ
⊢ ∑ y : Perm (Fin n), sign (decomposeFin.symm (0, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (0, y)) x) x =
    (-1) ^ ↑0 * A 0 0 * (of fun i j => A (Fin.succAbove 0 i) j.succ).det

Tactic:
simp only [Fin.prod_univ_succ, Matrix.det_apply, Finset.mul_sum,
  Equiv.Perm.decomposeFin_symm_apply_zero, Fin.val_zero, one_mul,
  Equiv.Perm.decomposeFin.symm_sign, Equiv.swap_self, if_true, id, eq_self_iff_true,
  Equiv.Perm.decomposeFin_symm_apply_succ, Fin.succAbove_zero, Equiv.coe_refl, pow_zero,
  mul_smul_comm, of_apply]

Result:
no goals

Proof state:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ (-1 * sign σ) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, σ)) x) x =
    -1 *
      (A i.succ 0 *
        sign σ •
          ∏ i_1 : Fin n, (of fun i_2 j => A (i.succ.succAbove i_2) j.succ).submatrix (⇑i.cycleRange) id (σ i_1) i_1)

Tactic:
calc
  ((-1 * Perm.sign σ : ℤ) • ∏ i', A (Perm.decomposeFin.symm (Fin.succ i, σ) i') i') =
      (-1 * Perm.sign σ : ℤ) • (A (Fin.succ i) 0 *
        ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by
    simp only [Fin.prod_univ_succ, Fin.succAbove_cycleRange,
      Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ]
  _ = -1 * (A (Fin.succ i) 0 * (Perm.sign σ : ℤ) •
      ∏ i', A ((Fin.succ i).succAbove (Fin.cycleRange i (σ i'))) i'.succ) := by
    simp [mul_assoc, mul_comm, _root_.neg_mul, one_mul, zsmul_eq_mul, neg_inj, neg_smul,
      Fin.succAbove_cycleRange, mul_left_comm]

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
x✝ : i✝ ∈ univ
i : Fin n
⊢ (-1) ^ ↑i = ↑↑(sign i.cycleRange)

Tactic:
simp [Fin.sign_cycleRange]

Result:
no goals

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ ∑ x : Fin n.succ,
      ∑ y : Perm (Fin n), sign (decomposeFin.symm (x, y)) • ∏ x_1 : Fin n.succ, A ((decomposeFin.symm (x, y)) x_1) x_1 =
    ∑ x : Fin n.succ, (-1) ^ ↑x * A x 0 * (of fun i j => A (x.succAbove i) j.succ).det

Tactic:
refine Finset.sum_congr rfl fun i _ => Fin.cases ?_ (fun i => ?_) i

Result:
case refine_1
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
x✝ : i ∈ univ
⊢ ∑ y : Perm (Fin n), sign (decomposeFin.symm (0, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (0, y)) x) x =
    (-1) ^ ↑0 * A 0 0 * (of fun i j => A (Fin.succAbove 0 i) j.succ).det

case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
⊢ ∑ y : Perm (Fin n), sign (decomposeFin.symm (i.succ, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, y)) x) x =
    (-1) ^ ↑i.succ * A i.succ 0 * (of fun i_1 j => A (i.succ.succAbove i_1) j.succ).det

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ (-1 * ↑(sign σ)) • ∏ i' : Fin n.succ, A ((decomposeFin.symm (i.succ, σ)) i') i' =
    (-1 * ↑(sign σ)) • (A i.succ 0 * ∏ i' : Fin n, A (i.succ.succAbove (i.cycleRange (σ i'))) i'.succ)

Tactic:
simp only [Fin.prod_univ_succ, Fin.succAbove_cycleRange,
  Equiv.Perm.decomposeFin_symm_apply_zero, Equiv.Perm.decomposeFin_symm_apply_succ]

Result:
no goals

Proof state:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ ∑ σ ∈ Finset.map decomposeFin.symm.toEmbedding (univ ×ˢ univ), sign σ • ∏ i : Fin n.succ, A (σ i) i =
    ∑ i : Fin n.succ, (-1) ^ ↑i * A i 0 * (A.submatrix i.succAbove Fin.succ).det

Tactic:
simp only [Finset.sum_map, Equiv.toEmbedding_apply, Finset.sum_product, Matrix.submatrix]

Result:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
⊢ ∑ x : Fin n.succ,
      ∑ y : Perm (Fin n), sign (decomposeFin.symm (x, y)) • ∏ x_1 : Fin n.succ, A ((decomposeFin.symm (x, y)) x_1) x_1 =
    ∑ x : Fin n.succ, (-1) ^ ↑x * A x 0 * (of fun i j => A (x.succAbove i) j.succ).det

Proof state:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y : Perm (Fin n), sign (decomposeFin.symm (i.succ, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, y)) x) x =
    ∑ i_1 : Perm (Fin n),
      -1 *
        (A i.succ 0 *
          sign i_1 •
            ∏ i_2 : Fin n, (of fun i_3 j => A (i.succ.succAbove i_3) j.succ).submatrix (⇑i.cycleRange) id (i_1 i_2) i_2)

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

Result:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝¹ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
σ : Perm (Fin n)
x✝ : σ ∈ univ
⊢ sign (decomposeFin.symm (i.succ, σ)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, σ)) x) x =
    -1 *
      (A i.succ 0 *
        sign σ •
          ∏ i_1 : Fin n, (of fun i_2 j => A (i.succ.succAbove i_2) j.succ).submatrix (⇑i.cycleRange) id (σ i_1) i_1)

Proof state:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
⊢ ∑ y : Perm (Fin n), sign (decomposeFin.symm (i.succ, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, y)) x) x =
    (-1) ^ ↑i.succ * A i.succ 0 * (of fun i_1 j => A (i.succ.succAbove i_1) j.succ).det

Tactic:
have : (-1 : R) ^ (i : ℕ) = (Perm.sign i.cycleRange) := by simp [Fin.sign_cycleRange]

Result:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y : Perm (Fin n), sign (decomposeFin.symm (i.succ, y)) • ∏ x : Fin n.succ, A ((decomposeFin.symm (i.succ, y)) x) x =
    (-1) ^ ↑i.succ * A i.succ 0 * (of fun i_1 j => A (i.succ.succAbove i_1) j.succ).det