-- Mathlib/Algebra/Polynomial/Roots.lean
theorem exists_prod_multiset_X_sub_C_mul (p : R[X]) :
    ∃ q,
      (p.roots.map fun a => X - C a).prod * q = p ∧
        Multiset.card p.roots + q.natDegree = p.natDegree ∧ q.roots = 0

Proof state:
case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ q.roots = 0

Tactic:
replace he := congr_arg roots he.symm

Result:
case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : ((Multiset.map (fun a => X - C a) p.roots).prod * q).roots = p.roots
⊢ q.roots = 0

Proof state:
case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * 0
⊢ p.roots.card + natDegree 0 = p.natDegree ∧ roots 0 = 0

Tactic:
rw [mul_zero] at he

Result:
case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
he : p = 0
⊢ p.roots.card + natDegree 0 = p.natDegree ∧ roots 0 = 0

Proof state:
case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (roots 0).card + natDegree 0 = natDegree 0 ∧ roots 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : p.roots + q.roots = p.roots
⊢ q.roots = 0

case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : ((Multiset.map (fun a => X - C a) p.roots).prod * q).roots = p.roots
⊢ (Multiset.map (fun a => X - C a) p.roots).prod * q ≠ 0

Tactic:
exacts [add_right_eq_self.1 he, mul_ne_zero monic_prod_multiset_X_sub_C.ne_zero hq]

Result:
no goals

Proof state:
case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : ((Multiset.map (fun a => X - C a) p.roots).prod * q).roots = p.roots
⊢ q.roots = 0

Tactic:
rw [roots_mul, roots_multiset_prod_X_sub_C] at he

Result:
case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : p.roots + q.roots = p.roots
⊢ q.roots = 0

case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hq : q ≠ 0
he : ((Multiset.map (fun a => X - C a) p.roots).prod * q).roots = p.roots
⊢ (Multiset.map (fun a => X - C a) p.roots).prod * q ≠ 0

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ ∃ q, (Multiset.map (fun a => X - C a) p.roots).prod * q = p ∧ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

Tactic:
obtain ⟨q, he⟩ := p.prod_multiset_X_sub_C_dvd

Result:
case intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
⊢ ∃ q, (Multiset.map (fun a => X - C a) p.roots).prod * q = p ∧ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

Proof state:
case right.inr.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = ((Multiset.map (fun a => X - C a) p.roots).prod * q).natDegree

Tactic:
rw [monic_prod_multiset_X_sub_C.natDegree_mul' hq, natDegree_multiset_prod_X_sub_C_eq_card]

Result:
no goals

Proof state:
case right.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

Tactic:
constructor

Result:
case right.inr.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.natDegree

case right.inr.right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ q.roots = 0

Proof state:
case right.inr.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.natDegree

Tactic:
conv_rhs => rw [he]

Result:
case right.inr.left
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = ((Multiset.map (fun a => X - C a) p.roots).prod * q).natDegree

Proof state:
case intro
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
⊢ ∃ q, (Multiset.map (fun a => X - C a) p.roots).prod * q = p ∧ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

Tactic:
use q, he.symm

Result:
case right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

Proof state:
case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
he : p = 0
⊢ p.roots.card + natDegree 0 = p.natDegree ∧ roots 0 = 0

Tactic:
subst he

Result:
case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ (roots 0).card + natDegree 0 = natDegree 0 ∧ roots 0 = 0

Proof state:
case right
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0

Tactic:
obtain rfl | hq := eq_or_ne q 0

Result:
case right.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * 0
⊢ p.roots.card + natDegree 0 = p.natDegree ∧ roots 0 = 0

case right.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
he : p = (Multiset.map (fun a => X - C a) p.roots).prod * q
hq : q ≠ 0
⊢ p.roots.card + q.natDegree = p.natDegree ∧ q.roots = 0