awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (goal)
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]
hz' : z' = z - z1
n : ℕ
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
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])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]) =
      0
have rw : ¬norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p]) =
    0
Tactic: rw [hz.1]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (hypothesis)
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]
hz' : z' = z - z1
n : ℕ
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
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
⊢ { q : ℤ_[p] //
    ((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F = q * HPow.hPow (β := ℕ) z1 2 }
have hdzne : Ne (α := ℤ_[p])
  (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
      ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
    ℤ_[p])
  (0 : ℤ_[p])
Tactic: have hdzne : F.derivative.aeval z ≠ 0 :=
    mt norm_eq_zero.2 (by rw [hz.1]; apply deriv_norm_ne_zero; assumption)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (hypothesis)
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]
hz' : z' = z - z1
n : ℕ
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
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
hdzne :
  Ne (α := ℤ_[p])
    (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
      ℤ_[p])
    (0 : ℤ_[p])
⊢ { q : ℤ_[p] //
    ((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F = q * HPow.hPow (β := ℕ) z1 2 }
have hdzne' : Ne (α := ℚ_[p])
  (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
    ℚ_[p])
  0
Tactic: have hdzne' : (↑(F.derivative.aeval z) : ℚ_[p]) ≠ 0 := fun h => hdzne (Subtype.ext_iff.2 h)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (goal)
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]
hz' : z' = z - z1
n : ℕ
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
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
hdzne :
  Ne (α := ℤ_[p])
    (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
      ℤ_[p])
    (0 : ℤ_[p])
hdzne' :
  Ne (α := ℚ_[p])
    (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
      ℚ_[p])
    0
⊢ { q : ℤ_[p] //
    ((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F = q * HPow.hPow (β := ℕ) z1 2 }
have obtain : (q : ℤ_[p]) →
  (hq :
      Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
        Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
            Polynomial.eval z
                ((Polynomial.derivative : (a : Polynomial ℤ_[p]) → Polynomial ℤ_[p])
                  (Polynomial.map (algebraMap R ℤ_[p]) F)) *
              -z1 +
          q * HPow.hPow (β := ℕ) (-z1) 2) →
    { q : ℤ_[p] //
      ((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F = q * HPow.hPow (β := ℕ) z1 2 }
Tactic: obtain ⟨q, hq⟩ := (F.map (algebraMap R ℤ_[p])).binomExpansion z (-z1)
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (hypothesis)
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]
hz' : z' = z - z1
n : ℕ
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
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
hdzne :
  Ne (α := ℤ_[p])
    (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
      ℤ_[p])
    (0 : ℤ_[p])
hdzne' :
  Ne (α := ℚ_[p])
    (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
      ℚ_[p])
    0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z
            ((Polynomial.derivative : (a : Polynomial ℤ_[p]) → Polynomial ℤ_[p])
              (Polynomial.map (algebraMap R ℤ_[p]) F)) *
          -z1 +
      q * HPow.hPow (β := ℕ) (-z1) 2
⊢ { q : ℤ_[p] //
    ((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F = q * HPow.hPow (β := ℕ) z1 2 }
have this : ‖(↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
        ℚ_[p]) *
      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
Tactic: have : ‖(↑(F.derivative.aeval z) * (↑(F.aeval z) / ↑(F.derivative.aeval z)) : ℚ_[p])‖ ≤ 1 := by
    simpa using mul_le_one₀ (PadicInt.norm_le_one _) (norm_nonneg _) h1
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (goal)
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
⊢ ‖q‖ * HPow.hPow (β := ℕ) ‖z1‖ 2 ≤ 1 * HPow.hPow (β := ℕ) ‖z1‖ 2
have hbc : ‖q‖ ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (goal)
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 (β := ℕ)
        (norm (E := ℤ_[p]) (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) 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 (β := ℕ)
        (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
have hab : 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: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (goal)
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 (β := ℕ)
        (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 =
    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 + 1)
have rw : 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 *
    T_gen p F a ^ HPow.hPow (α := ℕ) 2 (n + 1)
Tactic: rw [← pow_mul, pow_succ 2]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (goal)
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 + 1)
have by : norm (E := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
  ‖q‖ * HPow.hPow (β := ℕ) ‖z1‖ 2
Tactic: calc
    ‖F.aeval z'‖ = ‖q‖ * ‖z1‖ ^ 2 := by simp [heq]
    _ ≤ 1 * ‖z1‖ ^ 2 := by gcongr; apply PadicInt.norm_le_one
    _ = ‖F.aeval z‖ ^ 2 / ‖F.derivative.aeval a‖ ^ 2 := by simp [hzeq, hz.1, div_pow]
    _ ≤ (‖F.derivative.aeval a‖ ^ 2 * T ^ 2 ^ n) ^ 2 / ‖F.derivative.aeval a‖ ^ 2 := by
      gcongr
      exact hz.2
    _ = (‖F.derivative.aeval a‖ ^ 2) ^ 2 * (T ^ 2 ^ n) ^ 2 / ‖F.derivative.aeval a‖ ^ 2 := by
      simp only [mul_pow]
    _ = ‖F.derivative.aeval a‖ ^ 2 * (T ^ 2 ^ n) ^ 2 := div_sq_cancel _ _
    _ = ‖F.derivative.aeval a‖ ^ 2 * T ^ 2 ^ (n + 1) := by rw [← pow_mul, pow_succ 2]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (goal)
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
by :
  norm (E := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    ‖q‖ * HPow.hPow (β := ℕ) ‖z1‖ 2
⊢ 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 + 1)
have by₁ : ‖q‖ * HPow.hPow (β := ℕ) ‖z1‖ 2 ≤ 1 * HPow.hPow (β := ℕ) ‖z1‖ 2
Tactic: calc
    ‖F.aeval z'‖ = ‖q‖ * ‖z1‖ ^ 2 := by simp [heq]
    _ ≤ 1 * ‖z1‖ ^ 2 := by gcongr; apply PadicInt.norm_le_one
    _ = ‖F.aeval z‖ ^ 2 / ‖F.derivative.aeval a‖ ^ 2 := by simp [hzeq, hz.1, div_pow]
    _ ≤ (‖F.derivative.aeval a‖ ^ 2 * T ^ 2 ^ n) ^ 2 / ‖F.derivative.aeval a‖ ^ 2 := by
      gcongr
      exact hz.2
    _ = (‖F.derivative.aeval a‖ ^ 2) ^ 2 * (T ^ 2 ^ n) ^ 2 / ‖F.derivative.aeval a‖ ^ 2 := by
      simp only [mul_pow]
    _ = ‖F.derivative.aeval a‖ ^ 2 * (T ^ 2 ^ n) ^ 2 := div_sq_cancel _ _
    _ = ‖F.derivative.aeval a‖ ^ 2 * T ^ 2 ^ (n + 1) := by rw [← pow_mul, pow_succ 2]