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
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
⊢ ‖z - soln‖ = ‖z - a + (a - soln)‖
rw [sub_add_sub_cancel]
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
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ 0 = Polynomial.eval (soln + h) F
simp [hev]
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
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval (soln + h) F = Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
rw [hq, eval_soln, zero_add]
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
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2 =
    (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h
rw [sq, right_distrib, mul_assoc]
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
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
⊢ Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
simpa using eq_neg_of_add_eq_zero_left this
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
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖Polynomial.eval soln (↑Polynomial.derivative F)‖ = ‖-q * h‖
rw [this]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖-q‖ * ‖h‖ ≤ 1 * ‖h‖
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖-q * h‖ ≤ 1 * ‖h‖
rw [PadicInt.norm_mul]
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
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖-q‖ * ‖h‖ ≤ 1 * ‖h‖
exact mul_le_mul_of_nonneg_right (PadicInt.norm_le_one _) (norm_nonneg _)
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
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ 1 * ‖h‖ = ‖z - soln‖
simp
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖z - soln‖ < ‖Polynomial.eval soln (↑Polynomial.derivative F)‖
rw [soln_deriv_norm]
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
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
apply soln_dist
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
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
this : h = 0
⊢ z - soln = 0
rw [← this]