-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_diagonal {d : n → R} : det (diagonal d) = ∏ i, d i

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ (diagonal d).det = ∏ i : n, d i

Tactic:
rw [det_apply']

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, diagonal d (σ i) i = ∏ i : n, d i

Proof state:
case h.e'_2.h.e'_6
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬σ x = 1 x
⊢ diagonal d (σ x) x = 0

Tactic:
exact if_neg h3

Result:
no goals

Proof state:
case refine_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ∀ b ∈ univ, b ≠ 1 → ↑↑(sign b) * ∏ i : n, diagonal d (b i) i = 0

Tactic:
rintro σ - h2

Result:
case refine_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
⊢ ↑↑(sign σ) * ∏ i : n, diagonal d (σ i) i = 0

Proof state:
case h.e'_2.h.e'_6
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬σ x = 1 x
⊢ ∏ i : n, diagonal d (σ i) i = 0

Tactic:
apply Finset.prod_eq_zero (mem_univ x)

Result:
case h.e'_2.h.e'_6
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬σ x = 1 x
⊢ diagonal d (σ x) x = 0

Proof state:
case refine_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
⊢ ↑↑(sign σ) * ∏ i : n, diagonal d (σ i) i = 0

Tactic:
obtain ⟨x, h3⟩ := not_forall.1 (mt Equiv.ext h2)

Result:
case refine_1.intro
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬σ x = 1 x
⊢ ↑↑(sign σ) * ∏ i : n, diagonal d (σ i) i = 0

Proof state:
case refine_2
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ 1 ∉ univ → ↑↑(sign 1) * ∏ i : n, diagonal d (1 i) i = 0

Tactic:
simp

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, diagonal d (σ i) i = ∏ i : n, d i

Tactic:
refine (Finset.sum_eq_single 1 ?_ ?_).trans ?_

Result:
case refine_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ∀ b ∈ univ, b ≠ 1 → ↑↑(sign b) * ∏ i : n, diagonal d (b i) i = 0

case refine_2
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ 1 ∉ univ → ↑↑(sign 1) * ∏ i : n, diagonal d (1 i) i = 0

case refine_3
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ↑↑(sign 1) * ∏ i : n, diagonal d (1 i) i = ∏ i : n, d i

Proof state:
case refine_3
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ↑↑(sign 1) * ∏ i : n, diagonal d (1 i) i = ∏ i : n, d i

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.intro
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬σ x = 1 x
⊢ ↑↑(sign σ) * ∏ i : n, diagonal d (σ i) i = 0

Tactic:
convert mul_zero (ε σ)

Result:
case h.e'_2.h.e'_6
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬σ x = 1 x
⊢ ∏ i : n, diagonal d (σ i) i = 0