-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem newton_seq_succ_dist_weak (n : ℕ) :
    ‖newton_seq (n + 2) - newton_seq (n + 1)‖ < ‖F.eval a‖ / ‖F.derivative.eval a‖ :=
  have : 2 ≤ 2 ^ (n + 1)

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
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ 1 < 2

Tactic:
norm_num

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
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (Polynomial.derivative F)‖ * ‖Polynomial.eval a F‖ /
      (‖↑(Polynomial.eval a (Polynomial.derivative F))‖ * ‖↑(Polynomial.eval a (Polynomial.derivative F))‖) =
    ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
apply mul_div_mul_left

Result:
case hc
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
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (Polynomial.derivative F)‖ ≠ 0

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
n : ℕ
⊢ 2 ≤ 2 ^ (n + 1)

Tactic:
have := pow_right_mono₀ (by norm_num : 1 ≤ 2) (Nat.le_add_left _ _ : 1 ≤ n + 1)

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
n : ℕ
this : (fun x => 2 ^ x) 1 ≤ (fun x => 2 ^ x) (n + 1)
⊢ 2 ≤ 2 ^ (n + 1)

Proof state:
case hc
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
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (Polynomial.derivative F)‖ ≠ 0

Tactic:
apply deriv_norm_ne_zero

Result:
case hc.hnorm
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
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2

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
n : ℕ
⊢ 1 ≤ 2

Tactic:
norm_num

Result:
no goals

Proof state:
case hc.hnorm
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
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2

Tactic:
assumption

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
n : ℕ
this : (fun x => 2 ^ x) 1 ≤ (fun x => 2 ^ x) (n + 1)
⊢ 2 ≤ 2 ^ (n + 1)

Tactic:
simpa using 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
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (Polynomial.derivative F)‖ * T_gen p F a ^ 1 =
    ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
rw [T_gen, sq, pow_one, norm_div, ← mul_div_assoc, PadicInt.padic_norm_e_of_padicInt,
  PadicInt.coe_mul, padicNormE.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
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (Polynomial.derivative F)‖ * ‖Polynomial.eval a F‖ /
      (‖↑(Polynomial.eval a (Polynomial.derivative F))‖ * ‖↑(Polynomial.eval a (Polynomial.derivative F))‖) =
    ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