[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
have hb' : (0 : ℝ) < ↑(abs b) := Int.cast_pos.mpr (abs_pos.mpr hb)
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
have hbε : 0 < abs b • ε := by
  rw [Algebra.smul_def]
  exact mul_pos hb' hε
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ 0 < |b| • ε
[PROOFSTEP]
rw [Algebra.smul_def]
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ 0 < ↑(algebraMap ℤ ℝ) |b| * ε
[PROOFSTEP]
exact mul_pos hb' hε
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
have hfloor : ∀ i, 0 ≤ floor ((A i % b : ℤ) / abs b • ε : ℝ) := fun _ ↦
  floor_nonneg.mpr (div_nonneg (cast_nonneg.mpr (emod_nonneg _ hb)) hbε.le)
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
refine' ⟨fun i ↦ ⟨natAbs (floor ((A i % b : ℤ) / abs b • ε : ℝ)), _⟩, _⟩
[GOAL]
case refine'_1
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊
[PROOFSTEP]
rw [← ofNat_lt, natAbs_of_nonneg (hfloor i), floor_lt]
[GOAL]
case refine'_1
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ ↑(A i % b) / |b| • ε < ↑↑⌈1 / ε⌉₊
[PROOFSTEP]
apply lt_of_lt_of_le _ (Nat.le_ceil _)
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ ↑(A i % b) / |b| • ε < 1 / ε
[PROOFSTEP]
rw [Algebra.smul_def, eq_intCast, ← div_div, div_lt_div_right hε, div_lt_iff hb', one_mul, cast_lt]
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ A i % b < |b|
[PROOFSTEP]
exact Int.emod_lt _ hb
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
⊢ ∀ (i₀ i₁ : Fin n),
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
        (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁ →
      ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
intro i₀ i₁ hi
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi :
  (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
have hi : (⌊↑(A i₀ % b) / abs b • ε⌋.natAbs : ℤ) = ⌊↑(A i₁ % b) / abs b • ε⌋.natAbs :=
  congr_arg ((↑) : ℕ → ℤ) (Fin.mk_eq_mk.mp hi)
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝ :
  (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁
hi : ↑(natAbs ⌊↑(A i₀ % b) / |b| • ε⌋) = ↑(natAbs ⌊↑(A i₁ % b) / |b| • ε⌋)
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
rw [natAbs_of_nonneg (hfloor i₀), natAbs_of_nonneg (hfloor i₁)] at hi
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝ :
  (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁
hi : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
have hi := abs_sub_lt_one_of_floor_eq_floor hi
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝¹ :
  (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁
hi✝ : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
hi : |↑(A i₀ % b) / |b| • ε - ↑(A i₁ % b) / |b| • ε| < 1
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
rw [abs_sub_comm, ← sub_div, abs_div, abs_of_nonneg hbε.le, div_lt_iff hbε, one_mul] at hi
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝¹ :
  (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁
hi✝ : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
hi : |↑(A i₁ % b) - ↑(A i₀ % b)| < |b| • ε
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
rwa [Int.cast_abs, Int.cast_sub]


[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp2 : p = 2
x✝ : Irreducible ↑p
not_unit✝ : ¬IsUnit ↑p
h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b
⊢ False
[PROOFSTEP]
have := h ⟨1, 1⟩ ⟨1, -1⟩ (hp2.symm ▸ rfl)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp2 : p = 2
x✝ : Irreducible ↑p
not_unit✝ : ¬IsUnit ↑p
h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b
this : IsUnit { re := 1, im := 1 } ∨ IsUnit { re := 1, im := -1 }
⊢ False
[PROOFSTEP]
rw [← norm_eq_one_iff, ← norm_eq_one_iff] at this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp2 : p = 2
x✝ : Irreducible ↑p
not_unit✝ : ¬IsUnit ↑p
h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b
this : Int.natAbs (Zsqrtd.norm { re := 1, im := 1 }) = 1 ∨ Int.natAbs (Zsqrtd.norm { re := 1, im := -1 }) = 1
⊢ False
[PROOFSTEP]
exact absurd this (by decide)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp2 : p = 2
x✝ : Irreducible ↑p
not_unit✝ : ¬IsUnit ↑p
h : ∀ (a b : ℤ[i]), ↑p = a * b → IsUnit a ∨ IsUnit b
this : Int.natAbs (Zsqrtd.norm { re := 1, im := 1 }) = 1 ∨ Int.natAbs (Zsqrtd.norm { re := 1, im := -1 }) = 1
⊢ ¬(Int.natAbs (Zsqrtd.norm { re := 1, im := 1 }) = 1 ∨ Int.natAbs (Zsqrtd.norm { re := 1, im := -1 }) = 1)
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
⊢ False
[PROOFSTEP]
have hp41 : p % 4 = 1 := by
  rw [← Nat.mod_mul_left_mod p 2 2, show 2 * 2 = 4 from rfl] at hp1
  have := Nat.mod_lt p (show 0 < 4 by decide)
  revert this hp3 hp1
  generalize p % 4 = m
  intros;
  interval_cases m <;>
    simp_all
      -- Porting note: was `decide!`
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
⊢ p % 4 = 1
[PROOFSTEP]
rw [← Nat.mod_mul_left_mod p 2 2, show 2 * 2 = 4 from rfl] at hp1
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 4 % 2 = 1
hp3 : p % 4 ≠ 3
⊢ p % 4 = 1
[PROOFSTEP]
have := Nat.mod_lt p (show 0 < 4 by decide)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 4 % 2 = 1
hp3 : p % 4 ≠ 3
⊢ 0 < 4
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 4 % 2 = 1
hp3 : p % 4 ≠ 3
this : p % 4 < 4
⊢ p % 4 = 1
[PROOFSTEP]
revert this hp3 hp1
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
⊢ p % 4 % 2 = 1 → p % 4 ≠ 3 → p % 4 < 4 → p % 4 = 1
[PROOFSTEP]
generalize p % 4 = m
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
⊢ m % 2 = 1 → m ≠ 3 → m < 4 → m = 1
[PROOFSTEP]
intros
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
hp1✝ : m % 2 = 1
hp3✝ : m ≠ 3
this✝ : m < 4
⊢ m = 1
[PROOFSTEP]
interval_cases m
[GOAL]
case «0»
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
hp1✝ : 0 % 2 = 1
hp3✝ : 0 ≠ 3
this✝ : 0 < 4
⊢ 0 = 1
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «1»
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
hp1✝ : 1 % 2 = 1
hp3✝ : 1 ≠ 3
this✝ : 1 < 4
⊢ 1 = 1
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «2»
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
hp1✝ : 2 % 2 = 1
hp3✝ : 2 ≠ 3
this✝ : 2 < 4
⊢ 2 = 1
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
case «3»
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
m : ℕ
hp1✝ : 3 % 2 = 1
hp3✝ : 3 ≠ 3
this✝ : 3 < 4
⊢ 3 = 1
[PROOFSTEP]
simp_all
  -- Porting note: was `decide!`
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
⊢ False
[PROOFSTEP]
let ⟨k, hk⟩ := (ZMod.exists_sq_eq_neg_one_iff (p := p)).2 <| by rw [hp41]; exact by decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
⊢ p % 4 ≠ 3
[PROOFSTEP]
rw [hp41]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
⊢ 1 ≠ 3
[PROOFSTEP]
exact by decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
⊢ 1 ≠ 3
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ZMod p
hk : -1 = k * k
⊢ False
[PROOFSTEP]
obtain ⟨k, k_lt_p, rfl⟩ : ∃ (k' : ℕ) (_ : k' < p), (k' : ZMod p) = k := by
  refine' ⟨k.val, k.val_lt, ZMod.nat_cast_zmod_val k⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ZMod p
hk : -1 = k * k
⊢ ∃ k' x, ↑k' = k
[PROOFSTEP]
refine' ⟨k.val, k.val_lt, ZMod.nat_cast_zmod_val k⟩
[GOAL]
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
⊢ False
[PROOFSTEP]
have hpk : p ∣ k ^ 2 + 1 := by
  rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one, ← hk, add_left_neg]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
⊢ p ∣ k ^ 2 + 1
[PROOFSTEP]
rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one, ← hk, add_left_neg]
[GOAL]
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
⊢ False
[PROOFSTEP]
have hkmul : (k ^ 2 + 1 : ℤ[i]) = ⟨k, 1⟩ * ⟨k, -1⟩ := by simp [sq, Zsqrtd.ext]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
⊢ ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
[PROOFSTEP]
simp [sq, Zsqrtd.ext]
[GOAL]
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
⊢ False
[PROOFSTEP]
have hkltp : 1 + k * k < p * p :=
  calc
    1 + k * k ≤ k + k * k := by
      apply add_le_add_right
      exact (Nat.pos_of_ne_zero fun (hk0 : k = 0) => by clear_aux_decl; simp_all [pow_succ'])
    _ = k * (k + 1) := by simp [add_comm, mul_add]
    _ < p * p := mul_lt_mul k_lt_p k_lt_p (Nat.succ_pos _) (Nat.zero_le _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
⊢ 1 + k * k ≤ k + k * k
[PROOFSTEP]
apply add_le_add_right
[GOAL]
case bc
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
⊢ 1 ≤ k
[PROOFSTEP]
exact (Nat.pos_of_ne_zero fun (hk0 : k = 0) => by clear_aux_decl; simp_all [pow_succ'])
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk0 : k = 0
⊢ False
[PROOFSTEP]
clear_aux_decl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk0 : k = 0
⊢ False
[PROOFSTEP]
simp_all [pow_succ']
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
⊢ k + k * k = k * (k + 1)
[PROOFSTEP]
simp [add_comm, mul_add]
[GOAL]
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
⊢ False
[PROOFSTEP]
have hpk₁ : ¬(p : ℤ[i]) ∣ ⟨k, -1⟩ := fun ⟨x, hx⟩ =>
  lt_irrefl (p * x : ℤ[i]).norm.natAbs <|
    calc
      (norm (p * x : ℤ[i])).natAbs = (Zsqrtd.norm ⟨k, -1⟩).natAbs := by rw [hx]
      _ < (norm (p : ℤ[i])).natAbs := by simpa [add_comm, Zsqrtd.norm] using hkltp
      _ ≤ (norm (p * x : ℤ[i])).natAbs :=
        norm_le_norm_mul_left _ fun hx0 => show (-1 : ℤ) ≠ 0 by decide <| by simpa [hx0] using congr_arg Zsqrtd.im hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
x✝ : ↑p ∣ { re := ↑k, im := -1 }
x : ℤ[i]
hx : { re := ↑k, im := -1 } = ↑p * x
⊢ Int.natAbs (Zsqrtd.norm (↑p * x)) = Int.natAbs (Zsqrtd.norm { re := ↑k, im := -1 })
[PROOFSTEP]
rw [hx]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
x✝ : ↑p ∣ { re := ↑k, im := -1 }
x : ℤ[i]
hx : { re := ↑k, im := -1 } = ↑p * x
⊢ Int.natAbs (Zsqrtd.norm { re := ↑k, im := -1 }) < Int.natAbs (Zsqrtd.norm ↑p)
[PROOFSTEP]
simpa [add_comm, Zsqrtd.norm] using hkltp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
x✝ : ↑p ∣ { re := ↑k, im := -1 }
x : ℤ[i]
hx : { re := ↑k, im := -1 } = ↑p * x
hx0 : x = 0
⊢ -1 ≠ 0
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
x✝ : ↑p ∣ { re := ↑k, im := -1 }
x : ℤ[i]
hx : { re := ↑k, im := -1 } = ↑p * x
hx0 : x = 0
⊢ -1 = 0
[PROOFSTEP]
simpa [hx0] using congr_arg Zsqrtd.im hx
[GOAL]
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
⊢ False
[PROOFSTEP]
have hpk₂ : ¬(p : ℤ[i]) ∣ ⟨k, 1⟩ := fun ⟨x, hx⟩ =>
  lt_irrefl (p * x : ℤ[i]).norm.natAbs <|
    calc
      (norm (p * x : ℤ[i])).natAbs = (Zsqrtd.norm ⟨k, 1⟩).natAbs := by rw [hx]
      _ < (norm (p : ℤ[i])).natAbs := by simpa [add_comm, Zsqrtd.norm] using hkltp
      _ ≤ (norm (p * x : ℤ[i])).natAbs :=
        norm_le_norm_mul_left _ fun hx0 => show (1 : ℤ) ≠ 0 by decide <| by simpa [hx0] using congr_arg Zsqrtd.im hx
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
⊢ Int.natAbs (Zsqrtd.norm (↑p * x)) = Int.natAbs (Zsqrtd.norm { re := ↑k, im := 1 })
[PROOFSTEP]
rw [hx]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
⊢ Int.natAbs (Zsqrtd.norm { re := ↑k, im := 1 }) < Int.natAbs (Zsqrtd.norm ↑p)
[PROOFSTEP]
simpa [add_comm, Zsqrtd.norm] using hkltp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
hx0 : x = 0
⊢ 1 ≠ 0
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
x✝ : ↑p ∣ { re := ↑k, im := 1 }
x : ℤ[i]
hx : { re := ↑k, im := 1 } = ↑p * x
hx0 : x = 0
⊢ 1 = 0
[PROOFSTEP]
simpa [hx0] using congr_arg Zsqrtd.im hx
[GOAL]
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
⊢ False
[PROOFSTEP]
obtain ⟨y, hy⟩ := hpk
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ False
[PROOFSTEP]
have := hpi.2.2 ⟨k, 1⟩ ⟨k, -1⟩ ⟨y, by rw [← hkmul, ← Nat.cast_mul p, ← hy]; simp⟩
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ { re := ↑k, im := 1 } * { re := ↑k, im := -1 } = ↑p * ↑y
[PROOFSTEP]
rw [← hkmul, ← Nat.cast_mul p, ← hy]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ ↑(k ^ 2) + 1 = ↑(k ^ 2 + 1)
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
this : ↑p ∣ { re := ↑k, im := 1 } ∨ ↑p ∣ { re := ↑k, im := -1 }
⊢ False
[PROOFSTEP]
clear_aux_decl
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
hp41 : p % 4 = 1
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hkmul : ↑(k ^ 2) + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
this : ↑p ∣ { re := ↑k, im := 1 } ∨ ↑p ∣ { re := ↑k, im := -1 }
⊢ False
[PROOFSTEP]
tauto
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p
[PROOFSTEP]
erw [← ZMod.nat_cast_mod p 4, hp3]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑3
[PROOFSTEP]
exact by decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑3
[PROOFSTEP]
decide
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
this : ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p
⊢ ↑a ^ 2 + ↑b ^ 2 = ↑(a ^ 2 + b ^ 2)
[PROOFSTEP]
simp


[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖Polynomial.eval x F - Polynomial.eval y F‖ = ‖z‖ * ‖x - y‖
[PROOFSTEP]
simp [hz]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖z‖ * ‖x - y‖ ≤ 1 * ‖x - y‖
[PROOFSTEP]
gcongr
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ ‖z‖ ≤ 1
[PROOFSTEP]
apply PadicInt.norm_le_one
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
x y z : ℤ_[p]
hz : Polynomial.eval x F - Polynomial.eval y F = z * (x - y)
⊢ 1 * ‖x - y‖ = ‖x - y‖
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
⊢ Tendsto (fun i => ‖Polynomial.eval (↑ncs i) (↑Polynomial.derivative F)‖) atTop
    (𝓝 ‖Polynomial.eval a (↑Polynomial.derivative F)‖)
[PROOFSTEP]
convert @tendsto_const_nhds ℝ ℕ _ _ _
[GOAL]
case h.e'_3.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
x✝ : ℕ
⊢ ‖Polynomial.eval (↑ncs x✝) (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [ncs_der_val]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
hnorm : Tendsto (fun i => ‖Polynomial.eval (↑ncs i) F‖) atTop (𝓝 0)
⊢ Tendsto (fun e => ‖Polynomial.eval (↑ncs e) F - 0‖) atTop (𝓝 0)
[PROOFSTEP]
simpa using hnorm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
h : ‖Polynomial.eval a (↑Polynomial.derivative F)‖ = 0
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 = 0
[PROOFSTEP]
simp [*, sq]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ T_gen p F a = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
simp [T_gen, ← PadicInt.norm_def]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ T_gen p F a < 1
[PROOFSTEP]
have h := (div_lt_one (deriv_sq_norm_pos hnorm)).2 hnorm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
h : ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 < 1
⊢ T_gen p F a < 1
[PROOFSTEP]
rw [T_def]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
h : ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 < 1
⊢ ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 < 1
[PROOFSTEP]
exact h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ 0
[PROOFSTEP]
simp [T_def, mul_div_cancel' _ (ne_of_gt (deriv_sq_norm_pos hnorm))]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖↑(Polynomial.eval z F)‖ / ‖↑(Polynomial.eval z (↑Polynomial.derivative F))‖ =
    ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
simp [hz.1]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ≤
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
gcongr
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
apply hz.2
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖z' - z‖ = ‖z1‖
[PROOFSTEP]
simp only [sub_eq_add_neg, add_assoc, hz', add_add_neg_cancel'_right, norm_neg]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ≤
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
gcongr
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
hz1 : ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
n : ℕ
hz : ih_gen n z
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
apply hz.2
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
have hdzne : F.derivative.eval z ≠ 0 := mt norm_eq_zero.2 (by rw [hz.1]; apply deriv_norm_ne_zero; assumption)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ¬‖Polynomial.eval z (↑Polynomial.derivative F)‖ = 0
[PROOFSTEP]
rw [hz.1]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ¬‖Polynomial.eval a (↑Polynomial.derivative F)‖ = 0
[PROOFSTEP]
apply deriv_norm_ne_zero
[GOAL]
case hnorm
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
assumption
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
have hdzne' : (↑(F.derivative.eval z) : ℚ_[p]) ≠ 0 := fun h => hdzne (Subtype.ext_iff_val.2 h)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
obtain ⟨q, hq⟩ := F.binomExpansion z (-z1)
[GOAL]
case mk
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
have : ‖(↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)) : ℚ_[p])‖ ≤ 1 :=
  by
  rw [padicNormE.mul]
  exact mul_le_one (PadicInt.norm_le_one _) (norm_nonneg _) h1
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
⊢ ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
[PROOFSTEP]
rw [padicNormE.mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
⊢ ‖↑(Polynomial.eval z (↑Polynomial.derivative F))‖ *
      ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤
    1
[PROOFSTEP]
exact mul_le_one (PadicInt.norm_le_one _) (norm_nonneg _) h1
[GOAL]
case mk
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
have : F.derivative.eval z * -z1 = -F.eval z := by
  calc
    F.derivative.eval z * -z1 = F.derivative.eval z * -⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩ := by rw [hzeq]
    _ = -(F.derivative.eval z * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) := (mul_neg _ _)
    _ = -⟨F.derivative.eval z * (F.eval z / (F.derivative.eval z : ℤ_[p]) : ℚ_[p]), this⟩ :=
      (Subtype.ext <| by simp only [PadicInt.coe_neg, PadicInt.coe_mul, Subtype.coe_mk])
    _ = -F.eval z := by simp only [mul_div_cancel' _ hdzne', Subtype.coe_eta]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
⊢ Polynomial.eval z (↑Polynomial.derivative F) * -z1 = -Polynomial.eval z F
[PROOFSTEP]
calc
  F.derivative.eval z * -z1 = F.derivative.eval z * -⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩ := by rw [hzeq]
  _ = -(F.derivative.eval z * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) := (mul_neg _ _)
  _ = -⟨F.derivative.eval z * (F.eval z / (F.derivative.eval z : ℤ_[p]) : ℚ_[p]), this⟩ :=
    (Subtype.ext <| by simp only [PadicInt.coe_neg, PadicInt.coe_mul, Subtype.coe_mk])
  _ = -F.eval z := by simp only [mul_div_cancel' _ hdzne', Subtype.coe_eta]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
⊢ Polynomial.eval z (↑Polynomial.derivative F) * -z1 =
    Polynomial.eval z (↑Polynomial.derivative F) *
      -{ val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
[PROOFSTEP]
rw [hzeq]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
⊢ ↑(-(Polynomial.eval z (↑Polynomial.derivative F) *
          { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 })) =
    ↑(-{
          val :=
            ↑(Polynomial.eval z (↑Polynomial.derivative F)) *
              (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))),
          property := this })
[PROOFSTEP]
simp only [PadicInt.coe_neg, PadicInt.coe_mul, Subtype.coe_mk]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
⊢ -{
        val :=
          ↑(Polynomial.eval z (↑Polynomial.derivative F)) *
            (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))),
        property := this } =
    -Polynomial.eval z F
[PROOFSTEP]
simp only [mul_div_cancel' _ hdzne', Subtype.coe_eta]
[GOAL]
case mk
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this✝ :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
this : Polynomial.eval z (↑Polynomial.derivative F) * -z1 = -Polynomial.eval z F
⊢ { q // Polynomial.eval z' F = q * z1 ^ 2 }
[PROOFSTEP]
exact ⟨q, by simpa only [sub_eq_add_neg, this, hz', add_right_neg, neg_sq, zero_add] using hq⟩
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
hdzne : Polynomial.eval z (↑Polynomial.derivative F) ≠ 0
hdzne' : ↑(Polynomial.eval z (↑Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) F = Polynomial.eval z F + Polynomial.eval z (↑Polynomial.derivative F) * -z1 + q * (-z1) ^ 2
this✝ :
  ‖↑(Polynomial.eval z (↑Polynomial.derivative F)) *
        (↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)))‖ ≤
    1
this : Polynomial.eval z (↑Polynomial.derivative F) * -z1 = -Polynomial.eval z F
⊢ Polynomial.eval z' F = q * z1 ^ 2
[PROOFSTEP]
simpa only [sub_eq_add_neg, this, hz', add_right_neg, neg_sq, zero_add] using hq
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval z' F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ (n + 1)
[PROOFSTEP]
calc
  ‖F.eval z'‖ = ‖q‖ * ‖z1‖ ^ 2 := by simp [heq]
  _ ≤ 1 * ‖z1‖ ^ 2 := by gcongr; apply PadicInt.norm_le_one
  _ = ‖F.eval z‖ ^ 2 / ‖F.derivative.eval a‖ ^ 2 := by simp [hzeq, hz.1, div_pow]
  _ ≤ (‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ n) ^ 2 / ‖F.derivative.eval a‖ ^ 2 :=
    by
    gcongr
    exact hz.2
  _ = (‖F.derivative.eval a‖ ^ 2) ^ 2 * (T ^ 2 ^ n) ^ 2 / ‖F.derivative.eval a‖ ^ 2 := by simp only [mul_pow]
  _ = ‖F.derivative.eval a‖ ^ 2 * (T ^ 2 ^ n) ^ 2 := (div_sq_cancel _ _)
  _ = ‖F.derivative.eval a‖ ^ 2 * T ^ 2 ^ (n + 1) := by
    rw [← pow_mul, pow_succ' 2]
      -- Porting note: unsupported option eqn_compiler.zeta
      -- set_option eqn_compiler.zeta true
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval z' F‖ = ‖q‖ * ‖z1‖ ^ 2
[PROOFSTEP]
simp [heq]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖q‖ * ‖z1‖ ^ 2 ≤ 1 * ‖z1‖ ^ 2
[PROOFSTEP]
gcongr
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖q‖ ≤ 1
[PROOFSTEP]
apply PadicInt.norm_le_one
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ 1 * ‖z1‖ ^ 2 = ‖Polynomial.eval z F‖ ^ 2 / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
simp [hzeq, hz.1, div_pow]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval z F‖ ^ 2 / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 ≤
    (‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) ^ 2 /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
gcongr
[GOAL]
case h.hab
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval z F‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
exact hz.2
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ (‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) ^ 2 /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 =
    (‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2) ^ 2 * (T_gen p F a ^ 2 ^ n) ^ 2 /
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
simp only [mul_pow]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : Polynomial.eval z' F = q * z1 ^ 2
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * (T_gen p F a ^ 2 ^ n) ^ 2 =
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ (n + 1)
[PROOFSTEP]
rw [← pow_mul, pow_succ' 2]
  -- Porting note: unsupported option eqn_compiler.zeta
  -- set_option eqn_compiler.zeta true
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
z' : ℤ_[p] := z - z1
⊢ ‖z1‖ = ‖Polynomial.eval z F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
simp [hz.1]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
z' : ℤ_[p] := z - z1
hdist :
  ‖Polynomial.eval z' (↑Polynomial.derivative F) - Polynomial.eval z (↑Polynomial.derivative F)‖ <
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖
⊢ ‖Polynomial.eval z' (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [sub_eq_add_neg, ← hz.1, ← norm_neg (F.derivative.eval z)] at hdist
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
z' : ℤ_[p] := z - z1
hdist :
  ‖Polynomial.eval z' (↑Polynomial.derivative F) + -Polynomial.eval z (↑Polynomial.derivative F)‖ <
    ‖-Polynomial.eval z (↑Polynomial.derivative F)‖
⊢ ‖Polynomial.eval z' (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
have := PadicInt.norm_eq_of_norm_add_lt_right hdist
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := { val := ↑(Polynomial.eval z F) / ↑(Polynomial.eval z (↑Polynomial.derivative F)), property := h1 }
z' : ℤ_[p] := z - z1
hdist :
  ‖Polynomial.eval z' (↑Polynomial.derivative F) + -Polynomial.eval z (↑Polynomial.derivative F)‖ <
    ‖-Polynomial.eval z (↑Polynomial.derivative F)‖
this : ‖Polynomial.eval z' (↑Polynomial.derivative F)‖ = ‖-Polynomial.eval z (↑Polynomial.derivative F)‖
⊢ ‖Polynomial.eval z' (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rwa [norm_neg, hz.1] at this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ ‖newton_seq (n + 1) - newton_seq n‖ =
    ‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval (newton_seq n) (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [newton_seq_gen, newton_seq_gen, newton_seq_aux, ih_n]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ ‖↑(let_fun h1 :=
            (_ :
              ‖↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) F) /
                    ↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) (↑Polynomial.derivative F))‖ ≤
                1);
          let z1 :=
            {
              val :=
                ↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) F) /
                  ↑(Polynomial.eval (↑(newton_seq_aux hnorm n)) (↑Polynomial.derivative F)),
              property := h1 };
          let z' := ↑(newton_seq_aux hnorm n) - z1;
          { val := z', property := (_ : ih_gen (n + 1) z') }) -
        ↑(newton_seq_aux hnorm n)‖ =
    ‖Polynomial.eval (↑(newton_seq_aux hnorm n)) F‖ /
      ‖Polynomial.eval (↑(newton_seq_aux hnorm n)) (↑Polynomial.derivative F)‖
[PROOFSTEP]
simp [sub_eq_add_neg, add_comm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ ‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval (newton_seq n) (↑Polynomial.derivative F)‖ =
    ‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [newton_seq_deriv_norm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ T_gen p F a > 0
[PROOFSTEP]
rw [T_def]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 > 0
[PROOFSTEP]
exact div_pos (norm_pos_iff.2 hnsol) (deriv_sq_norm_pos hnorm)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ 2 ≤ 2 ^ (n + 1)
[PROOFSTEP]
have := pow_le_pow (by norm_num : 1 ≤ 2) (Nat.le_add_left _ _ : 1 ≤ n + 1)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ 1 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ^ 1 ≤ 2 ^ (n + 1)
⊢ 2 ≤ 2 ^ (n + 1)
[PROOFSTEP]
simpa using this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ 1 < 2
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 1 =
    ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [T_gen, sq, pow_one, norm_div, ← mul_div_assoc, PadicInt.padic_norm_e_of_padicInt, PadicInt.coe_mul, padicNormE.mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * ‖Polynomial.eval a F‖ /
      (‖↑(Polynomial.eval a (↑Polynomial.derivative F))‖ * ‖↑(Polynomial.eval a (↑Polynomial.derivative F))‖) =
    ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
apply mul_div_mul_left
[GOAL]
case hc
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ≠ 0
[PROOFSTEP]
apply deriv_norm_ne_zero
[GOAL]
case hc.hnorm
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
assumption
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n : ℕ
⊢ ‖newton_seq (n + 0) - newton_seq n‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
simp [T_pow_nonneg, mul_nonneg]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
⊢ 2 ^ n ≤ 2 ^ (n + k)
[PROOFSTEP]
apply pow_le_pow
[GOAL]
case ha
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
⊢ 1 ≤ 2
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
⊢ n ≤ n + k
[PROOFSTEP]
norm_num
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
⊢ n ≤ n + k
[PROOFSTEP]
apply Nat.le_add_right
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
this : 2 ^ n ≤ 2 ^ (n + k)
⊢ ‖newton_seq (n + (k + 1)) - newton_seq n‖ = ‖newton_seq (n + k + 1) - newton_seq n‖
[PROOFSTEP]
rw [add_assoc]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
this : 2 ^ n ≤ 2 ^ (n + k)
⊢ ‖newton_seq (n + k + 1) - newton_seq n‖ =
    ‖newton_seq (n + k + 1) - newton_seq (n + k) + (newton_seq (n + k) - newton_seq n)‖
[PROOFSTEP]
rw [← sub_add_sub_cancel]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
hnk : n ≤ k
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
have hex : ∃ m, k = n + m := exists_eq_add_of_le hnk
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
let ⟨_, hex'⟩ := hex
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
w✝ : ℕ
hex' : k = n + w✝
⊢ ‖newton_seq k - newton_seq n‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
rw [hex']
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
n k : ℕ
hnk : n ≤ k
hex : ∃ m, k = n + m
w✝ : ℕ
hex' : k = n + w✝
⊢ ‖newton_seq (n + w✝) - newton_seq n‖ ≤ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n
[PROOFSTEP]
apply newton_seq_dist_aux
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
_h : 0 < 1
⊢ ‖newton_seq 1 - a‖ = ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
simp [sub_eq_add_neg, add_assoc, newton_seq_gen, newton_seq_aux, ih_n]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖
[PROOFSTEP]
rw [newton_seq_dist_to_a (k + 1) (succ_pos _)]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖Polynomial.eval a F‖ / ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
apply newton_seq_succ_dist_weak
[GOAL]
case hnsol
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
⊢ Polynomial.eval a F ≠ 0
[PROOFSTEP]
assumption
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
k : ℕ
_h : 0 < k + 2
hlt : ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖
hne' : ‖newton_seq (k + 2) - newton_seq (k + 1)‖ ≠ ‖newton_seq (k + 1) - a‖
⊢ ‖newton_seq (k + 2) - a‖ = ‖newton_seq (k + 2) - newton_seq (k + 1) + (newton_seq (k + 1) - a)‖
[PROOFSTEP]
rw [← sub_add_sub_cancel]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto (fun n => ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)
[PROOFSTEP]
rw [← mul_zero ‖F.derivative.eval a‖]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto (fun n => ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop
    (𝓝 (‖Polynomial.eval a (↑Polynomial.derivative F)‖ * 0))
[PROOFSTEP]
exact
  tendsto_const_nhds.mul
    (Tendsto.comp (tendsto_pow_atTop_nhds_0_of_lt_1 (norm_nonneg _) (T_lt_one hnorm))
      (Nat.tendsto_pow_atTop_atTop_of_one_lt (by norm_num)))
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ 1 < 2
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
have := bound' hnorm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this : Tendsto (fun n => ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)
⊢ ∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
simp [Tendsto, nhds] at this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this :
  ∀ (i : Set ℝ),
    0 ∈ i →
      IsOpen i → ∃ a_3, ∀ (b : ℕ), a_3 ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ i
⊢ ∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
intro ε hε
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this :
  ∀ (i : Set ℝ),
    0 ∈ i →
      IsOpen i → ∃ a_3, ∀ (b : ℕ), a_3 ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ i
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
cases' this (ball 0 ε) (mem_ball_self hε) isOpen_ball with N hN
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this :
  ∀ (i : Set ℝ),
    0 ∈ i →
      IsOpen i → ∃ a_3, ∀ (b : ℕ), a_3 ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ i
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ ball 0 ε
⊢ ∃ N, ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
exists N
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this :
  ∀ (i : Set ℝ),
    0 ∈ i →
      IsOpen i → ∃ a_3, ∀ (b : ℕ), a_3 ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ i
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ ball 0 ε
⊢ ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
intro n hn
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
this :
  ∀ (i : Set ℝ),
    0 ∈ i →
      IsOpen i → ∃ a_3, ∀ (b : ℕ), a_3 ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ i
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ b ∈ ball 0 ε
n : ℕ
hn : n ≥ N
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
[PROOFSTEP]
simpa [abs_of_nonneg T_nonneg] using hN _ hn
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto (fun n => ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)
[PROOFSTEP]
rw [← mul_zero ‖F.derivative.eval a‖, sq]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto
    (fun n =>
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * ‖Polynomial.eval a (↑Polynomial.derivative F)‖ *
        T_gen p F a ^ 2 ^ n)
    atTop (𝓝 (‖Polynomial.eval a (↑Polynomial.derivative F)‖ * 0))
[PROOFSTEP]
simp only [mul_assoc]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto
    (fun n =>
      ‖Polynomial.eval a (↑Polynomial.derivative F)‖ *
        (‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n))
    atTop (𝓝 (‖Polynomial.eval a (↑Polynomial.derivative F)‖ * 0))
[PROOFSTEP]
apply Tendsto.mul
[GOAL]
case hf
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto (fun x => ‖Polynomial.eval a (↑Polynomial.derivative F)‖) atTop
    (𝓝 ‖Polynomial.eval a (↑Polynomial.derivative F)‖)
[PROOFSTEP]
apply tendsto_const_nhds
[GOAL]
case hg
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Tendsto (fun x => ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ x) atTop (𝓝 0)
[PROOFSTEP]
apply bound'
[GOAL]
case hg.hnorm
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
assumption
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ IsCauSeq norm newton_seq
[PROOFSTEP]
intro ε hε
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖newton_seq j - newton_seq i‖ < ε
[PROOFSTEP]
cases' bound hnorm hε with N hN
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖newton_seq j - newton_seq i‖ < ε
[PROOFSTEP]
exists N
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
⊢ ∀ (j : ℕ), j ≥ N → ‖newton_seq j - newton_seq N‖ < ε
[PROOFSTEP]
intro j hj
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖newton_seq j - newton_seq N‖ < ε
[PROOFSTEP]
apply lt_of_le_of_lt
[GOAL]
case intro.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖newton_seq j - newton_seq N‖ ≤ ?intro.b
[PROOFSTEP]
apply newton_seq_dist hnorm hj
[GOAL]
case intro.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ N < ε
[PROOFSTEP]
apply hN
[GOAL]
case intro.a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ {n : ℕ}, n ≥ N → ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n < ε
j : ℕ
hj : j ≥ N
⊢ N ≥ N
[PROOFSTEP]
exact le_rfl
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖soln - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [soln_dist_to_a, div_lt_iff]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ <
    ‖Polynomial.eval a (↑Polynomial.derivative F)‖ * ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
rwa [sq] at hnorm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ 0 < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
apply deriv_norm_pos
[GOAL]
case hnorm
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
[PROOFSTEP]
assumption
[GOAL]
case hnsol
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
⊢ Polynomial.eval a F ≠ 0
[PROOFSTEP]
exact hnsol
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
⊢ ‖z - soln‖ = ‖z - a + (a - soln)‖
[PROOFSTEP]
rw [sub_add_sub_cancel]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ 0 = Polynomial.eval (soln + h) F
[PROOFSTEP]
simp [hev]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval (soln + h) F = Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
[PROOFSTEP]
rw [hq, eval_soln, zero_add]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2 =
    (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h
[PROOFSTEP]
rw [sq, right_distrib, mul_assoc]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
⊢ Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
[PROOFSTEP]
simpa using eq_neg_of_add_eq_zero_left this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖Polynomial.eval soln (↑Polynomial.derivative F)‖ = ‖-q * h‖
[PROOFSTEP]
rw [this]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖-q * h‖ ≤ 1 * ‖h‖
[PROOFSTEP]
rw [PadicInt.norm_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖-q‖ * ‖h‖ ≤ 1 * ‖h‖
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right (PadicInt.norm_le_one _) (norm_nonneg _)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ 1 * ‖h‖ = ‖z - soln‖
[PROOFSTEP]
simp
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖z - soln‖ < ‖Polynomial.eval soln (↑Polynomial.derivative F)‖
[PROOFSTEP]
rw [soln_deriv_norm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval soln (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval soln (↑Polynomial.derivative F) = -q * h
⊢ ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
apply soln_dist
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
hnsol : Polynomial.eval a F ≠ 0
z : ℤ_[p]
hev : Polynomial.eval z F = 0
hnlt : ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
soln_dist : ‖z - soln‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z - soln
q : ℤ_[p]
hq :
  Polynomial.eval (soln + h) F =
    Polynomial.eval soln F + Polynomial.eval soln (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval soln (↑Polynomial.derivative F) + q * h) * h = 0
this : h = 0
⊢ z - soln = 0
[PROOFSTEP]
rw [← this]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ 0 = Polynomial.eval (a + (z' - a)) F
[PROOFSTEP]
rw [add_comm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ 0 = Polynomial.eval (z' - a + a) F
[PROOFSTEP]
simp [hz']
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval (a + h) F = Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
[PROOFSTEP]
rw [hq, ha, zero_add]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
⊢ Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2 =
    (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h
[PROOFSTEP]
rw [sq, right_distrib, mul_assoc]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
⊢ Polynomial.eval a (↑Polynomial.derivative F) = -q * h
[PROOFSTEP]
simpa using eq_neg_of_add_eq_zero_left this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ ‖Polynomial.eval a (↑Polynomial.derivative F)‖ = ‖q‖ * ‖h‖
[PROOFSTEP]
simp [this]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ ‖q‖ * ‖h‖ ≤ 1 * ‖h‖
[PROOFSTEP]
gcongr
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ ‖q‖ ≤ 1
[PROOFSTEP]
apply PadicInt.norm_le_one
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝¹ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this✝ : Polynomial.eval a (↑Polynomial.derivative F) + q * h = 0
this : Polynomial.eval a (↑Polynomial.derivative F) = -q * h
⊢ 1 * ‖h‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
simpa
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
ha : Polynomial.eval a F = 0
z' : ℤ_[p]
hz' : Polynomial.eval z' F = 0
hnormz' : ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq : Polynomial.eval (a + h) F = Polynomial.eval a F + Polynomial.eval a (↑Polynomial.derivative F) * h + q * h ^ 2
this✝ : (Polynomial.eval a (↑Polynomial.derivative F) + q * h) * h = 0
this : h = 0
⊢ z' - a = 0
[PROOFSTEP]
rw [← this]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
ha : Polynomial.eval a F = 0
⊢ ‖a - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖
[PROOFSTEP]
simp [deriv_ne_zero hnorm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
F : Polynomial ℤ_[p]
a : ℤ_[p]
hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ^ 2
ha : ¬Polynomial.eval a F = 0
⊢ ∃ z,
    Polynomial.eval z F = 0 ∧
      ‖z - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ∧
        ‖Polynomial.eval z (↑Polynomial.derivative F)‖ = ‖Polynomial.eval a (↑Polynomial.derivative F)‖ ∧
          ∀ (z' : ℤ_[p]), Polynomial.eval z' F = 0 → ‖z' - a‖ < ‖Polynomial.eval a (↑Polynomial.derivative F)‖ → z' = z
[PROOFSTEP]
exact
  ⟨soln_gen hnorm, eval_soln hnorm, soln_dist_to_a_lt_deriv hnorm ha, soln_deriv_norm hnorm, fun z =>
    soln_unique hnorm ha z⟩