-- Mathlib/LinearAlgebra/Matrix/Polynomial.lean
theorem natDegree_det_X_add_C_le (A B : Matrix n n α) :
    natDegree (det ((X : α[X]) • A.map C + B.map C : Matrix n n α[X])) ≤ Fintype.card n

Proof state:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (a : Equiv.Perm n), (sign a • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (a i) i).natDegree ≤ Fintype.card n

Tactic:
intro g

Result:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ (sign g • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree ≤ Fintype.card n

Proof state:
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
⊢ (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).natDegree

Tactic:
rw [sg, one_smul]

Result:
no goals

Proof state:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ x ∈ Multiset.map (natDegree ∘ fun σ => sign σ • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (σ i) i) Finset.univ.val,
    x ≤ Fintype.card n

Tactic:
simp only [forall_apply_eq_imp_iff, true_and, Function.comp_apply, Multiset.map_map,
  Multiset.mem_map, exists_imp, Finset.mem_univ_val]

Result:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ (a : Equiv.Perm n), (sign a • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (a i) i).natDegree ≤ Fintype.card n

Proof state:
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
⊢ (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).natDegree

Tactic:
rw [sg, Units.neg_smul, one_smul, natDegree_neg]

Result:
no goals

Proof state:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (∑ σ : Equiv.Perm n, sign σ • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (σ i) i).natDegree ≤ Fintype.card n

Tactic:
refine (natDegree_sum_le _ _).trans ?_

Result:
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 • A.map ⇑C + B.map ⇑C) (σ i) i) Finset.univ ≤
    Fintype.card n

Proof state:
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.univ.card • 1 ≤ Fintype.card n

Tactic:
simp [mul_one, Algebra.id.smul_eq_mul, Finset.card_univ]

Result:
no goals

Proof state:
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 • A.map ⇑C + B.map ⇑C) (σ i) i) Finset.univ ≤
    Fintype.card n

Tactic:
refine Multiset.max_le_of_forall_le _ _ ?_

Result:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ ∀ x ∈ Multiset.map (natDegree ∘ fun σ => sign σ • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (σ i) i) Finset.univ.val,
    x ≤ Fintype.card n

Proof state:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
g : Equiv.Perm n
⊢ (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).natDegree

Tactic:
rcases Int.units_eq_one_or (sign g) with sg | sg

Result:
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
⊢ (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).natDegree

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
⊢ (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).natDegree

Proof state:
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
⊢ ((X • A.map ⇑C + B.map ⇑C) (g i) i).natDegree ≤ 1

Tactic:
dsimp only [add_apply, smul_apply, map_apply, smul_eq_mul]

Result:
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
⊢ (X * C (A (g i) i) + C (B (g i) i)).natDegree ≤ 1

Proof state:
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
⊢ (X * C (A (g i) i) + C (B (g i) i)).natDegree ≤ 1

Tactic:
compute_degree

Result:
no goals

Proof state:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (X • A.map ⇑C + B.map ⇑C).det.natDegree ≤ Fintype.card n

Tactic:
rw [det_apply]

Result:
n : Type u_1
α : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A B : Matrix n n α
⊢ (∑ σ : Equiv.Perm n, sign σ • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (σ i) i).natDegree ≤ Fintype.card n