m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ∑ σ : Perm n, ↑↑(↑sign σ) * ∏ i : n, diagonal d (↑σ i) i = ∏ i : n, d i
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
⊢ det (diagonal d) = ∏ i : n, d i
rw [det_apply']
case refine'_1
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ∀ (b : Perm n), b ∈ univ → b ≠ 1 → ↑↑(↑sign b) * ∏ i : n, diagonal d (↑b i) i = 0

case refine'_2
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ¬1 ∈ univ → ↑↑(↑sign 1) * ∏ i : n, diagonal d (↑1 i) i = 0

case refine'_3
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ↑↑(↑sign 1) * ∏ i : n, diagonal d (↑1 i) i = ∏ i : n, d i
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ∑ σ : Perm n, ↑↑(↑sign σ) * ∏ i : n, diagonal d (↑σ i) i = ∏ i : n, d i
refine' (Finset.sum_eq_single 1 _ _).trans _
case refine'_1
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
⊢ ↑↑(↑sign σ) * ∏ i : n, diagonal d (↑σ i) i = 0
case refine'_1
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ∀ (b : Perm n), b ∈ univ → b ≠ 1 → ↑↑(↑sign b) * ∏ i : n, diagonal d (↑b i) i = 0
rintro σ - h2
case refine'_1.intro
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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
case refine'_1
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
⊢ ↑↑(↑sign σ) * ∏ i : n, diagonal d (↑σ i) i = 0
cases' not_forall.1 (mt Equiv.ext h2) with x h3
case h.e'_2.h.e'_6
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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
case refine'_1.intro
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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
convert MulZeroClass.mul_zero (ε σ)
case h.e'_2.h.e'_6
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬↑σ x = ↑1 x
⊢ diagonal d (↑σ x) x = 0
case h.e'_2.h.e'_6
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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
apply Finset.prod_eq_zero (mem_univ x)
no goals
case h.e'_2.h.e'_6
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
σ : Perm n
h2 : σ ≠ 1
x : n
h3 : ¬↑σ x = ↑1 x
⊢ diagonal d (↑σ x) x = 0
exact if_neg h3
no goals
case refine'_2
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ¬1 ∈ univ → ↑↑(↑sign 1) * ∏ i : n, diagonal d (↑1 i) i = 0
simp
no goals
case refine'_3
m : Type ?u.110979
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
d : n → R
⊢ ↑↑(↑sign 1) * ∏ i : n, diagonal d (↑1 i) i = ∏ i : n, d i
simp