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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
hnorm :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦
      norm (E := ℤ_[p])
        (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]))
    atTop (𝓝 0)
⊢ Tendsto
    (fun (i : ℕ) ↦
      ((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F)
    atTop (𝓝 (Polynomial.eval ncs.lim (Polynomial.map (algebraMap R ℤ_[p]) F)))
have refine : ∀ (x : ℕ),
  Polynomial.eval ((↑ncs : ℕ → ℤ_[p]) x) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    ((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) x) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F
Tactic: refine (comp_tendsto_lim ncs).congr ?_
-- 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]
ha :
  Eq (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) (0 : ℤ_[p])
z' : ℤ_[p]
hz' :
  Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])
hnormz' :
  ‖z' - a‖ <
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
h : ℤ_[p] := z' - a
⊢ z' = a
have let : ∀ (q : ℤ_[p])
  (hq :
    Polynomial.eval (a + h) (Polynomial.map (algebraMap R ℤ_[p]) F) =
      Polynomial.eval a (Polynomial.map (algebraMap R ℤ_[p]) F) +
          Polynomial.eval a
              ((Polynomial.derivative : (a : Polynomial ℤ_[p]) → Polynomial ℤ_[p])
                (Polynomial.map (algebraMap R ℤ_[p]) F)) *
            h +
        q * HPow.hPow (β := ℕ) h 2),
  z' = a
Tactic: let ⟨q, hq⟩ := (F.map (algebraMap R ℤ_[p])).binomExpansion a h
-- 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]
ha :
  Eq (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) (0 : ℤ_[p])
z' : ℤ_[p]
hz' :
  Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])
hnormz' :
  ‖z' - a‖ <
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  Polynomial.eval (a + h) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval a (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval a
            ((Polynomial.derivative : (a : Polynomial ℤ_[p]) → Polynomial ℤ_[p])
              (Polynomial.map (algebraMap R ℤ_[p]) F)) *
          h +
      q * HPow.hPow (β := ℕ) h 2
⊢ z' = a
have hq₁ : ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F =
  HAdd.hAdd (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (HMul.hMul (α := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        h) +
    q * HPow.hPow (β := ℕ) h 2
Tactic: simp only [Polynomial.eval_map_algebraMap, Polynomial.derivative_map] at hq
Cleared hypotheses: hq
-- 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]
ha :
  Eq (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) (0 : ℤ_[p])
z' : ℤ_[p]
hz' :
  Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])
hnormz' :
  ‖z' - a‖ <
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F =
    HAdd.hAdd (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (HMul.hMul (α := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p])
          h) +
      q * HPow.hPow (β := ℕ) h 2
