-- 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:
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
h : q = 0
⊢ (Multiset.map (fun a => X - C a) (map i p).roots).prod * q = 0

Tactic:
rw [h, mul_zero]

Result:
no goals

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
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

Tactic:
rw [← splits_id_iff_splits, ← he] at hsplit

Result:
case neg.intro.intro.intro
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
hp : ¬map i p = 0
q : L[X]
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
⊢ (map i p).natDegree = (map i p).roots.card

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
⊢ (Multiset.map (fun a => X - C a) (map i p).roots).prod * q ≠ 0

Tactic:
exact mul_ne_zero monic_prod_multiset_X_sub_C.ne_zero hq

Result:
no goals

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
⊢ False

Tactic:
have h' : (map (RingHom.id L) q).natDegree ≠ 0 := by simp [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
h' : (map (RingHom.id L) q).natDegree ≠ 0
⊢ False

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
⊢ (map i p).natDegree = (map i p).roots.card

Tactic:
have hq : q ≠ 0 := fun h => hp (by rw [h, mul_zero])

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
⊢ (map i p).natDegree = (map i p).roots.card

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 : (map (RingHom.id L) q).roots ≠ 0
⊢ False

Tactic:
rw [map_id] at this

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 : q.roots ≠ 0
⊢ False

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
⊢ (map i p).natDegree = (map i p).roots.card

Tactic:
rw [← hd, add_right_eq_self]

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
⊢ q.natDegree = 0

Proof state:
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
⊢ (map (RingHom.id L) q).natDegree ≠ 0

Tactic:
simp [h]

Result:
no goals

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
hp : ¬map i p = 0
q : L[X]
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
⊢ (map i p).natDegree = (map i p).roots.card

Tactic:
rw [← he] at hp

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
⊢ (map i p).natDegree = (map i p).roots.card