awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen.{u_1} (R := R) (F := F) (a := a) n z
q : ℤ_[p]
heq : ((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F = q * HPow.hPow (β := ℕ) z1 2
h1 :
  ‖HDiv.hDiv (α := ℚ_[p]) (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p])‖ ≤
    1
hzeq :
  z1 =
    Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
      (HDiv.hDiv (α := ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p]))
      h1
⊢ norm (E := ℤ_[p]) (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) ≤
    HPow.hPow (β := ℕ)
        (norm (E := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p]))
        2 *
      T_gen p F a ^ HPow.hPow (α := ℕ) 2 n

Tactic:
exact hz.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen.{u_1} (R := R) (F := F) (a := a) n z
q : ℤ_[p]
heq : ((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F = q * HPow.hPow (β := ℕ) z1 2
h1 :
  ‖HDiv.hDiv (α := ℚ_[p]) (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p])‖ ≤
    1
hzeq :
  z1 =
    Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
      (HDiv.hDiv (α := ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p]))
      h1
⊢ HPow.hPow (β := ℕ)
        (HPow.hPow (β := ℕ)
            (norm (E := ℤ_[p])
              (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                  ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
                ℤ_[p]))
            2 *
          T_gen p F a ^ HPow.hPow (α := ℕ) 2 n)
        2 /
      HPow.hPow (β := ℕ)
        (norm (E := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p]))
        2 =
    HPow.hPow (β := ℕ)
          (HPow.hPow (β := ℕ)
            (norm (E := ℤ_[p])
              (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                  ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
                ℤ_[p]))
            2)
          2 *
        HPow.hPow (β := ℕ) (T_gen p F a ^ HPow.hPow (α := ℕ) 2 n) 2 /
      HPow.hPow (β := ℕ)
        (norm (E := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p]))
        2

Tactic:
simp only [mul_pow]

Premises used: mul_pow
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen.{u_1} (R := R) (F := F) (a := a) n z
q : ℤ_[p]
heq : ((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F = q * HPow.hPow (β := ℕ) z1 2
h1 :
  ‖HDiv.hDiv (α := ℚ_[p]) (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p])‖ ≤
    1
hzeq :
  z1 =
    Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
      (HDiv.hDiv (α := ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p]))
      h1
⊢ HPow.hPow (β := ℕ)
          (HPow.hPow (β := ℕ)
            (norm (E := ℤ_[p])
              (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                  ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
                ℤ_[p]))
            2)
          2 *
        HPow.hPow (β := ℕ) (T_gen p F a ^ HPow.hPow (α := ℕ) 2 n) 2 /
      HPow.hPow (β := ℕ)
        (norm (E := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p]))
        2 =
    HPow.hPow (β := ℕ)
        (norm (E := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p]))
        2 *
      HPow.hPow (β := ℕ) (T_gen p F a ^ HPow.hPow (α := ℕ) 2 n) 2

Tactic:
div_sq_cancel _ _

Premises used: div_sq_cancel
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
n : ℕ
z : ℤ_[p]
hz : ih_gen.{u_1} (R := R) (F := F) (a := a) n z
h1 :
  ‖HDiv.hDiv (α := ℚ_[p]) (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p])‖ ≤
    1
z1 : ℤ_[p] :=
  Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
    (HDiv.hDiv (α := ℚ_[p])
      (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
      (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
        ℚ_[p]))
    h1
z' : ℤ_[p] := z - z1
⊢ ‖z1‖ =
    norm (E := ℤ_[p]) (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) /
      norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])

Tactic:
simp [z1, hz.1]

Premises used: And.left
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
n : ℕ
z : ℤ_[p]
hz : ih_gen.{u_1} (R := R) (F := F) (a := a) n z
h1 :
  ‖HDiv.hDiv (α := ℚ_[p]) (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p])‖ ≤
    1
