-- Mathlib/FieldTheory/SeparableDegree.lean
theorem eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits (hm : f.Monic)
    (hs : f.Splits (RingHom.id F))
    (h : f.natSepDegree = 1) : ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = (X - C y) ^ m

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod
h2 : (f.aroots F).toFinset.card = f.natSepDegree
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Tactic:
rw [h, aroots_def, Algebra.id.map_eq_id, map_id, Multiset.toFinset_card_eq_one_iff] at h2

Result:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod
h2 : f.roots.card ≠ 0 ∧ ∃ a, f.roots = f.roots.card • {a}
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Tactic:
have h1 := eq_prod_roots_of_monic_of_splits_id hm hs

Result:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Tactic:
have h2 := (natSepDegree_eq_of_splits f hs).symm

Result:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod
h2 : (f.aroots F).toFinset.card = f.natSepDegree
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod
h2 : f.roots.card ≠ 0 ∧ ∃ a, f.roots = f.roots.card • {a}
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Tactic:
obtain ⟨h2, y, h3⟩ := h2

Result:
case intro.intro
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod
h2 : f.roots.card ≠ 0
y : F
h3 : f.roots = f.roots.card • {y}
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Tactic:
classical
have h1 := eq_prod_roots_of_monic_of_splits_id hm hs
have h2 := (natSepDegree_eq_of_splits f hs).symm
rw [h, aroots_def, Algebra.id.map_eq_id, map_id, Multiset.toFinset_card_eq_one_iff] at h2
obtain ⟨h2, y, h3⟩ := h2
exact ⟨_, y, h2, by rwa [h3, Multiset.map_nsmul, Multiset.map_singleton, Multiset.prod_nsmul,
  Multiset.prod_singleton] at h1⟩

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod
h2 : f.roots.card ≠ 0
y : F
h3 : f.roots = f.roots.card • {y}
⊢ f = (X - C y) ^ f.roots.card

Tactic:
rwa [h3, Multiset.map_nsmul, Multiset.map_singleton, Multiset.prod_nsmul,
Multiset.prod_singleton] at h1

Result:
no goals

Proof state:
case intro.intro
F : Type u
inst✝ : Field F
f : F[X]
hm : f.Monic
hs : Splits (RingHom.id F) f
h : f.natSepDegree = 1
h1 : f = (Multiset.map (fun a => X - C a) f.roots).prod
h2 : f.roots.card ≠ 0
y : F
h3 : f.roots = f.roots.card • {y}
⊢ ∃ m y, m ≠ 0 ∧ f = (X - C y) ^ m

Tactic:
exact ⟨_, y, h2, by rwa [h3, Multiset.map_nsmul, Multiset.map_singleton, Multiset.prod_nsmul,
  Multiset.prod_singleton] at h1⟩

Result:
no goals