-- 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
⊢ ‖-q‖ * ‖h‖ ≤ 1 * ‖h‖

Tactic:
exact mul_le_mul_of_nonneg_right (PadicInt.norm_le_one _) (norm_nonneg _)

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
⊢ Polynomial.eval soln (Polynomial.derivative F) = -q * h

Tactic:
simpa using eq_neg_of_add_eq_zero_left 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
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‖

Tactic:
rw [PadicInt.norm_mul]

Result:
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‖

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
⊢ Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2 =
    (Polynomial.eval soln (Polynomial.derivative F) + q * h) * h

Tactic:
rw [sq, right_distrib, mul_assoc]

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
this : h = 0
⊢ z - soln = 0

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
⊢ Polynomial.eval (soln + h) F = Polynomial.eval soln (Polynomial.derivative F) * h + q * h ^ 2

Tactic:
rw [hq, eval_soln, zero_add]

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 soln (Polynomial.derivative F)‖

Tactic:
rw [soln_deriv_norm]

Result:
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)‖