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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
⊢ Tendsto
    (fun (i : ℕ) ↦
      norm (E := ℤ_[p])
        (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
    atTop
    (𝓝
      (norm (E := ℤ_[p])
        (((Polynomial.aeval ncs.lim : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])))

Tactic:
Tendsto.comp (continuous_iff_continuousAt.1 continuous_norm _) ?_

Premises used: Iff.mp, Filter.Tendsto.comp, continuous_norm, continuous_iff_continuousAt
-- 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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
refine :
  Tendsto (β := ℤ_[p])
    (fun (i : ℕ) ↦
      (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p]))
    atTop
    (𝓝
        (((Polynomial.aeval ncs.lim : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
      Filter ℤ_[p])
⊢ Tendsto
    (fun (i : ℕ) ↦
      norm (E := ℤ_[p])
        (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
    atTop
    (𝓝
      (norm (E := ℤ_[p])
        (((Polynomial.aeval ncs.lim : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])))

Tactic:
refine Tendsto.comp (continuous_iff_continuousAt.1 continuous_norm _) ?_

Premises used: Iff.mp, Filter.Tendsto.comp, continuous_norm, continuous_iff_continuousAt
-- 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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
rw :
  Tendsto
    (fun (i : ℕ) ↦
      ((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F))
    atTop
    (𝓝
      (Polynomial.eval ncs.lim
        (Polynomial.map (algebraMap R ℤ_[p]) ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F))))
⊢ Tendsto (β := ℤ_[p])
    (fun (i : ℕ) ↦
      (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p]))
    atTop
    (𝓝
        (((Polynomial.aeval ncs.lim : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
      Filter ℤ_[p])

Tactic:
rw [← Polynomial.eval_map_algebraMap]

Premises used: Polynomial.eval_map_algebraMap
-- 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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
⊢ Tendsto
    (fun (i : ℕ) ↦
      ((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F))
    atTop
    (𝓝
      (Polynomial.eval ncs.lim
        (Polynomial.map (algebraMap R ℤ_[p]) ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F))))

Tactic:
(comp_tendsto_lim ncs).congr ?_

Premises used: _private.0.comp_tendsto_lim, Filter.Tendsto.congr
-- 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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
refine :
  ∀ (x : ℕ),
    Polynomial.eval ((↑ncs : ℕ → ℤ_[p]) x)
        (Polynomial.map (algebraMap R ℤ_[p]) ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) =
      ((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) x) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)
⊢ Tendsto
    (fun (i : ℕ) ↦
      ((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F))
    atTop
    (𝓝
      (Polynomial.eval ncs.lim
        (Polynomial.map (algebraMap R ℤ_[p]) ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F))))

Tactic:
refine (comp_tendsto_lim ncs).congr ?_

Premises used: _private.0.comp_tendsto_lim, Filter.Tendsto.congr
-- 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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
⊢ ∀ (x : ℕ),
    Polynomial.eval ((↑ncs : ℕ → ℤ_[p]) x)
        (Polynomial.map (algebraMap R ℤ_[p]) ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) =
      ((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) x) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)

Tactic:
simp
-- 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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ),
    norm (E := ℤ_[p])
        (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) 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])
⊢ Tendsto
    (fun (x : ℕ) ↦
      norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
    atTop
    (𝓝
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])))

Tactic:
@tendsto_const_nhds ℝ _ ℕ _ _

Premises used: tendsto_const_nhds
-- 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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
a : ℤ_[p]
ncs_der_val h :
  ∀ (x : ℕ),
    norm (E := ℤ_[p])
        (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) x) : 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])
⊢ Tendsto
    (fun (i : ℕ) ↦
      norm (E := ℤ_[p])
        (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
    atTop
    (𝓝
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])))

Tactic:
convert! @tendsto_const_nhds ℝ _ ℕ _ _

Premises used: tendsto_const_nhds
-- 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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ),
    norm (E := ℤ_[p])
        (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) 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])
x : ℕ
h h₁ :
  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 a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
⊢ norm (E := ℤ_[p])
      (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) x) : 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:
rw [ncs_der_val]
-- 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]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ),
    norm (E := ℤ_[p])
        (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) 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])
⊢ norm (E := ℤ_[p])
      (((Polynomial.aeval ncs.lim : 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:
tendsto_nhds_unique ncs_tendsto_lim (ncs_tendsto_const ncs_der_val)

Premises used: _private.0.ncs_tendsto_const, _private.0.ncs_tendsto_lim, tendsto_nhds_unique
-- 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]
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 (e : ℕ) ↦
      ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
          (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) e) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F :
            ℤ_[p])
          (0 : ℤ_[p])‖)
    atTop (𝓝 0)

Tactic:
simpa using hnorm
-- 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]
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)
⊢ Eq (α := ℤ_[p]) (((Polynomial.aeval ncs.lim : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])

Tactic:
tendsto_nhds_unique ?_ (tendsto_zero_of_norm_tendsto_zero hnorm)

Premises used: _private.0.tendsto_zero_of_norm_tendsto_zero, tendsto_nhds_unique
-- 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]
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)
refine :
  Tendsto (β := ℤ_[p])
    (fun (i : ℕ) ↦
      (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]))
    atTop (𝓝 (((Polynomial.aeval ncs.lim : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : Filter ℤ_[p])
⊢ Eq (α := ℤ_[p]) (((Polynomial.aeval ncs.lim : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])

Tactic:
refine tendsto_nhds_unique ?_ (tendsto_zero_of_norm_tendsto_zero hnorm)

Premises used: _private.0.tendsto_zero_of_norm_tendsto_zero, tendsto_nhds_unique
-- 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]
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)
rw :
  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)))
⊢ Tendsto (β := ℤ_[p])
    (fun (i : ℕ) ↦
      (((Polynomial.aeval ((↑ncs : ℕ → ℤ_[p]) i) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]))
    atTop (𝓝 (((Polynomial.aeval ncs.lim : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : Filter ℤ_[p])

Tactic:
rw [← Polynomial.eval_map_algebraMap]

Premises used: Polynomial.eval_map_algebraMap
-- 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]
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)))

Tactic:
(comp_tendsto_lim ncs).congr ?_

Premises used: _private.0.comp_tendsto_lim, Filter.Tendsto.congr
-- 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]
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)
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
⊢ 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)))

Tactic:
refine (comp_tendsto_lim ncs).congr ?_

Premises used: _private.0.comp_tendsto_lim, Filter.Tendsto.congr
-- 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]
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)
⊢ ∀ (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:
simp
-- 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]
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
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
⊢ z' = a

Tactic:
let ⟨q, hq⟩ := (F.map (algebraMap R ℤ_[p])).binomExpansion a h
-- 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]
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
⊢ ((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

Premises used: Polynomial.eval_map_algebraMap, Polynomial.derivative_map
-- 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]
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
⊢ Eq (α := ℤ_[p])
    (((Polynomial.aeval (a + (z' - a)) : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) (0 : ℤ_[p])

Tactic:
simp [hz']
-- 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]
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
⊢ 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:
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']

Premises used: HAdd.hAdd, 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]
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

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']