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

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.coeff (Fintype.card n) = A.det

Tactic:
rw [det_apply, det_apply, finset_sum_coeff]

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

Proof state:
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, A (g i) i = (∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n)

Tactic:
rw [← mul_one (Fintype.card n)]

Result:
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, A (g i) i = (∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n * 1)

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

Tactic:
simp only [Algebra.id.smul_eq_mul, Finset.mem_univ, RingHom.mapMatrix_apply, forall_true_left,
  map_apply, Pi.smul_apply]

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

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

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

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

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

Tactic:
refine Finset.sum_congr rfl ?_

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

Proof state:
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 ∈ Finset.univ, ((X • A.map ⇑C + B.map ⇑C) (g p) p).natDegree ≤ 1

Tactic:
rintro p -

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

Proof state:
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✝ = ((X • A.map ⇑C + B.map ⇑C) (g x✝) x✝).coeff 1

Tactic:
simp [coeff_C]

Result:
no goals

Proof state:
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
⊢ (X * C (A (g p) p) + C (B (g p) p)).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 : Equiv.Perm n),
    (sign x • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (x i) i).coeff (Fintype.card n) = sign x • ∏ i : n, A (x i) i

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).coeff (Fintype.card n) = sign g • ∏ i : n, A (g i) i

Proof state:
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, A (g i) i = (∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n * 1)

Tactic:
convert (coeff_prod_of_natDegree_le (R := α) _ _ _ _).symm

Result:
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✝ = ((X • A.map ⇑C + B.map ⇑C) (g x✝) x✝).coeff 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 ∈ Finset.univ, ((X • A.map ⇑C + B.map ⇑C) (g p) p).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
⊢ (sign g • ∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n) = sign g • ∏ i : n, A (g i) i

Tactic:
convert coeff_smul (R := α) (sign g) _ _

Result:
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, A (g i) i = (∏ i : n, (X • A.map ⇑C + B.map ⇑C) (g i) i).coeff (Fintype.card n)