awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : Algebra R ℚ
inst_2 : IsIntegralClosure R ℤ ℚ
inst_3 : IsDedekindDomain R
inst_4 : IsFractionRing R ℚ
v : HeightOneSpectrum R
y : ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]
hy :
  y ∈
    (↑(subring (↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)) :
      Set ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
hx :
  (adicCompletionIntegers.padicIntEquiv v :
        (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
          ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      x =
    Subtype.mk (p :=
      fun
        (x :
          ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) ↦
      ‖x‖ ≤ 1) y hy
rw :
  (↑((adicCompletionIntegers.padicIntEquiv v :
            (a : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) →
              ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
          x) :
      ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) =
    y
⊢ (padicEquiv v :
        (a : HeightOneSpectrum.adicCompletion ℚ v) →
          ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)])
      (↑x : HeightOneSpectrum.adicCompletion ℚ v) =
    y
have rw₁ : (↑(Subtype.mk (p :=
        fun
          (x :
            ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes) v) :
                ℕ)]) ↦
        ‖x‖ ≤ 1) y hy) :
    ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes) v) : ℕ)]) =
  y
Tactic: rw [← adicCompletionIntegers.coe_padicIntEquiv_apply, hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
inst_4 : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ℤ_[(↑p : ℕ)]
⊢ Eq (α :=
    HeightOneSpectrum.adicCompletion.{u_2, 0} (R := R) ℚ
      ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))
    ((↑((adicCompletionIntegersEquiv R p :
              (a : ℤ_[(↑p : ℕ)]) →
                ↥(HeightOneSpectrum.adicCompletionIntegers ℚ
                    ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)))
            x) :
        HeightOneSpectrum.adicCompletion.{u_2, 0} (R := R) ℚ
          ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
      HeightOneSpectrum.adicCompletion.{u_2, 0} (R := R) ℚ
        ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))
    ((adicCompletionEquiv R p :
          (a : ℚ_[(↑p : ℕ)]) →
            HeightOneSpectrum.adicCompletion ℚ ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p))
        (↑x : ℚ_[(↑p : ℕ)]) :
      HeightOneSpectrum.adicCompletion.{u_2, 0} (R := R) ℚ
        ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))
have simp : HEq (α :=
  ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
          ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
      ℕ)])
  (↑(cast sorry x) :
    ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
            ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)])
  (↑x : ℚ_[(↑p : ℕ)])
Tactic: simp only [adicCompletionIntegersEquiv, ContinuousAlgEquiv.trans_apply,
    adicCompletionIntegers.coe_padicIntEquiv_symm_apply,
    adicCompletionEquiv, ContinuousAlgEquiv.trans_apply, ContinuousAlgEquiv.cast_apply,
    EmbeddingLike.apply_eq_iff_eq, Equiv.cast_apply, eq_cast_iff_heq]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
inst_4 : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ℤ_[(↑p : ℕ)]
⊢ ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)] =
    ℚ_[(↑p : ℕ)]
have rw : ℚ_[(↑p : ℕ)] = ℚ_[(↑p : ℕ)]
Tactic: rw [primesEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
inst_4 : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ℤ_[(↑p : ℕ)]
⊢ HEq (α :=
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)] →
      Prop)
    fun
      (x :
        ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
            ℕ)]) ↦
    ‖x‖ ≤ 1 (β := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦ ‖x‖ ≤ 1
have rw : HEq (α := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦ ‖x‖ ≤ 1 (β := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦
  ‖x‖ ≤ 1
Tactic: rw [primesEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
inst_4 : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ℤ_[(↑p : ℕ)]
⊢ HEq (α :=
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)])
    (↑(cast ⋯ x) :
      ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
              ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)])
    (↑x : ℚ_[(↑p : ℕ)])
have rw : HEq (α :=
  { x :
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)] //
    ‖x‖ ≤ 1 })
  (cast sorry x :
    ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)])
  x
Tactic: rw [← Subtype.heq_iff_coe_heq (by rw [primesEquiv.apply_symm_apply])
    (by rw [primesEquiv.apply_symm_apply])]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
inst_4 : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))
⊢ Eq (α := ℚ_[(↑p : ℕ)])
    ((↑((ContinuousAlgEquiv.symm (adicCompletionIntegersEquiv R p) :
              (a :
                  ↥(HeightOneSpectrum.adicCompletionIntegers ℚ
                      ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p))) →
                ℤ_[(↑p : ℕ)])
            x) :
        ℚ_[(↑p : ℕ)]) :
      ℚ_[(↑p : ℕ)])
    ((ContinuousAlgEquiv.symm (adicCompletionEquiv R p) :
          (a : HeightOneSpectrum.adicCompletion ℚ ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) →
            ℚ_[(↑p : ℕ)])
        (↑x : HeightOneSpectrum.adicCompletion ℚ ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
      ℚ_[(↑p : ℕ)])
have simp : HEq (α := ℚ_[(↑p : ℕ)])
  (↑(cast (α :=
        ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
            ℕ)])
        sorry
        ((adicCompletionIntegers.padicIntEquiv ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p) :
              (a :
                  ↥(HeightOneSpectrum.adicCompletionIntegers ℚ
                      ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p))) →
                ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
                        ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
                    ℕ)])
            x :
          ℤ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                  ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
              ℕ)])) :
    ℚ_[(↑p : ℕ)])
  (β :=
  ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
          ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
      ℕ)])
  (↑((adicCompletionIntegers.padicIntEquiv ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p) :
          (a :
              ↥(HeightOneSpectrum.adicCompletionIntegers ℚ
                  ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p))) →
            ℤ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
                    ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
                ℕ)])
        x) :
    ℚ_[(↑((primesEquiv : (a : HeightOneSpectrum R) → Nat.Primes)
            ((primesEquiv.symm : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)])
Tactic: simp only [adicCompletionIntegersEquiv, ContinuousAlgEquiv.symm_trans_apply,
    ContinuousAlgEquiv.symm_symm, adicCompletionEquiv, Equiv.cast_apply, eq_cast_iff_heq,
    ← adicCompletionIntegers.coe_padicIntEquiv_apply, ContinuousAlgEquiv.cast_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
inst_4 : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))
⊢ ℚ_[(↑p : ℕ)] =
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
            ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
        ℕ)]