z1 : ℤ_[p] :=
  Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
    (HDiv.hDiv (α := ℚ_[p])
      (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
      (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
        ℚ_[p]))
    h1
z' : ℤ_[p] := z - z1
hdist :
  ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])‖ <
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
⊢ ‖HAdd.hAdd (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (-((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])‖ <
    norm (E := ℤ_[p])
      (-((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])

Tactic:
rw [sub_eq_add_neg, ← hz.1, ← norm_neg (F.derivative.aeval z)] at hdist

Premises used: Polynomial.derivative, sub_eq_add_neg, And.left, norm_neg, Polynomial.aeval, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
n : ℕ
z : ℤ_[p]
hz : ih_gen.{u_1} (R := R) (F := F) (a := a) n z
h1 :
  ‖HDiv.hDiv (α := ℚ_[p]) (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p])‖ ≤
    1
z1 : ℤ_[p] :=
  Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
    (HDiv.hDiv (α := ℚ_[p])
      (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
      (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
        ℚ_[p]))
    h1
z' : ℤ_[p] := z - z1
hdist :
  ‖HAdd.hAdd (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (-((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])‖ <
    norm (E := ℤ_[p])
      (-((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
⊢ norm (E := ℤ_[p])
      (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p]) =
    norm (E := ℤ_[p])
      (-((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])

Tactic:
have := PadicInt.norm_eq_of_norm_add_lt_right hdist
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
n : ℕ
⊢ norm (E := ℤ_[p])
      (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p]) =
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])

Tactic:
(newton_seq_aux hnorm n).2.1

Premises used: _private.0.newton_seq_aux, And.left, _private.0.newton_seq_gen, Subtype.property
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
n : ℕ
⊢ norm (E := ℤ_[p])
      (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) ≤
    HPow.hPow (β := ℕ)
        (norm (E := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p]))
        2 *
      T_gen p F a ^ HPow.hPow (α := ℕ) 2 n

Tactic:
(newton_seq_aux hnorm n).2.2

Premises used: _private.0.newton_seq_aux, And.right, _private.0.newton_seq_gen, Subtype.property
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
n : ℕ
rw :
  ‖(↑(Subtype.mk (p := fun (z' : ℤ_[p]) ↦ ih_gen.{u_1} (R := R) (F := F) (a := a) (n + 1) z')
              ((↑(newton_seq_aux hnorm n) : ℤ_[p]) -
                Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
                  (HDiv.hDiv (α := ℚ_[p])
                    (↑(((Polynomial.aeval (↑(newton_seq_aux hnorm n) : ℤ_[p]) : Polynomial R →ₐ[R] ℤ_[p]) :
                            (a : Polynomial R) → ℤ_[p])
                          F) :
                      ℚ_[p])
                    (↑(((Polynomial.aeval (↑(newton_seq_aux hnorm n) : ℤ_[p]) : Polynomial R →ₐ[R] ℤ_[p]) :
                            (a : Polynomial R) → ℤ_[p])
                          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
                      ℚ_[p]))
                  ⋯)
              ⋯) :
          ℤ_[p]) -
        (↑(newton_seq_aux hnorm n) : ℤ_[p])‖ =
    norm (E := ℤ_[p])
        (((Polynomial.aeval (↑(newton_seq_aux hnorm n) : ℤ_[p]) : Polynomial R →ₐ[R] ℤ_[p]) :
              (a : Polynomial R) → ℤ_[p])
            F :
          ℤ_[p]) /
      norm (E := ℤ_[p])
        (((Polynomial.aeval (↑(newton_seq_aux hnorm n) : ℤ_[p]) : Polynomial R →ₐ[R] ℤ_[p]) :
              (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
⊢ ‖newton_seq (n + 1) - newton_seq n‖ =
    norm (E := ℤ_[p])
        (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) /
      norm (E := ℤ_[p])
        (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])

Tactic:
rw [newton_seq_gen, newton_seq_gen, newton_seq_aux, ih_n]

Premises used: _private.0.newton_seq_aux, _private.0.ih_n, _private.0.newton_seq_gen
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
n : ℕ
⊢ ‖(↑(Subtype.mk (p := fun (z' : ℤ_[p]) ↦ ih_gen.{u_1} (R := R) (F := F) (a := a) (n + 1) z')
              ((↑(newton_seq_aux hnorm n) : ℤ_[p]) -
                Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
                  (HDiv.hDiv (α := ℚ_[p])
                    (↑(((Polynomial.aeval (↑(newton_seq_aux hnorm n) : ℤ_[p]) : Polynomial R →ₐ[R] ℤ_[p]) :
                            (a : Polynomial R) → ℤ_[p])
                          F) :
                      ℚ_[p])
                    (↑(((Polynomial.aeval (↑(newton_seq_aux hnorm n) : ℤ_[p]) : Polynomial R →ₐ[R] ℤ_[p]) :
                            (a : Polynomial R) → ℤ_[p])
                          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
                      ℚ_[p]))
                  ⋯)
              ⋯) :
          ℤ_[p]) -
        (↑(newton_seq_aux hnorm n) : ℤ_[p])‖ =
    norm (E := ℤ_[p])
        (((Polynomial.aeval (↑(newton_seq_aux hnorm n) : ℤ_[p]) : Polynomial R →ₐ[R] ℤ_[p]) :
              (a : Polynomial R) → ℤ_[p])
            F :
          ℤ_[p]) /
      norm (E := ℤ_[p])
        (((Polynomial.aeval (↑(newton_seq_aux hnorm n) : ℤ_[p]) : Polynomial R →ₐ[R] ℤ_[p]) :
              (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])

Tactic:
simp [sub_eq_add_neg, add_comm]

Premises used: sub_eq_add_neg, add_comm
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
n : ℕ
rw rw₁ :
  norm (E := ℤ_[p])
        (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) /
      norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]) =
    norm (E := ℤ_[p])
        (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) /
      norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
⊢ norm (E := ℤ_[p])
        (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) /
      norm (E := ℤ_[p])
        (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]) =
    norm (E := ℤ_[p])
        (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) /
      norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])

Tactic:
rw [newton_seq_deriv_norm]

Premises used: _private.0.newton_seq_deriv_norm
-- Module: Mathlib.NumberTheory.Padics.Hensel
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
n : ℕ
hab :
  norm (E := ℤ_[p])
      (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) ≤
    HPow.hPow (β := ℕ)
        (norm (E := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p]))
        2 *
      T_gen p F a ^ HPow.hPow (α := ℕ) 2 n
⊢ norm (E := ℤ_[p])
        (((Polynomial.aeval (newton_seq n) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) /
      norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]) ≤
    HPow.hPow (β := ℕ)
          (norm (E := ℤ_[p])
            (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
              ℤ_[p]))
          2 *
        T_gen p F a ^ HPow.hPow (α := ℕ) 2 n /
      norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])

Tactic:
gcongr