-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem soln_unique (z : ℤ_[p]) (hev : F.eval z = 0)
    (hnlt : ‖z - a‖ < ‖F.derivative.eval a‖) : z = soln :=
  have soln_dist : ‖z - soln‖ < ‖F.derivative.eval a‖ :=
    calc
      ‖z - soln‖ = ‖z - a + (a - soln)‖

Proof state:
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‖

Tactic:
rw [this]

Result:
no goals

Proof state:
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

Tactic:
simp [h, hev]

Result:
no goals

Proof state:
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)‖

Tactic:
rw [sub_add_sub_cancel]

Result:
no goals

Proof state:
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‖

Tactic:
simp [h]

Result:
no goals

Proof state:
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)‖

Tactic:
apply soln_dist

Result:
no goals