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
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
rw [det_apply]
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
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
refine' (natDegree_sum_le _ _).trans _
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
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
refine' Multiset.max_nat_le_of_forall_le _ _ _
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
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
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]
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
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
intro g
no goals
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
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
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)

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)
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)
cases' Int.units_eq_one_or (sign g) with sg sg
no goals
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)
rw [sg, one_smul]
no goals
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)
rw [sg, Units.neg_smul, one_smul, natDegree_neg]
no goals
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
simp [mul_one, Algebra.id.smul_eq_mul, Finset.card_univ]
no goals
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))
simp