Theorem: KummersLemma.splits_poly (FltRegular/NumberTheory/KummersLemma/Field.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
α : L
e : α ^ ↑p = (algebraMap K L) ((algebraMap (𝓞 K) K) ↑u)
⊢ Splits (algebraMap (𝓞 K) L) (poly hp hζ u hcong)
Tactic:
rw [← splits_id_iff_splits, splits_iff_card_roots, roots_poly hp hζ u hcong α e,
  (monic_poly hp hζ u hcong).natDegree_map, natDegree_poly hp hζ,
  Finset.range_val, Multiset.card_map, Multiset.card_range]
State after:
no goals