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) (Fintype.card n) =
    ∑ σ : Equiv.Perm n, ↑sign σ • ∏ i : n, A (↑σ 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)) (Fintype.card n) = det A
rw [det_apply, det_apply, finset_sum_coeff]
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) (Fintype.card n) =
        ↑sign x • ∏ i : n, A (↑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) (Fintype.card n) =
    ∑ σ : Equiv.Perm n, ↑sign σ • ∏ i : n, A (↑σ 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 α
⊢ ∀ (x : Equiv.Perm n),
    coeff (↑sign x • ∏ x_1 : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑x x_1) x_1) (Fintype.card n) =
      ↑sign x • ∏ x_1 : n, A (↑x x_1) x_1
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) (Fintype.card n) =
        ↑sign x • ∏ i : n, A (↑x i) i
simp only [Algebra.id.smul_eq_mul, Finset.mem_univ, RingHom.mapMatrix_apply, forall_true_left,
  map_apply, Pi.smul_apply]
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 • ∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) (Fintype.card n) =
    ↑sign g • ∏ x : n, A (↑g x) x
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (x : Equiv.Perm n),
    coeff (↑sign x • ∏ x_1 : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑x x_1) x_1) (Fintype.card n) =
      ↑sign x • ∏ x_1 : n, A (↑x x_1) x_1
intro 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
⊢ ∏ x : n, A (↑g x) x = coeff (∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) (Fintype.card n)
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 • ∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) (Fintype.card n) =
    ↑sign g • ∏ x : n, A (↑g x) x
convert coeff_smul (R := α) (sign 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
⊢ ∏ x : n, A (↑g x) x = coeff (∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) (Fintype.card n * 1)
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, A (↑g x) x = coeff (∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) (Fintype.card n)
rw [← mul_one (Fintype.card n)]
case h.e'_2.a
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
a✝ : x✝ ∈ Finset.univ
⊢ A (↑g x✝) x✝ = coeff ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x✝) x✝) 1

case h.e'_3.h.e'_6.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ (p : n), p ∈ Finset.univ → natDegree ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g p) p) ≤ 1
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, A (↑g x) x = coeff (∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) (Fintype.card n * 1)
convert (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm
no goals
case h.e'_2.a
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
a✝ : x✝ ∈ Finset.univ
⊢ A (↑g x✝) x✝ = coeff ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x✝) x✝) 1
simp [coeff_C]
case h.e'_3.h.e'_6.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
p : n
⊢ natDegree ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g p) p) ≤ 1
case h.e'_3.h.e'_6.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ ∀ (p : n), p ∈ Finset.univ → natDegree ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g p) p) ≤ 1
rintro p -
case h.e'_3.h.e'_6.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
p : n
⊢ max (natDegree ((X • Matrix.map A ↑C) (↑g p) p)) (natDegree (Matrix.map B (↑C) (↑g p) p)) ≤ 1
case h.e'_3.h.e'_6.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
p : n
⊢ natDegree ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g p) p) ≤ 1
refine' (natDegree_add_le _ _).trans _
no goals
case h.e'_3.h.e'_6.convert_5
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
p : n
⊢ max (natDegree ((X • Matrix.map A ↑C) (↑g p) p)) (natDegree (Matrix.map B (↑C) (↑g p) p)) ≤ 1
simpa [Pi.smul_apply, map_apply, Algebra.id.smul_eq_mul, X_mul_C, natDegree_C,
  max_eq_left, zero_le'] using (natDegree_C_mul_le _ _).trans (natDegree_X_le (R := α))