no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
ha : ¬Polynomial.eval a F = 0
⊢ ∃ z,
    Polynomial.eval z F = 0 ∧
      ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ∧
        ‖Polynomial.eval z (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ∧
          ∀ (z' : ℤ_[p]), Polynomial.eval z' F = 0 → ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ → z' = z
exact ⟨soln_gen hnorm, eval_soln hnorm,
  soln_dist_to_a_lt_deriv hnorm ha, soln_deriv_norm hnorm, fun z => soln_unique hnorm ha z⟩