⊢ HAdd.hAdd (α := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (q * h) *
      h =
    ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F
have rw : HAdd.hAdd (α := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
      (q * h) *
    h =
  HAdd.hAdd (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (HMul.hMul (α := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        h) +
    q * HPow.hPow (β := ℕ) h 2
Tactic: rw [hq, ha, zero_add, sq, right_distrib, mul_assoc]
-- 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]
ha :
  Eq (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) (0 : ℤ_[p])
z' : ℤ_[p]
hz' :
  Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])
hnormz' :
  ‖z' - a‖ <
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F =
    HAdd.hAdd (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (HMul.hMul (α := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p])
          h) +
      q * HPow.hPow (β := ℕ) h 2
rw :
  HAdd.hAdd (α := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (q * h) *
      h =
    HAdd.hAdd (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (HMul.hMul (α := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p])
          h) +
      q * HPow.hPow (β := ℕ) h 2
⊢ HAdd.hAdd (α := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (q * h) *
      h =
    ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F
have rw₁ : HAdd.hAdd (α := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
      (q * h) *
    h =
  0 +
      HMul.hMul (α := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        h +
    q * HPow.hPow (β := ℕ) h 2
Tactic: rw [hq, ha, zero_add, sq, right_distrib, mul_assoc]
-- 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]
ha :
  Eq (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) (0 : ℤ_[p])
z' : ℤ_[p]
hz' :
  Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])
hnormz' :
  ‖z' - a‖ <
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F =
    HAdd.hAdd (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (HMul.hMul (α := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p])
          h) +
      q * HPow.hPow (β := ℕ) h 2
⊢ HAdd.hAdd (α := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (q * h) *
      h =
    0
have _ : HAdd.hAdd (α := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
      (q * h) *
    h =
  ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F
Tactic: calc
    _ = F.aeval (a + h) := by rw [hq, ha, zero_add, sq, right_distrib, mul_assoc]
    _ = _ := show F.aeval (a + (z' - a)) = 0 by simp [hz']
-- 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]
ha :
  Eq (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) (0 : ℤ_[p])
z' : ℤ_[p]
hz' :
  Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])
hnormz' :
  ‖z' - a‖ <
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F =
    HAdd.hAdd (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (HMul.hMul (α := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p])
          h) +
      q * HPow.hPow (β := ℕ) h 2
⊢ z' = a
have this : HAdd.hAdd (α := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
      (q * h) *
    h =
  0
Tactic: have : (F.derivative.aeval a + q * h) * h = 0 := by calc
    _ = F.aeval (a + h) := by rw [hq, ha, zero_add, sq, right_distrib, mul_assoc]
    _ = _ := show F.aeval (a + (z' - a)) = 0 by simp [hz']
-- 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]
ha :
  Eq (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) (0 : ℤ_[p])
z' : ℤ_[p]
hz' :
  Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])
hnormz' :
  ‖z' - a‖ <
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F =
    HAdd.hAdd (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (HMul.hMul (α := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p])
          h) +
      q * HPow.hPow (β := ℕ) h 2
this_1 :
  HAdd.hAdd (α := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (q * h) *
      h =
    0
hne : ¬h = 0
this_2 :
  HAdd.hAdd (α := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
      (q * h) =
    0
this :
  ((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
      ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) =
    -q * h
⊢ ‖q‖ * ‖h‖ ≤ 1 * ‖h‖
have hbc : ‖q‖ ≤ 1
Tactic: gcongr
-- 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]
ha :
  Eq (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) (0 : ℤ_[p])
z' : ℤ_[p]
hz' :
  Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])
hnormz' :
  ‖z' - a‖ <
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F =
    HAdd.hAdd (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (HMul.hMul (α := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p])
          h) +
      q * HPow.hPow (β := ℕ) h 2
this :
  HAdd.hAdd (α := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (q * h) *
      h =
    0
⊢ z' = a
have this₁ : h = 0
Tactic: have : h = 0 := by_contra fun hne ↦
    have : F.derivative.aeval a + q * h = 0 :=
      (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne
    have : F.derivative.aeval a = -q * h := by simpa using eq_neg_of_add_eq_zero_left this
    lt_irrefl ‖F.derivative.aeval a‖
      (calc
        ‖F.derivative.aeval a‖ = ‖q‖ * ‖h‖ := by simp [this]
        _ ≤ 1 * ‖h‖ := by gcongr; apply PadicInt.norm_le_one
        _ < ‖F.derivative.aeval a‖ := by simpa)
-- 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]
ha :
  Eq (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) (0 : ℤ_[p])
z' : ℤ_[p]
hz' :
  Eq (α := ℤ_[p]) (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])
hnormz' :
  ‖z' - a‖ <
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  ((Polynomial.aeval (a + h) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F =
    HAdd.hAdd (α := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (HMul.hMul (α := ℤ_[p])
          (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
            ℤ_[p])
          h) +
      q * HPow.hPow (β := ℕ) h 2
this_1 :
  HAdd.hAdd (α := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (q * h) *
      h =
    0
this : h = 0
⊢ z' - a = 0
have rw : z' - a = h
Tactic: rw [← this]
-- 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
⊢ T_gen p F a < 1
have h : 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 <
  1
Tactic: have h := (div_lt_one (deriv_sq_norm_pos hnorm)).2 hnorm
-- 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
n : ℕ
z : ℤ_[p]
hz : ih_gen.{u_1} (R := R) (F := F) (a := a) n z
⊢ 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]) ≤
    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])
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]
hz' : z' = z - z1
hz1 :
  ‖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])
n : ℕ
hz : ih_gen.{u_1} (R := R) (F := F) (a := a) n z
⊢ 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]) ≤
    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])
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