[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ natDegree (det (X • Matrix.map A ↑C + Matrix.map B ↑C)) ≤ Fintype.card n
[PROOFSTEP]
rw [det_apply]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ natDegree (∑ σ : Equiv.Perm n, ↑sign σ • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑σ i) i) ≤ Fintype.card n
[PROOFSTEP]
refine' (natDegree_sum_le _ _).trans _
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ Finset.fold max 0 (natDegree ∘ fun σ => ↑sign σ • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑σ i) i)
      Finset.univ ≤
    Fintype.card n
[PROOFSTEP]
refine' Multiset.max_nat_le_of_forall_le _ _ _
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (x : ℕ),
    x ∈
        Multiset.map (natDegree ∘ fun σ => ↑sign σ • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑σ i) i)
          Finset.univ.val →
      x ≤ Fintype.card n
[PROOFSTEP]
simp only [forall_apply_eq_imp_iff', true_and_iff, Function.comp_apply, Multiset.map_map, Multiset.mem_map, exists_imp,
  Finset.mem_univ_val]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (a : Equiv.Perm n), natDegree (↑sign a • ∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑a x) x) ≤ Fintype.card n
[PROOFSTEP]
intro g
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ natDegree (↑sign g • ∏ x : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g x) x) ≤ Fintype.card n
[PROOFSTEP]
calc
  natDegree (sign g • ∏ i : n, (X • A.map C + B.map C) (g i) i) ≤
      natDegree (∏ i : n, (X • A.map C + B.map C) (g i) i) :=
    by
    cases' Int.units_eq_one_or (sign g) with sg sg
    · rw [sg, one_smul]
    · rw [sg, Units.neg_smul, one_smul, natDegree_neg]
  _ ≤ ∑ i : n, natDegree (((X : α[X]) • A.map C + B.map C) (g i) i) :=
    (natDegree_prod_le (Finset.univ : Finset n) fun i : n => (X • A.map C + B.map C) (g i) i)
  _ ≤ Finset.univ.card • 1 := (Finset.sum_le_card_nsmul _ _ 1 fun (i : n) _ => ?_)
  _ ≤ Fintype.card n := by simp [mul_one, Algebra.id.smul_eq_mul, Finset.card_univ]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ natDegree (↑sign g • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) ≤
    natDegree (∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i)
[PROOFSTEP]
cases' Int.units_eq_one_or (sign g) with sg sg
[GOAL]
case inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : ↑sign g = 1
⊢ natDegree (↑sign g • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) ≤
    natDegree (∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i)
[PROOFSTEP]
rw [sg, one_smul]
[GOAL]
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
sg : ↑sign g = -1
⊢ natDegree (↑sign g • ∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) ≤
    natDegree (∏ i : n, (X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i)
[PROOFSTEP]
rw [sg, Units.neg_smul, one_smul, natDegree_neg]
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ Finset.card Finset.univ • 1 ≤ Fintype.card n
[PROOFSTEP]
simp [mul_one, Algebra.id.smul_eq_mul, Finset.card_univ]
[GOAL]
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
x✝ : i ∈ Finset.univ
⊢ natDegree ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) ≤ 1
[PROOFSTEP]
calc
  natDegree (((X : α[X]) • A.map C + B.map C) (g i) i) = natDegree ((X : α[X]) * C (A (g i) i) + C (B (g i) i)) := by
    simp
  _ ≤ max (natDegree ((X : α[X]) * C (A (g i) i))) (natDegree (C (B (g i) i))) := (natDegree_add_le _ _)
  _ = natDegree ((X : α[X]) * C (A (g i) i)) := (max_eq_left ((natDegree_C _).le.trans (zero_le _)))
  _ ≤ natDegree (X : α[X]) := (natDegree_mul_C_le _ _)
  _ ≤ 1 := natDegree_X_le
[GOAL]
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
x✝ : i ∈ Finset.univ
⊢ natDegree ((X • Matrix.map A ↑C + Matrix.map B ↑C) (↑g i) i) = natDegree (X * ↑C (A (↑g i) i) + ↑C (B (↑g i) i))
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
rw [det_apply, finset_sum_coeff, det_apply]
[GOAL]
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
[PROOFSTEP]
refine' Finset.sum_congr rfl _
[GOAL]
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
[PROOFSTEP]
rintro g -
[GOAL]
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
[PROOFSTEP]
convert coeff_smul (R := α) (sign g) _ 0
[GOAL]
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
[PROOFSTEP]
rw [coeff_zero_prod]
[GOAL]
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
[PROOFSTEP]
refine' Finset.prod_congr rfl _
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
rw [det_apply, det_apply, finset_sum_coeff]
[GOAL]
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
[PROOFSTEP]
refine' Finset.sum_congr rfl _
[GOAL]
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
[PROOFSTEP]
simp only [Algebra.id.smul_eq_mul, Finset.mem_univ, RingHom.mapMatrix_apply, forall_true_left, map_apply, Pi.smul_apply]
[GOAL]
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
[PROOFSTEP]
intro g
[GOAL]
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
[PROOFSTEP]
convert coeff_smul (R := α) (sign g) _ _
[GOAL]
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)
[PROOFSTEP]
rw [← mul_one (Fintype.card n)]
[GOAL]
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)
[PROOFSTEP]
convert (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm
[GOAL]
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
[PROOFSTEP]
simp [coeff_C]
[GOAL]
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
[PROOFSTEP]
rintro p -
[GOAL]
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
[PROOFSTEP]
refine' (natDegree_add_le _ _).trans _
[GOAL]
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
[PROOFSTEP]
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 := α))
[GOAL]
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1
[PROOFSTEP]
cases subsingleton_or_nontrivial α
[GOAL]
case inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Subsingleton α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1
[PROOFSTEP]
simp
[GOAL]
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ leadingCoeff (det (X • 1 + Matrix.map A ↑C)) = 1
[PROOFSTEP]
rw [← @det_one n, ← coeff_det_X_add_C_card _ A, leadingCoeff]
[GOAL]
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
simp only [Matrix.map_one, C_eq_zero, RingHom.map_one]
[GOAL]
case inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
cases' (natDegree_det_X_add_C_le 1 A).eq_or_lt with h h
[GOAL]
case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) = Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
simp only [RingHom.map_one, Matrix.map_one, C_eq_zero] at h 
[GOAL]
case inr.inl
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • 1 + Matrix.map A ↑C)) = Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
rw [h]
[GOAL]
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
have H := coeff_eq_zero_of_natDegree_lt h
[GOAL]
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
H : coeff (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) (Fintype.card n) = 0
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
rw [coeff_det_X_add_C_card] at H 
[GOAL]
case inr.inr
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
h✝ : Nontrivial α
h : natDegree (det (X • Matrix.map 1 ↑C + Matrix.map A ↑C)) < Fintype.card n
H : det 1 = 0
⊢ coeff (det (X • 1 + Matrix.map A ↑C)) (natDegree (det (X • 1 + Matrix.map A ↑C))) =
    coeff (det (X • 1 + Matrix.map A ↑C)) (Fintype.card n)
[PROOFSTEP]
simp at H 