have rw : ℚ_[(↑p : ℕ)] = ℚ_[(↑p : ℕ)]
Tactic: rw [primesEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.Padics.HeightOneSpectrum (goal)
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDedekindDomain R
inst_2 : Algebra R ℚ
inst_3 : IsFractionRing R ℚ
inst_4 : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p))
⊢ HEq (α := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦ ‖x‖ ≤ 1 (β :=
    ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
              ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
          ℕ)] →
      Prop)
    fun
      (x :
        ℚ_[(↑(((primesEquiv : HeightOneSpectrum R ≃ Nat.Primes) : (a : HeightOneSpectrum R) → Nat.Primes)
                ((Equiv.symm primesEquiv : (a : Nat.Primes) → HeightOneSpectrum R) p)) :
            ℕ)]) ↦
    ‖x‖ ≤ 1
have rw : HEq (α := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦ ‖x‖ ≤ 1 (β := ℚ_[(↑p : ℕ)] → Prop) fun (x : ℚ_[(↑p : ℕ)]) ↦
  ‖x‖ ≤ 1
Tactic: rw [primesEquiv.apply_symm_apply]
-- 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
x y : ℤ_[p]
⊢ ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ ≤
    ‖x - y‖
have let : ∀ (z : ℤ_[p])
  (hz :
    Polynomial.eval x (Polynomial.map (algebraMap R ℤ_[p]) F) -
        Polynomial.eval y (Polynomial.map (algebraMap R ℤ_[p]) F) =
      z * (x - y)),
  ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ ≤
    ‖x - y‖
Tactic: let ⟨z, hz⟩ := (F.map (algebraMap R ℤ_[p])).evalSubFactor x y
-- 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
x y z : ℤ_[p]
hz :
  Polynomial.eval x (Polynomial.map (algebraMap R ℤ_[p]) F) -
      Polynomial.eval y (Polynomial.map (algebraMap R ℤ_[p]) F) =
    z * (x - y)
⊢ ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ ≤
    ‖x - y‖
have hz₁ : HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
    (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
  z * (x - y)
Tactic: simp only [Polynomial.eval_map_algebraMap] at hz
Cleared hypotheses: 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
x y z : ℤ_[p]
hz :
  HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    z * (x - y)
⊢ ‖z‖ * ‖x - y‖ ≤ 1 * ‖x - y‖
have hbc : ‖z‖ ≤ 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
x y z : ℤ_[p]
hz :
  HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    z * (x - y)
⊢ ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ ≤
    ‖x - y‖
have x₁ : ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ =
  ‖z‖ * ‖x - y‖
Tactic: calc
    ‖F.aeval x - F.aeval y‖ = ‖z‖ * ‖x - y‖ := by simp [hz]
    _ ≤ 1 * ‖x - y‖ := by gcongr; apply PadicInt.norm_le_one
    _ = ‖x - y‖ := by simp
-- 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
x y z : ℤ_[p]
hz :
  HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    z * (x - y)
x₁ :
  ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ =
    ‖z‖ * ‖x - y‖
⊢ ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ ≤
    ‖x - y‖
have x₂ : ‖z‖ * ‖x - y‖ ≤ 1 * ‖x - y‖
Tactic: calc
    ‖F.aeval x - F.aeval y‖ = ‖z‖ * ‖x - y‖ := by simp [hz]
    _ ≤ 1 * ‖x - y‖ := by gcongr; apply PadicInt.norm_le_one
    _ = ‖x - y‖ := by simp
-- 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
x y z : ℤ_[p]
hz :
  HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
      (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
      (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) =
    z * (x - y)
x₁ :
  ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ =
    ‖z‖ * ‖x - y‖
x₂ : ‖z‖ * ‖x - y‖ ≤ 1 * ‖x - y‖
⊢ ‖HSub.hSub (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval x : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
        (((Polynomial.aeval y : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])‖ ≤
    ‖x - y‖
have x₃ : 1 * ‖x - y‖ = ‖x - y‖
Tactic: calc
    ‖F.aeval x - F.aeval y‖ = ‖z‖ * ‖x - y‖ := by simp [hz]
    _ ≤ 1 * ‖x - y‖ := by gcongr; apply PadicInt.norm_le_one
    _ = ‖x - y‖ := by simp
-- 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
⊢ 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])))
have 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])
Tactic: refine Tendsto.comp (continuous_iff_continuousAt.1 continuous_norm _) ?_
-- 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
⊢ 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])
have 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))))
Tactic: rw [← Polynomial.eval_map_algebraMap]
-- 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
⊢ 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))))
have 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)
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]
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 : ℕ
⊢ 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])
have 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])
Tactic: rw [ncs_der_val]
-- 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)
⊢ Eq (α := ℤ_[p]) (((Polynomial.aeval ncs.lim : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p])
    (0 : ℤ_[p])
have 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])
Tactic: refine tendsto_nhds_unique ?_ (tendsto_zero_of_norm_tendsto_zero 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]
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 (β := ℤ_[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])
have 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)))
Tactic: rw [← Polynomial.eval_map_algebraMap]