-- Mathlib/Algebra/Polynomial/Splits.lean
theorem natDegree_eq_card_roots' {p : K[X]} {i : K →+* L} (hsplit : Splits i p) :
    (p.map i).natDegree = Multiset.card (p.map i).roots

Proof state:
case neg.intro.intro.intro.refine_2
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0
hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)
he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p
hd : (map i p).roots.card + q.natDegree = (map i p).natDegree
hr : q.roots = 0
hq : q ≠ 0
h : ¬q.natDegree = 0
h' : (map (RingHom.id L) q).natDegree ≠ 0
this : q.roots ≠ 0
⊢ False

Tactic:
exact this hr

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ (map i p).natDegree = (map i p).roots.card

Tactic:
by_cases hp : p.map i = 0

Result:
case pos
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : map i p = 0
⊢ (map i p).natDegree = (map i p).roots.card

case neg
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : ¬map i p = 0
⊢ (map i p).natDegree = (map i p).roots.card

Proof state:
case neg.intro.intro.intro
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0
hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)
he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p
hd : (map i p).roots.card + q.natDegree = (map i p).natDegree
hr : q.roots = 0
hq : q ≠ 0
h : ¬q.natDegree = 0
h' : (map (RingHom.id L) q).natDegree ≠ 0
⊢ False

Tactic:
have := roots_ne_zero_of_splits' (RingHom.id L) (splits_of_splits_mul' _ ?_ hsplit).2 h'

Result:
case neg.intro.intro.intro.refine_2
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0
hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)
he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p
hd : (map i p).roots.card + q.natDegree = (map i p).natDegree
hr : q.roots = 0
hq : q ≠ 0
h : ¬q.natDegree = 0
h' : (map (RingHom.id L) q).natDegree ≠ 0
this : (map (RingHom.id L) q).roots ≠ 0
⊢ False

case neg.intro.intro.intro.refine_1
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0
hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)
he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p
hd : (map i p).roots.card + q.natDegree = (map i p).natDegree
hr : q.roots = 0
hq : q ≠ 0
h : ¬q.natDegree = 0
h' : (map (RingHom.id L) q).natDegree ≠ 0
⊢ map (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q) ≠ 0

Proof state:
case pos
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : map i p = 0
⊢ (map i p).natDegree = (map i p).roots.card

Tactic:
rw [hp, natDegree_zero, roots_zero, Multiset.card_zero]

Result:
no goals

Proof state:
case neg
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : ¬map i p = 0
⊢ (map i p).natDegree = (map i p).roots.card

Tactic:
obtain ⟨q, he, hd, hr⟩ := exists_prod_multiset_X_sub_C_mul (p.map i)

Result:
case neg.intro.intro.intro
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
hp : ¬map i p = 0
q : L[X]
he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p
hd : (map i p).roots.card + q.natDegree = (map i p).natDegree
hr : q.roots = 0
⊢ (map i p).natDegree = (map i p).roots.card

Proof state:
case neg.intro.intro.intro
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0
hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)
he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p
hd : (map i p).roots.card + q.natDegree = (map i p).natDegree
hr : q.roots = 0
hq : q ≠ 0
⊢ q.natDegree = 0

Tactic:
by_contra h

Result:
case neg.intro.intro.intro
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0
hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)
he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p
hd : (map i p).roots.card + q.natDegree = (map i p).natDegree
hr : q.roots = 0
hq : q ≠ 0
h : ¬q.natDegree = 0
⊢ False

Proof state:
case neg.intro.intro.intro.refine_1
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0
hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)
he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p
hd : (map i p).roots.card + q.natDegree = (map i p).natDegree
hr : q.roots = 0
hq : q ≠ 0
h : ¬q.natDegree = 0
h' : (map (RingHom.id L) q).natDegree ≠ 0
⊢ map (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q) ≠ 0

Tactic:
rw [map_id]

Result:
case neg.intro.intro.intro.refine_1
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
q : L[X]
hp : ¬(Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0
hsplit : Splits (RingHom.id L) ((Multiset.map (fun a => X - C a) (map i p).roots).prod * q)
he : (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = map i p
hd : (map i p).roots.card + q.natDegree = (map i p).natDegree
hr : q.roots = 0
hq : q ≠ 0
h : ¬q.natDegree = 0
h' : (map (RingHom.id L) q).natDegree ≠ 0
⊢ (Multiset.map (fun a => X - C a) (map i p).roots).prod * q ≠ 0