n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∑ b : Equiv.Perm n, coeff (↑sign b • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑b i) i) 0 =
    ∑ σ : Equiv.Perm n, ↑sign σ • ∏ i : n, B (↑σ i) i
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ coeff (det (X • Matrix.map A ↑C + Matrix.map B ↑C)) 0 = det B
rw [det_apply, finset_sum_coeff, det_apply]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (x : Equiv.Perm n),
    x ∈ Finset.univ →
      coeff (↑sign x • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑x i) i) 0 = ↑sign x • ∏ i : n, B (↑x i) i
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∑ b : Equiv.Perm n, coeff (↑sign b • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑b i) i) 0 =
    ∑ σ : Equiv.Perm n, ↑sign σ • ∏ i : n, B (↑σ i) i
refine' Finset.sum_congr rfl _
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ coeff (↑sign g • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) 0 = ↑sign g • ∏ i : n, B (↑g i) i
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (x : Equiv.Perm n),
    x ∈ Finset.univ →
      coeff (↑sign x • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑x i) i) 0 = ↑sign x • ∏ i : n, B (↑x i) i
rintro g -
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i : n, B (↑g i) i = coeff (∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) 0
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ coeff (↑sign g • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) 0 = ↑sign g • ∏ i : n, B (↑g i) i
convert coeff_smul (R := α) (sign g) _ 0
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i : n, B (↑g i) i = ∏ i : n, coeff ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) 0
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i : n, B (↑g i) i = coeff (∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) 0
rw [coeff_zero_prod]
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ (x : n), x ∈ Finset.univ → B (↑g x) x = coeff ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) 0
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∏ i : n, B (↑g i) i = ∏ i : n, coeff ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) 0
refine' Finset.prod_congr rfl _
no goals
case h.e'_3.h.e'_6
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ (x : n), x ∈ Finset.univ → B (↑g x) x = coeff ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) 0
simp