[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this : ∃ ε, ε > 0 ∧ ∃ N1, ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
⊢ padicNorm p (↑f m) = padicNorm p (↑f n)
[PROOFSTEP]
have : padicNorm p (f n - f m) < ε := hN2 _ (max_le_iff.1 hn).2 _ (max_le_iff.1 hm).2
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝ : ∃ ε, ε > 0 ∧ ∃ N1, ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this : padicNorm p (↑f n - ↑f m) < ε
⊢ padicNorm p (↑f m) = padicNorm p (↑f n)
[PROOFSTEP]
have : padicNorm p (f n - f m) < padicNorm p (f n) := lt_of_lt_of_le this <| hN1 _ (max_le_iff.1 hn).1
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝¹ : ∃ ε, ε > 0 ∧ ∃ N1, ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝ : padicNorm p (↑f n - ↑f m) < ε
this : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
⊢ padicNorm p (↑f m) = padicNorm p (↑f n)
[PROOFSTEP]
have : padicNorm p (f n - f m) < max (padicNorm p (f n)) (padicNorm p (f m)) := lt_max_iff.2 (Or.inl this)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε, ε > 0 ∧ ∃ N1, ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
⊢ padicNorm p (↑f m) = padicNorm p (↑f n)
[PROOFSTEP]
by_contra hne
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε, ε > 0 ∧ ∃ N1, ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
hne : ¬padicNorm p (↑f m) = padicNorm p (↑f n)
⊢ False
[PROOFSTEP]
rw [← padicNorm.neg (f m)] at hne 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε, ε > 0 ∧ ∃ N1, ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)
⊢ False
[PROOFSTEP]
have hnam := add_eq_max_of_ne hne
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε, ε > 0 ∧ ∃ N1, ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)
hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (-↑f m)) (padicNorm p (↑f n))
⊢ False
[PROOFSTEP]
rw [padicNorm.neg, max_comm] at hnam 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε, ε > 0 ∧ ∃ N1, ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (↑f n - ↑f m) < max (padicNorm p (↑f n)) (padicNorm p (↑f m))
hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)
hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (↑f n)) (padicNorm p (↑f m))
⊢ False
[PROOFSTEP]
rw [← hnam, sub_eq_add_neg, add_comm] at this 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ (padicNorm p)
hf : ¬f ≈ 0
this✝² : ∃ ε, ε > 0 ∧ ∃ N1, ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
ε : ℚ
hε : ε > 0
N1 : ℕ
hN1 : ∀ (j : ℕ), j ≥ N1 → ε ≤ padicNorm p (↑f j)
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → padicNorm p (↑f j - ↑f k) < ε
n m : ℕ
hn : max N1 N2 ≤ n
hm : max N1 N2 ≤ m
this✝¹ : padicNorm p (↑f n - ↑f m) < ε
this✝ : padicNorm p (↑f n - ↑f m) < padicNorm p (↑f n)
this : padicNorm p (-↑f m + ↑f n) < padicNorm p (-↑f m + ↑f n)
hne : ¬padicNorm p (-↑f m) = padicNorm p (↑f n)
hnam : padicNorm p (-↑f m + ↑f n) = max (padicNorm p (↑f n)) (padicNorm p (↑f m))
⊢ False
[PROOFSTEP]
apply _root_.lt_irrefl _ this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ norm f = 0 ↔ f ≈ 0
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ norm f = 0 → f ≈ 0
[PROOFSTEP]
intro h
[GOAL]
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : norm f = 0
⊢ f ≈ 0
[PROOFSTEP]
by_contra hf
[GOAL]
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : norm f = 0
hf : ¬f ≈ 0
⊢ False
[PROOFSTEP]
unfold norm at h 
[GOAL]
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) = 0
hf : ¬f ≈ 0
⊢ False
[PROOFSTEP]
split_ifs at h 
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h✝ : f ≈ 0
h : 0 = 0
⊢ False
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
⊢ False
[PROOFSTEP]
apply hf
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
⊢ f ≈ 0
[PROOFSTEP]
intro ε hε
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → padicNorm p (↑(f - 0) j) < ε
[PROOFSTEP]
exists stationaryPoint hf
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
ε : ℚ
hε : ε > 0
⊢ ∀ (j : ℕ), j ≥ stationaryPoint hf → padicNorm p (↑(f - 0) j) < ε
[PROOFSTEP]
intro j hj
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
ε : ℚ
hε : ε > 0
j : ℕ
hj : j ≥ stationaryPoint hf
⊢ padicNorm p (↑(f - 0) j) < ε
[PROOFSTEP]
have heq := stationaryPoint_spec hf le_rfl hj
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
ε : ℚ
hε : ε > 0
j : ℕ
hj : j ≥ stationaryPoint hf
heq : padicNorm p (↑f j) = padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑(f - 0) j) < ε
[PROOFSTEP]
simpa [h, heq]
[GOAL]
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ f ≈ 0 → norm f = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : f ≈ 0
⊢ norm f = 0
[PROOFSTEP]
simp [norm, h]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : f ≈ 0
ε : ℚ
hε : ε > 0
i : ℕ
hi : ∀ (j : ℕ), j ≥ i → padicNorm p (↑(f - 0) j) < ε
j : ℕ
hj : j ≥ i
⊢ padicNorm p (↑(g - 0) j) < ε
[PROOFSTEP]
simpa [h] using hi _ hj
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ norm f = padicNorm p (↑f (stationaryPoint hf))
[PROOFSTEP]
simp [norm, hf]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
heq : norm f = padicNorm p (↑f (stationaryPoint hf))
h : ↑f (stationaryPoint hf) = 0
⊢ norm f = 0
[PROOFSTEP]
simpa [h] using heq
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
h : LimZero (const (padicNorm p) q - 0)
⊢ LimZero (const (padicNorm (?m.10166 hq h)) q)
[PROOFSTEP]
simpa using h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : f ≈ 0
⊢ 0 ≤ norm f
[PROOFSTEP]
simp [hf, norm]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ 0 ≤ norm f
[PROOFSTEP]
simp [norm, hf, padicNorm.nonneg]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max (stationaryPoint hf) (max v2 v3)))
[PROOFSTEP]
apply stationaryPoint_spec hf
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ max (stationaryPoint hf) (max v2 v3)
[PROOFSTEP]
apply le_max_left
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v2 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf
[PROOFSTEP]
exact le_rfl
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max v1 (max (stationaryPoint hf) v3)))
[PROOFSTEP]
apply stationaryPoint_spec hf
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ max v1 (max (stationaryPoint hf) v3)
[PROOFSTEP]
apply le_trans
[GOAL]
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ ?a.b✝
[PROOFSTEP]
apply le_max_left _ v3
[GOAL]
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ max (stationaryPoint hf) v3 ≤ max v1 (max (stationaryPoint hf) v3)
[PROOFSTEP]
apply le_max_right
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v3 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf
[PROOFSTEP]
exact le_rfl
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f (max v1 (max v2 (stationaryPoint hf))))
[PROOFSTEP]
apply stationaryPoint_spec hf
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ max v1 (max v2 (stationaryPoint hf))
[PROOFSTEP]
apply le_trans
[GOAL]
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ ?a.b✝
[PROOFSTEP]
apply le_max_right v2
[GOAL]
case a.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ max v2 (stationaryPoint hf) ≤ max v1 (max v2 (stationaryPoint hf))
[PROOFSTEP]
apply le_max_right
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
v1 v2 : ℕ
⊢ stationaryPoint hf ≤ stationaryPoint hf
[PROOFSTEP]
exact le_rfl
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ norm f = ↑p ^ (-valuation f)
[PROOFSTEP]
rw [norm, valuation, dif_neg hf, dif_neg hf, padicNorm, if_neg]
[GOAL]
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ ¬↑f (stationaryPoint hf) = 0
[PROOFSTEP]
intro H
[GOAL]
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
⊢ False
[PROOFSTEP]
apply CauSeq.not_limZero_of_not_congr_zero hf
[GOAL]
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
⊢ LimZero f
[PROOFSTEP]
intro ε hε
[GOAL]
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → padicNorm p (↑f j) < ε
[PROOFSTEP]
use stationaryPoint hf
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
⊢ ∀ (j : ℕ), j ≥ stationaryPoint hf → padicNorm p (↑f j) < ε
[PROOFSTEP]
intro n hn
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f n) < ε
[PROOFSTEP]
rw [stationaryPoint_spec hf le_rfl hn]
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f (stationaryPoint hf)) < ε
[PROOFSTEP]
simpa [H] using hε
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ valuation f = valuation g ↔ norm f = norm g
[PROOFSTEP]
rw [norm_eq_pow_val hf, norm_eq_pow_val hg, ← neg_inj, zpow_inj]
[GOAL]
case h₀
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ 0 < ↑p
[PROOFSTEP]
exact_mod_cast (Fact.out : p.Prime).pos
[GOAL]
case h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ↑p ≠ 1
[PROOFSTEP]
exact_mod_cast (Fact.out : p.Prime).ne_one
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
⊢ norm (f * g) = norm f * norm g
[PROOFSTEP]
have hg : f * g ≈ 0 := mul_equiv_zero' _ hf
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : f ≈ 0
hg : f * g ≈ 0
⊢ norm (f * g) = norm f * norm g
[PROOFSTEP]
simp only [hf, hg, norm, dif_pos, zero_mul]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ norm (f * g) = norm f * norm g
[PROOFSTEP]
have hf : f * g ≈ 0 := mul_equiv_zero _ hg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf✝ : ¬f ≈ 0
hg : g ≈ 0
hf : f * g ≈ 0
⊢ norm (f * g) = norm f * norm g
[PROOFSTEP]
simp only [hf, hg, norm, dif_pos, mul_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ norm (f * g) = norm f * norm g
[PROOFSTEP]
unfold norm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f * g ≈ 0 then 0 else padicNorm p (↑(f * g) (stationaryPoint hf))) =
    (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) *
      if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))
[PROOFSTEP]
split_ifs with hfg
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f * g ≈ 0
⊢ 0 = padicNorm p (↑f (stationaryPoint hf)) * padicNorm p (↑g (stationaryPoint hg))
case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p (↑(f * g) (stationaryPoint hfg)) =
    padicNorm p (↑f (stationaryPoint hf)) * padicNorm p (↑g (stationaryPoint hg))
[PROOFSTEP]
exact (mul_not_equiv_zero hf hg hfg).elim
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p (↑(f * g) (stationaryPoint hfg)) =
    padicNorm p (↑f (stationaryPoint hf)) * padicNorm p (↑g (stationaryPoint hg))
[PROOFSTEP]
rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ padicNorm p (↑(f * g) (max (stationaryPoint hfg) (max ?neg.v2✝ ?neg.v3✝))) =
    padicNorm p (↑f (max ?neg.v1✝ (max (stationaryPoint hf) ?neg.v3✝))) *
      padicNorm p (↑g (max ?neg.v1✝ (max ?neg.v2✝ (stationaryPoint hg))))
case neg.v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : ¬f * g ≈ 0
⊢ ℕ
case neg.v3 p : ℕ hp : Fact (Nat.Prime p) f g : PadicSeq p hf : ¬f ≈ 0 hg : ¬g ≈ 0 hfg : ¬f * g ≈ 0 ⊢ ℕ
[PROOFSTEP]
apply padicNorm.mul
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
[PROOFSTEP]
have : const (padicNorm p) q ≈ 0 := by simp [hq]; apply Setoid.refl (const (padicNorm p) 0)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ const (padicNorm p) q ≈ 0
[PROOFSTEP]
simp [hq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
⊢ 0 ≈ 0
[PROOFSTEP]
apply Setoid.refl (const (padicNorm p) 0)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : q = 0
this : const (padicNorm p) q ≈ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
[PROOFSTEP]
subst hq
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
this : const (padicNorm p) 0 ≈ 0
⊢ norm (const (padicNorm p) 0) = padicNorm p 0
[PROOFSTEP]
simp [norm, this]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
[PROOFSTEP]
have : ¬const (padicNorm p) q ≈ 0 := not_equiv_zero_const_of_nonzero hq
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
hq : ¬q = 0
this : ¬const (padicNorm p) q ≈ 0
⊢ norm (const (padicNorm p) q) = padicNorm p q
[PROOFSTEP]
simp [norm, this]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
⊢ ∃ z, norm a = ↑p ^ (-z)
[PROOFSTEP]
let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
k : ℚ
hk : norm a = padicNorm p k
hk' : k ≠ 0
⊢ ∃ z, norm a = ↑p ^ (-z)
[PROOFSTEP]
simpa [hk] using padicNorm.values_discrete hk'
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ norm 1 = 1
[PROOFSTEP]
have h1 : ¬(1 : PadicSeq p) ≈ 0 := one_not_equiv_zero _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
h1 : ¬1 ≈ 0
⊢ norm 1 = 1
[PROOFSTEP]
simp [h1, norm, hp.1.one_lt]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ False
[PROOFSTEP]
have hpn : 0 < padicNorm p (f (stationaryPoint hf)) - padicNorm p (g (stationaryPoint hg)) := sub_pos_of_lt hlt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
⊢ False
[PROOFSTEP]
cases' hfg _ hpn with N hN
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
⊢ False
[PROOFSTEP]
let i := max N (max (stationaryPoint hf) (stationaryPoint hg))
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
⊢ False
[PROOFSTEP]
have hi : N ≤ i := le_max_left _ _
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
⊢ False
[PROOFSTEP]
have hN' := hN _ hi
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' : padicNorm p (↑(f - g) i) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
⊢ False
[PROOFSTEP]
rw [lift_index_left hf N (stationaryPoint hg), lift_index_right hg N (stationaryPoint hf)] at hN' h hlt 
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑(f - g) i) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
⊢ False
[PROOFSTEP]
have hpne : padicNorm p (f i) ≠ padicNorm p (-g i) := by rwa [← padicNorm.neg (g i)] at h 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑(f - g) i) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
⊢ padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
[PROOFSTEP]
rwa [← padicNorm.neg (g i)] at h 
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑(f - g) i) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ False
[PROOFSTEP]
rw [CauSeq.sub_apply, sub_eq_add_neg, add_eq_max_of_ne hpne, padicNorm.neg, max_eq_left_of_lt hlt] at hN' 
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ False
[PROOFSTEP]
have : padicNorm p (f i) < padicNorm p (f i) :=
  by
  apply lt_of_lt_of_le hN'
  apply sub_le_self
  apply padicNorm.nonneg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ padicNorm p (↑f i) < padicNorm p (↑f i)
[PROOFSTEP]
apply lt_of_lt_of_le hN'
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≤
    padicNorm p (↑f i)
[PROOFSTEP]
apply sub_le_self
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
⊢ 0 ≤ padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
[PROOFSTEP]
apply padicNorm.nonneg
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
hpn : 0 < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
N : ℕ
hlt :
  padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg))))
h :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) ≠
    padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hN :
  ∀ (j : ℕ),
    j ≥ N → padicNorm p (↑(f - g) j) < padicNorm p (↑f (stationaryPoint hf)) - padicNorm p (↑g (stationaryPoint hg))
i : ℕ := max N (max (stationaryPoint hf) (stationaryPoint hg))
hi : N ≤ i
hN' :
  padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) <
    padicNorm p (↑f (max N (max (stationaryPoint hf) (stationaryPoint hg)))) -
      padicNorm p (↑g (max N (max (stationaryPoint hf) (stationaryPoint hg))))
hpne : padicNorm p (↑f i) ≠ padicNorm p (-↑g i)
this : padicNorm p (↑f i) < padicNorm p (↑f i)
⊢ False
[PROOFSTEP]
exact lt_irrefl _ this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
[PROOFSTEP]
by_contra h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
⊢ False
[PROOFSTEP]
cases' Decidable.em (padicNorm p (g (stationaryPoint hg)) < padicNorm p (f (stationaryPoint hf))) with hlt hnlt
[GOAL]
case inl
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hlt : padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ False
[PROOFSTEP]
exact norm_eq_of_equiv_aux hf hg hfg h hlt
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ False
[PROOFSTEP]
apply norm_eq_of_equiv_aux hg hf (Setoid.symm hfg) (Ne.symm h)
[GOAL]
case inr
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) < padicNorm p (↑g (stationaryPoint hg))
[PROOFSTEP]
apply lt_of_le_of_ne
[GOAL]
case inr.a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) ≤ padicNorm p (↑g (stationaryPoint hg))
case inr.a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
[PROOFSTEP]
apply le_of_not_gt hnlt
[GOAL]
case inr.a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hnlt : ¬padicNorm p (↑g (stationaryPoint hg)) < padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
[PROOFSTEP]
apply h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
⊢ norm f = norm g
[PROOFSTEP]
have hg : g ≈ 0 := Setoid.trans (Setoid.symm hfg) hf
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : f ≈ 0
hg : g ≈ 0
⊢ norm f = norm g
[PROOFSTEP]
simp [norm, hf, hg]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
⊢ norm f = norm g
[PROOFSTEP]
have hg : ¬g ≈ 0 := hf ∘ Setoid.trans hfg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ norm f = norm g
[PROOFSTEP]
unfold norm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) =
    if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))
[PROOFSTEP]
split_ifs
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
[PROOFSTEP]
exact norm_eq_of_equiv hf hg hfg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
unfold norm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f + g ≈ 0 then 0 else padicNorm p (↑(f + g) (stationaryPoint hf))) ≤
    max (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf)))
      (if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf)))
[PROOFSTEP]
split_ifs
  -- Porting note: originally `padic_index_simp [hfg, hf, hg]`
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) ≤
    max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))
[PROOFSTEP]
rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p (↑(f + g) (max (stationaryPoint hfg) (max ?v2 ?v3))) ≤
    max (padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))))
      (padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg)))))
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ ℕ
case v3 p : ℕ hp : Fact (Nat.Prime p) f g : PadicSeq p hfg : ¬f + g ≈ 0 hf : ¬f ≈ 0 hg : ¬g ≈ 0 ⊢ ℕ
[PROOFSTEP]
apply padicNorm.nonarchimedean
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
have : 0 ≤ max f.norm g.norm := le_max_of_le_left (norm_nonneg _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : f + g ≈ 0
this : 0 ≤ max (norm f) (norm g)
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
simpa only [hfg, norm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
have hfg' : f + g ≈ g := by
  change LimZero (f - 0) at hf 
  show LimZero (f + g - g); · simpa only [sub_zero, add_sub_cancel] using hf
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ f + g ≈ g
[PROOFSTEP]
change LimZero (f - 0) at hf 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : LimZero (f - 0)
⊢ f + g ≈ g
[PROOFSTEP]
show LimZero (f + g - g)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : LimZero (f - 0)
⊢ LimZero (f + g - g)
[PROOFSTEP]
simpa only [sub_zero, add_sub_cancel] using hf
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
have hcfg : (f + g).norm = g.norm := norm_equiv hfg'
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
have hcl : f.norm = 0 := (norm_zero_iff f).2 hf
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
have : max f.norm g.norm = g.norm := by rw [hcl]; exact max_eq_right (norm_nonneg _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
⊢ max (norm f) (norm g) = norm g
[PROOFSTEP]
rw [hcl]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
⊢ max 0 (norm g) = norm g
[PROOFSTEP]
exact max_eq_right (norm_nonneg _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : f ≈ 0
hfg' : f + g ≈ g
hcfg : norm (f + g) = norm g
hcl : norm f = 0
this : max (norm f) (norm g) = norm g
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
rw [this, hcfg]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
have hfg' : f + g ≈ f := by
  change LimZero (g - 0) at hg 
  show LimZero (f + g - f); · simpa only [add_sub_cancel', sub_zero] using hg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ f + g ≈ f
[PROOFSTEP]
change LimZero (g - 0) at hg 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : LimZero (g - 0)
⊢ f + g ≈ f
[PROOFSTEP]
show LimZero (f + g - f)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : LimZero (g - 0)
⊢ LimZero (f + g - f)
[PROOFSTEP]
simpa only [add_sub_cancel', sub_zero] using hg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
have hcfg : (f + g).norm = f.norm := norm_equiv hfg'
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : norm (f + g) = norm f
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
have hcl : g.norm = 0 := (norm_zero_iff g).2 hg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : norm (f + g) = norm f
hcl : norm g = 0
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
have : max f.norm g.norm = f.norm := by rw [hcl]; exact max_eq_left (norm_nonneg _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : norm (f + g) = norm f
hcl : norm g = 0
⊢ max (norm f) (norm g) = norm f
[PROOFSTEP]
rw [hcl]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : norm (f + g) = norm f
hcl : norm g = 0
⊢ max (norm f) 0 = norm f
[PROOFSTEP]
exact max_eq_left (norm_nonneg _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
hfg' : f + g ≈ f
hcfg : norm (f + g) = norm f
hcl : norm g = 0
this : max (norm f) (norm g) = norm f
⊢ norm (f + g) ≤ max (norm f) (norm g)
[PROOFSTEP]
rw [this, hcfg]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : f ≈ 0
⊢ norm f = norm g
[PROOFSTEP]
have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : f ≈ 0
hg : g ≈ 0
⊢ norm f = norm g
[PROOFSTEP]
simp only [hf, hg, norm, dif_pos]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
⊢ norm f = norm g
[PROOFSTEP]
have hg : ¬g ≈ 0 := fun hg ↦
  hf <| equiv_zero_of_val_eq_of_equiv_zero (by simp only [h, forall_const, eq_self_iff_true]) hg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ ∀ (k : ℕ), padicNorm p (↑g k) = padicNorm p (↑f k)
[PROOFSTEP]
simp only [h, forall_const, eq_self_iff_true]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ norm f = norm g
[PROOFSTEP]
simp only [hg, hf, norm, dif_neg, not_false_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ padicNorm p (↑f (stationaryPoint (_ : ¬f ≈ 0))) = padicNorm p (↑g (stationaryPoint (_ : ¬g ≈ 0)))
[PROOFSTEP]
let i := max (stationaryPoint hf) (stationaryPoint hg)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
⊢ padicNorm p (↑f (stationaryPoint (_ : ¬f ≈ 0))) = padicNorm p (↑g (stationaryPoint (_ : ¬g ≈ 0)))
[PROOFSTEP]
have hpf : padicNorm p (f (stationaryPoint hf)) = padicNorm p (f i) :=
  by
  apply stationaryPoint_spec
  apply le_max_left
  exact le_rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
⊢ padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
[PROOFSTEP]
apply stationaryPoint_spec
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
⊢ stationaryPoint ?hf ≤ i
case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
⊢ stationaryPoint ?hf ≤ stationaryPoint hf
case hf
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
⊢ ¬f ≈ 0
[PROOFSTEP]
apply le_max_left
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
⊢ stationaryPoint hf ≤ stationaryPoint hf
[PROOFSTEP]
exact le_rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ padicNorm p (↑f (stationaryPoint (_ : ¬f ≈ 0))) = padicNorm p (↑g (stationaryPoint (_ : ¬g ≈ 0)))
[PROOFSTEP]
have hpg : padicNorm p (g (stationaryPoint hg)) = padicNorm p (g i) :=
  by
  apply stationaryPoint_spec
  apply le_max_right
  exact le_rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ padicNorm p (↑g (stationaryPoint hg)) = padicNorm p (↑g i)
[PROOFSTEP]
apply stationaryPoint_spec
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint ?hf ≤ i
case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint ?hf ≤ stationaryPoint hg
case hf
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ ¬g ≈ 0
[PROOFSTEP]
apply le_max_right
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
⊢ stationaryPoint hg ≤ stationaryPoint hg
[PROOFSTEP]
exact le_rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : ¬f ≈ 0
hg : ¬g ≈ 0
i : ℕ := max (stationaryPoint hf) (stationaryPoint hg)
hpf : padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑f i)
hpg : padicNorm p (↑g (stationaryPoint hg)) = padicNorm p (↑g i)
⊢ padicNorm p (↑f (stationaryPoint (_ : ¬f ≈ 0))) = padicNorm p (↑g (stationaryPoint (_ : ¬g ≈ 0)))
[PROOFSTEP]
rw [hpf, hpg, h]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
⊢ ∀ (k : ℕ), padicNorm p (↑(-a) k) = padicNorm p (↑a k)
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
⊢ norm f = norm g
[PROOFSTEP]
have : LimZero (f + g - 0) := h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : LimZero (f + g - 0)
⊢ norm f = norm g
[PROOFSTEP]
have : f ≈ -g := show LimZero (f - -g) by simpa only [sub_zero, sub_neg_eq_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this : LimZero (f + g - 0)
⊢ LimZero (f - -g)
[PROOFSTEP]
simpa only [sub_zero, sub_neg_eq_add]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝ : LimZero (f + g - 0)
this : f ≈ -g
⊢ norm f = norm g
[PROOFSTEP]
have : f.norm = (-g).norm := norm_equiv this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : f + g ≈ 0
this✝¹ : LimZero (f + g - 0)
this✝ : f ≈ -g
this : norm f = norm (-g)
⊢ norm f = norm g
[PROOFSTEP]
simpa only [norm_neg] using this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : f ≈ 0
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
have : LimZero (f - 0) := hf
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this : LimZero (f - 0)
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
have : f + g ≈ g := show LimZero (f + g - g) by simpa only [sub_zero, add_sub_cancel]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this : LimZero (f - 0)
⊢ LimZero (f + g - g)
[PROOFSTEP]
simpa only [sub_zero, add_sub_cancel]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this✝ : LimZero (f - 0)
this : f + g ≈ g
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
have h1 : (f + g).norm = g.norm := norm_equiv this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this✝ : LimZero (f - 0)
this : f + g ≈ g
h1 : norm (f + g) = norm g
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
have h2 : f.norm = 0 := (norm_zero_iff _).2 hf
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : f ≈ 0
this✝ : LimZero (f - 0)
this : f + g ≈ g
h1 : norm (f + g) = norm g
h2 : norm f = 0
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
rw [h1, h2, max_eq_right (norm_nonneg _)]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
have : LimZero (g - 0) := hg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this : LimZero (g - 0)
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
have : f + g ≈ f := show LimZero (f + g - f) by rw [add_sub_cancel']; simpa only [sub_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this : LimZero (g - 0)
⊢ LimZero (f + g - f)
[PROOFSTEP]
rw [add_sub_cancel']
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this : LimZero (g - 0)
⊢ LimZero g
[PROOFSTEP]
simpa only [sub_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : LimZero (g - 0)
this : f + g ≈ f
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
have h1 : (f + g).norm = f.norm := norm_equiv this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : LimZero (g - 0)
this : f + g ≈ f
h1 : norm (f + g) = norm f
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
have h2 : g.norm = 0 := (norm_zero_iff _).2 hg
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : g ≈ 0
this✝ : LimZero (g - 0)
this : f + g ≈ f
h1 : norm (f + g) = norm f
h2 : norm g = 0
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
rw [h1, h2, max_eq_left (norm_nonneg _)]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne : norm f ≠ norm g
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ norm (f + g) = max (norm f) (norm g)
[PROOFSTEP]
unfold norm at hfgne ⊢
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfgne :
  (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf))) ≠
    if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf))
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ (if hf : f + g ≈ 0 then 0 else padicNorm p (↑(f + g) (stationaryPoint hf))) =
    max (if hf : f ≈ 0 then 0 else padicNorm p (↑f (stationaryPoint hf)))
      (if hf : g ≈ 0 then 0 else padicNorm p (↑g (stationaryPoint hf)))
[PROOFSTEP]
split_ifs at hfgne ⊢
  -- Porting note: originally `padic_index_simp [hfg, hf, hg] at hfgne ⊢`
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) =
    max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))
[PROOFSTEP]
rw [lift_index_left hf, lift_index_right hg] at hfgne 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ padicNorm p (↑(f + g) (stationaryPoint hfg)) =
    max (padicNorm p (↑f (stationaryPoint hf))) (padicNorm p (↑g (stationaryPoint hg)))
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
[PROOFSTEP]
rw [lift_index_left_left hfg, lift_index_left hf, lift_index_right hg]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ padicNorm p (↑(f + g) (max (stationaryPoint hfg) (max ?v2 ?v3))) =
    max (padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))))
      (padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg)))))
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝¹ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne✝ : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne :
  padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (max ?v1 (max ?v2 (stationaryPoint hg))))
⊢ ℕ
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
case v2
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne✝ : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
hfgne : padicNorm p (↑f (max ?v1 (max (stationaryPoint hf) ?v3))) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
case v1
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
case v3
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hfg : ¬f + g ≈ 0
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfgne : padicNorm p (↑f (stationaryPoint hf)) ≠ padicNorm p (↑g (stationaryPoint hg))
⊢ ℕ
[PROOFSTEP]
exact padicNorm.add_eq_max_of_ne hfgne
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Zero ℚ_[p]
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ One ℚ_[p]
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Add ℚ_[p]
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Mul ℚ_[p]
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Sub ℚ_[p]
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Neg ℚ_[p]
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Div ℚ_[p]
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ AddCommGroup ℚ_[p]
[PROOFSTEP]
infer_instance
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
q r : ℚ
heq : q = r
⊢ const (padicNorm p) q ≈ const (padicNorm p) r
[PROOFSTEP]
rw [heq]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
q r : ℚ
h : q = r
⊢ ↑q = ↑r
[PROOFSTEP]
rw [h]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
m n : ℕ
⊢ ↑m = ↑n → m = n
[PROOFSTEP]
rw [← Rat.cast_coe_nat]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
m n : ℕ
⊢ ↑↑m = ↑n → m = n
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
m n : ℕ
⊢ m = n → m = n
[PROOFSTEP]
exact id
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
r : CauSeq ℚ (padicNorm p)
⊢ MulHom.toFun
        { toFun := Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g),
          map_mul' :=
            (_ :
              ∀ (q r : ℚ_[p]),
                Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                    (q * r) =
                  Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q *
                    Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                      r) }
        (Quotient.mk equiv r) =
      0 ↔
    Quotient.mk equiv r = 0
[PROOFSTEP]
rw [Padic.zero_def, Quotient.eq]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
r : CauSeq ℚ (padicNorm p)
⊢ MulHom.toFun
        { toFun := Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g),
          map_mul' :=
            (_ :
              ∀ (q r : ℚ_[p]),
                Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                    (q * r) =
                  Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q *
                    Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                      r) }
        (Quotient.mk equiv r) =
      0 ↔
    r ≈ 0
[PROOFSTEP]
exact PadicSeq.norm_zero_iff r
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ MulHom.toFun
      { toFun := Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g),
        map_mul' :=
          (_ :
            ∀ (q r : ℚ_[p]),
              Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                  (q * r) =
                Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q *
                  Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) r) }
      (q + r) ≤
    MulHom.toFun
        { toFun := Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g),
          map_mul' :=
            (_ :
              ∀ (q r : ℚ_[p]),
                Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                    (q * r) =
                  Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q *
                    Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                      r) }
        q +
      MulHom.toFun
        { toFun := Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g),
          map_mul' :=
            (_ :
              ∀ (q r : ℚ_[p]),
                Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                    (q * r) =
                  Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q *
                    Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                      r) }
        r
[PROOFSTEP]
trans
  max ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) q)
    ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) r)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ MulHom.toFun
      { toFun := Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g),
        map_mul' :=
          (_ :
            ∀ (q r : ℚ_[p]),
              Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                  (q * r) =
                Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q *
                  Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) r) }
      (q + r) ≤
    max (Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q)
      (Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) r)
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ max (Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q)
      (Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) r) ≤
    MulHom.toFun
        { toFun := Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g),
          map_mul' :=
            (_ :
              ∀ (q r : ℚ_[p]),
                Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                    (q * r) =
                  Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q *
                    Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                      r) }
        q +
      MulHom.toFun
        { toFun := Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g),
          map_mul' :=
            (_ :
              ∀ (q r : ℚ_[p]),
                Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                    (q * r) =
                  Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q *
                    Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                      r) }
        r
[PROOFSTEP]
exact Quotient.inductionOn₂ q r <| PadicSeq.norm_nonarchimedean
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ max (Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q)
      (Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) r) ≤
    MulHom.toFun
        { toFun := Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g),
          map_mul' :=
            (_ :
              ∀ (q r : ℚ_[p]),
                Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                    (q * r) =
                  Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q *
                    Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                      r) }
        q +
      MulHom.toFun
        { toFun := Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g),
          map_mul' :=
            (_ :
              ∀ (q r : ℚ_[p]),
                Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                    (q * r) =
                  Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) q *
                    Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
                      r) }
        r
[PROOFSTEP]
refine' max_le_add_of_nonneg (Quotient.inductionOn q <| PadicSeq.norm_nonneg) _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ 0 ≤ Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g) r
[PROOFSTEP]
exact Quotient.inductionOn r <| PadicSeq.norm_nonneg
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (Padic.mk f - ↑(↑f i)) < ε
[PROOFSTEP]
dsimp [padicNormE]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N,
    ∀ (i : ℕ),
      i ≥ N →
        Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
            (Padic.mk f - ↑(↑f i)) <
          ε
[PROOFSTEP]
change ∃ N, ∀ i ≥ N, (f - const _ (f i)).norm < ε
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → PadicSeq.norm (f - const (padicNorm p) (↑f i)) < ε
[PROOFSTEP]
by_contra' h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
⊢ False
[PROOFSTEP]
cases' cauchy₂ f hε with N hN
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
⊢ False
[PROOFSTEP]
rcases h N with ⟨i, hi, hge⟩
[GOAL]
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
⊢ False
[PROOFSTEP]
have hne : ¬f - const (padicNorm p) (f i) ≈ 0 := by
  intro h
  unfold PadicSeq.norm at hge ; split_ifs at hge 
  exact not_lt_of_ge hge hε
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
⊢ ¬f - const (padicNorm p) (↑f i) ≈ 0
[PROOFSTEP]
intro h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
[PROOFSTEP]
unfold PadicSeq.norm at hge 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge :
  ε ≤
    if hf : f - const (padicNorm p) (↑f i) ≈ 0 then 0
    else padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hf))
h : f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
[PROOFSTEP]
split_ifs at hge 
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h✝ : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
h : f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ 0
⊢ False
[PROOFSTEP]
exact not_lt_of_ge hge hε
[GOAL]
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge : ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
[PROOFSTEP]
unfold PadicSeq.norm at hge 
[GOAL]
case intro.intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hge :
  ε ≤
    if hf : f - const (padicNorm p) (↑f i) ≈ 0 then 0
    else padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hf))
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
⊢ False
[PROOFSTEP]
split_ifs at hge 
[GOAL]
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne : ¬f - const (padicNorm p) (↑f i) ≈ 0
h✝ : f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ 0
⊢ False
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
⊢ False
[PROOFSTEP]
exact not_le_of_gt hε hge
[GOAL]
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
⊢ False
[PROOFSTEP]
apply not_le_of_gt _ hge
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
[PROOFSTEP]
cases' _root_.em (N ≤ stationaryPoint hne) with hgen hngen
[GOAL]
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hgen : N ≤ stationaryPoint hne
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
[PROOFSTEP]
apply hN _ hgen _ hi
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hngen : ¬N ≤ stationaryPoint hne
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
[PROOFSTEP]
have := stationaryPoint_spec hne le_rfl (le_of_not_le hngen)
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hngen : ¬N ≤ stationaryPoint hne
this :
  padicNorm p (↑(f - const (padicNorm p) (↑f i)) N) =
    padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
[PROOFSTEP]
rw [← this]
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
ε : ℚ
hε : 0 < ε
h : ∀ (N : ℕ), ∃ i, i ≥ N ∧ ε ≤ PadicSeq.norm (f - const (padicNorm p) (↑f i))
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ∀ (k : ℕ), k ≥ N → padicNorm p (↑f j - ↑f k) < ε
i : ℕ
hi : i ≥ N
hne h✝ : ¬f - const (padicNorm p) (↑f i) ≈ 0
hge : ε ≤ padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint h✝))
hngen : ¬N ≤ stationaryPoint hne
this :
  padicNorm p (↑(f - const (padicNorm p) (↑f i)) N) =
    padicNorm p (↑(f - const (padicNorm p) (↑f i)) (stationaryPoint hne))
⊢ ε > padicNorm p (↑(f - const (padicNorm p) (↑f i)) N)
[PROOFSTEP]
exact hN _ le_rfl _ hi
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
⊢ ↑padicNormE (Quotient.mk equiv q' - ↑(↑q' N)) < ε
[PROOFSTEP]
dsimp [padicNormE]
  -- Porting note: `change` → `convert_to` (`change` times out!)
        -- and add `PadicSeq p` type annotation
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
⊢ Quotient.lift PadicSeq.norm (_ : ∀ {f g : PadicSeq p}, f ≈ g → PadicSeq.norm f = PadicSeq.norm g)
      (Completion.mk q' - ↑(↑q' N)) <
    ε
[PROOFSTEP]
convert_to PadicSeq.norm (q' - const _ (q' N) : PadicSeq p) < ε
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
⊢ PadicSeq.norm (q' - const (padicNorm p) (↑q' N)) < ε
[PROOFSTEP]
cases' Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq hne'
[GOAL]
case inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
heq : q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ PadicSeq.norm (q' - const (padicNorm p) (↑q' N)) < ε
[PROOFSTEP]
simpa only [heq, PadicSeq.norm, dif_pos]
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ PadicSeq.norm (q' - const (padicNorm p) (↑q' N)) < ε
[PROOFSTEP]
simp only [PadicSeq.norm, dif_neg hne']
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) (stationaryPoint hne')) < ε
[PROOFSTEP]
change padicNorm p (q' _ - q' _) < ε
[GOAL]
case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
[PROOFSTEP]
cases' Decidable.em (stationaryPoint hne' ≤ N) with hle hle
[GOAL]
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
[PROOFSTEP]
have := (stationaryPoint_spec hne' le_rfl hle).symm
[GOAL]
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this✝ : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
this :
  padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) (stationaryPoint hne')) =
    padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) N)
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
[PROOFSTEP]
simp only [const_apply, sub_apply, padicNorm.zero, sub_self] at this 
[GOAL]
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this✝ : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
this : padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) = 0
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
[PROOFSTEP]
simpa only [this]
[GOAL]
case inr.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ (m : ℕ), m ≥ N → ∀ (n : ℕ), n ≥ N → padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : ¬stationaryPoint hne' ≤ N
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε
[PROOFSTEP]
exact hN _ (lt_of_not_ge hle).le _ le_rfl
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
n : ℕ
⊢ 0 < ↑n + 1
[PROOFSTEP]
exact_mod_cast succ_pos _
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε
[PROOFSTEP]
refine' (exists_nat_gt (1 / ε)).imp fun N hN i hi ↦ _
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
⊢ ↑padicNormE (↑f i - ↑(limSeq f i)) < ε
[PROOFSTEP]
have h := Classical.choose_spec (rat_dense' (f i) (div_nat_pos i))
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ ↑padicNormE (↑f i - ↑(limSeq f i)) < ε
[PROOFSTEP]
refine' lt_of_lt_of_le h ((div_le_iff' <| by exact_mod_cast succ_pos _).mpr _)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 0 < ↑i + 1
[PROOFSTEP]
exact_mod_cast succ_pos _
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 1 ≤ (↑i + 1) * ε
[PROOFSTEP]
rw [right_distrib]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε + 1 * ε
[PROOFSTEP]
apply le_add_of_le_of_nonneg
[GOAL]
case hbc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 1 ≤ ↑i * ε
[PROOFSTEP]
exact (div_le_iff hε).mp (le_trans (le_of_lt hN) (by exact_mod_cast hi))
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ ↑N ≤ ↑i
[PROOFSTEP]
exact_mod_cast hi
[GOAL]
case ha
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 0 ≤ 1 * ε
[PROOFSTEP]
apply le_of_lt
[GOAL]
case ha.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : 0 < ε
N : ℕ
hN : 1 / ε < ↑N
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑f i - ↑(Classical.choose (_ : ∃ r, ↑padicNormE (↑f i - ↑r) < 1 / (↑i + 1)))) < 1 / (↑i + 1)
⊢ 0 < 1 * ε
[PROOFSTEP]
simpa
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → padicNorm p (limSeq f j - limSeq f i) < ε
[PROOFSTEP]
have hε3 : 0 < ε / 3 := div_pos hε (by norm_num)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
⊢ 0 < 3
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → padicNorm p (limSeq f j - limSeq f i) < ε
[PROOFSTEP]
let ⟨N, hN⟩ := exi_rat_seq_conv f hε3
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → padicNorm p (limSeq f j - limSeq f i) < ε
[PROOFSTEP]
let ⟨N2, hN2⟩ := f.cauchy₂ hε3
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → padicNorm p (limSeq f j - limSeq f i) < ε
[PROOFSTEP]
exists max N N2
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
⊢ ∀ (j : ℕ), j ≥ max N N2 → padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
[PROOFSTEP]
intro j hj
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
[PROOFSTEP]
suffices padicNormE (limSeq f j - f (max N N2) + (f (max N N2) - limSeq f (max N N2)) : ℚ_[p]) < ε
  by
  ring_nf at this ⊢
  rw [← padicNormE.eq_padic_norm']
  exact_mod_cast this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this : ↑padicNormE (↑(limSeq f j) - ↑f (max N N2) + (↑f (max N N2) - ↑(limSeq f (max N N2)))) < ε
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
[PROOFSTEP]
ring_nf at this ⊢
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this : ↑padicNormE (↑(limSeq f j) - ↑(limSeq f (max N N2))) < ε
⊢ padicNorm p (limSeq f j - limSeq f (max N N2)) < ε
[PROOFSTEP]
rw [← padicNormE.eq_padic_norm']
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this : ↑padicNormE (↑(limSeq f j) - ↑(limSeq f (max N N2))) < ε
⊢ ↑padicNormE ↑(limSeq f j - limSeq f (max N N2)) < ε
[PROOFSTEP]
exact_mod_cast this
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑(limSeq f j) - ↑f (max N N2) + (↑f (max N N2) - ↑(limSeq f (max N N2)))) < ε
[PROOFSTEP]
apply lt_of_le_of_lt
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑(limSeq f j) - ↑f (max N N2) + (↑f (max N N2) - ↑(limSeq f (max N N2)))) ≤ ?b
[PROOFSTEP]
apply padicNormE.add_le
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑(limSeq f j) - ↑f (max N N2)) + ↑padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) < ε
[PROOFSTEP]
rw [← add_thirds ε]
[GOAL]
case a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑(limSeq f j) - ↑f (max N N2)) + ↑padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) <
    ε / 3 + ε / 3 + ε / 3
[PROOFSTEP]
apply _root_.add_lt_add
[GOAL]
case a.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑(limSeq f j) - ↑f (max N N2)) < ε / 3 + ε / 3
[PROOFSTEP]
suffices padicNormE (limSeq f j - f j + (f j - f (max N N2)) : ℚ_[p]) < ε / 3 + ε / 3 by simpa only [sub_add_sub_cancel]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
this : ↑padicNormE (↑(limSeq f j) - ↑f j + (↑f j - ↑f (max N N2))) < ε / 3 + ε / 3
⊢ ↑padicNormE (↑(limSeq f j) - ↑f (max N N2)) < ε / 3 + ε / 3
[PROOFSTEP]
simpa only [sub_add_sub_cancel]
[GOAL]
case a.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑(limSeq f j) - ↑f j + (↑f j - ↑f (max N N2))) < ε / 3 + ε / 3
[PROOFSTEP]
apply lt_of_le_of_lt
[GOAL]
case a.h₁.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑(limSeq f j) - ↑f j + (↑f j - ↑f (max N N2))) ≤ ?a.h₁.b✝
[PROOFSTEP]
apply padicNormE.add_le
[GOAL]
case a.h₁.a
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑(limSeq f j) - ↑f j) + ↑padicNormE (↑f j - ↑f (max N N2)) < ε / 3 + ε / 3
[PROOFSTEP]
apply _root_.add_lt_add
[GOAL]
case a.h₁.a.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑(limSeq f j) - ↑f j) < ε / 3
[PROOFSTEP]
rw [padicNormE.map_sub]
[GOAL]
case a.h₁.a.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑f j - ↑(limSeq f j)) < ε / 3
[PROOFSTEP]
apply_mod_cast hN j
[GOAL]
case a.h₁.a.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ j ≥ N
[PROOFSTEP]
exact le_of_max_le_left hj
[GOAL]
case a.h₁.a.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑f j - ↑f (max N N2)) < ε / 3
[PROOFSTEP]
exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _)
[GOAL]
case a.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ ↑padicNormE (↑f (max N N2) - ↑(limSeq f (max N N2))) < ε / 3
[PROOFSTEP]
apply_mod_cast hN (max N N2)
[GOAL]
case a.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
hε3 : 0 < ε / 3
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 3
N2 : ℕ
hN2 : ∀ (j : ℕ), j ≥ N2 → ∀ (k : ℕ), k ≥ N2 → ↑padicNormE (↑f j - ↑f k) < ε / 3
j : ℕ
hj : j ≥ max N N2
⊢ max N N2 ≥ N
[PROOFSTEP]
apply le_max_left
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (Padic.lim f - ↑f i) < ε
[PROOFSTEP]
obtain ⟨N, hN⟩ := exi_rat_seq_conv f (half_pos hε)
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (Padic.lim f - ↑f i) < ε
[PROOFSTEP]
obtain ⟨N2, hN2⟩ := padicNormE.defn (lim' f) (half_pos hε)
[GOAL]
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (Padic.lim f - ↑f i) < ε
[PROOFSTEP]
refine' ⟨max N N2, fun i hi ↦ _⟩
[GOAL]
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑f i) < ε
[PROOFSTEP]
rw [← sub_add_sub_cancel _ (lim' f i : ℚ_[p]) _]
[GOAL]
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i) + (↑(↑(Padic.lim' f) i) - ↑f i)) < ε
[PROOFSTEP]
refine' (padicNormE.add_le _ _).trans_lt _
[GOAL]
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + ↑padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε
[PROOFSTEP]
rw [← add_halves ε]
[GOAL]
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) + ↑padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2 + ε / 2
[PROOFSTEP]
apply _root_.add_lt_add
[GOAL]
case intro.intro.h₁
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (Padic.lim f - ↑(↑(Padic.lim' f) i)) < ε / 2
[PROOFSTEP]
apply hN2 _ (le_of_max_le_right hi)
[GOAL]
case intro.intro.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (↑(↑(Padic.lim' f) i) - ↑f i) < ε / 2
[PROOFSTEP]
rw [padicNormE.map_sub]
[GOAL]
case intro.intro.h₂
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - ↑(limSeq f i)) < ε / 2
N2 : ℕ
hN2 : ∀ (i : ℕ), i ≥ N2 → ↑padicNormE (mk (Padic.lim' f) - ↑(↑(Padic.lim' f) i)) < ε / 2
i : ℕ
hi : i ≥ max N N2
⊢ ↑padicNormE (↑f i - ↑(↑(Padic.lim' f) i)) < ε / 2
[PROOFSTEP]
exact hN _ (le_of_max_le_left hi)
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
⊢ ∃ q, ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - q) < ε
[PROOFSTEP]
obtain ⟨x, hx⟩ := complete' f
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
⊢ ∃ q, ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - q) < ε
[PROOFSTEP]
refine ⟨x, fun ε hε => ?_⟩
[GOAL]
case intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - x) < ε
[PROOFSTEP]
obtain ⟨N, hN⟩ := hx ε hε
[GOAL]
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
⊢ ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑f i - x) < ε
[PROOFSTEP]
refine ⟨N, fun i hi => ?_⟩
[GOAL]
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ ↑padicNormE (↑f i - x) < ε
[PROOFSTEP]
rw [padicNormE.map_sub]
[GOAL]
case intro.intro
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] ↑padicNormE
x : ℚ_[p]
hx : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
ε : ℚ
hε : ε > 0
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (x - ↑f i) < ε
i : ℕ
hi : i ≥ N
⊢ ↑padicNormE (x - ↑f i) < ε
[PROOFSTEP]
exact hN i hi
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (x : ℚ_[p]), dist x x = 0
[PROOFSTEP]
simp [dist]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ dist x y = dist y x
[PROOFSTEP]
simp [dist, ← padicNormE.map_neg (x - y : ℚ_[p])]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y z : ℚ_[p]
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
dsimp [dist]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x y z : ℚ_[p]
⊢ ↑(↑padicNormE (x - z)) ≤ ↑(↑padicNormE (x - y)) + ↑(↑padicNormE (y - z))
[PROOFSTEP]
exact_mod_cast padicNormE.sub_le x y z
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (x y : ℚ_[p]),
    (fun x y => ↑{ val := ↑(↑padicNormE (x - y)), property := (_ : 0 ≤ ↑(↑padicNormE (x - y))) }) x y =
      ENNReal.ofReal (dist x y)
[PROOFSTEP]
intros
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ_[p]
⊢ (fun x y => ↑{ val := ↑(↑padicNormE (x - y)), property := (_ : 0 ≤ ↑(↑padicNormE (x - y))) }) x✝ y✝ =
    ENNReal.ofReal (dist x✝ y✝)
[PROOFSTEP]
exact (ENNReal.ofReal_eq_coe_nnreal _).symm
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ {x y : ℚ_[p]}, dist x y = 0 → x = y
[PROOFSTEP]
dsimp [dist]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ {x y : ℚ_[p]}, ↑(↑padicNormE (x - y)) = 0 → x = y
[PROOFSTEP]
intro _ _ h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ_[p]
h : ↑(↑padicNormE (x✝ - y✝)) = 0
⊢ x✝ = y✝
[PROOFSTEP]
apply eq_of_sub_eq_zero
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ_[p]
h : ↑(↑padicNormE (x✝ - y✝)) = 0
⊢ x✝ - y✝ = 0
[PROOFSTEP]
apply padicNormE.eq_zero.1
[GOAL]
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ y✝ : ℚ_[p]
h : ↑(↑padicNormE (x✝ - y✝)) = 0
⊢ ↑padicNormE (x✝ - y✝) = 0
[PROOFSTEP]
exact_mod_cast h
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
src✝¹ : Field ℚ_[p] := field
src✝ : MetricSpace ℚ_[p] := metricSpace p
⊢ ∀ (a b : ℚ_[p]), ‖a * b‖ = ‖a‖ * ‖b‖
[PROOFSTEP]
simp [Norm.norm, map_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (x y : ℚ_[p]), ‖x * y‖ = ‖x‖ * ‖y‖
[PROOFSTEP]
simp [Norm.norm, map_mul]
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'l : 0 < ↑ε'
hε'r : ↑ε' < ε
⊢ 0 < ε'
[PROOFSTEP]
simpa using hε'l
[GOAL]
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℝ
hε : 0 < ε
ε' : ℚ
hε'l : 0 < ↑ε'
hε'r : ↑ε' < ε
r : ℚ
hr : ↑padicNormE (q - ↑r) < ε'
⊢ ‖q - ↑r‖ < ↑ε'
[PROOFSTEP]
simpa [Norm.norm] using hr
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ‖q * r‖ = ‖q‖ * ‖r‖
[PROOFSTEP]
simp [Norm.norm, map_mul]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ‖q + r‖ ≤ max ‖q‖ ‖r‖
[PROOFSTEP]
dsimp [norm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ↑(↑padicNormE (q + r)) ≤ max ↑(↑padicNormE q) ↑(↑padicNormE r)
[PROOFSTEP]
exact_mod_cast nonarchimedean' _ _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ‖q‖ ≠ ‖r‖
⊢ ‖q + r‖ = max ‖q‖ ‖r‖
[PROOFSTEP]
dsimp [norm] at h ⊢
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(↑padicNormE q) = ↑(↑padicNormE r)
⊢ ↑(↑padicNormE (q + r)) = max ↑(↑padicNormE q) ↑(↑padicNormE r)
[PROOFSTEP]
have : padicNormE q ≠ padicNormE r := by exact_mod_cast h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(↑padicNormE q) = ↑(↑padicNormE r)
⊢ ↑padicNormE q ≠ ↑padicNormE r
[PROOFSTEP]
exact_mod_cast h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
h : ¬↑(↑padicNormE q) = ↑(↑padicNormE r)
this : ↑padicNormE q ≠ ↑padicNormE r
⊢ ↑(↑padicNormE (q + r)) = max ↑(↑padicNormE q) ↑(↑padicNormE r)
[PROOFSTEP]
exact_mod_cast add_eq_max_of_ne' this
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ ‖↑q‖ = ↑(padicNorm p q)
[PROOFSTEP]
dsimp [norm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ ↑(↑padicNormE ↑q) = ↑(padicNorm p q)
[PROOFSTEP]
rw [← padicNormE.eq_padic_norm']
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ = (↑p)⁻¹
[PROOFSTEP]
rw [← @Rat.cast_coe_nat ℝ _ p]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ = (↑↑p)⁻¹
[PROOFSTEP]
rw [← @Rat.cast_coe_nat ℚ_[p] _ p]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑↑p‖ = (↑↑p)⁻¹
[PROOFSTEP]
simp [hp.1.ne_zero, hp.1.ne_one, norm, padicNorm, padicValRat, padicValInt, zpow_neg, -Rat.cast_coe_nat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ‖↑p‖ < 1
[PROOFSTEP]
rw [norm_p]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (↑p)⁻¹ < 1
[PROOFSTEP]
apply inv_lt_one
[GOAL]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
⊢ ‖↑p ^ n‖ = ↑p ^ (-n)
[PROOFSTEP]
rw [norm_zpow, norm_p, zpow_neg, inv_zpow]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ‖↑p ^ n‖ = ↑p ^ (-↑n)
[PROOFSTEP]
rw [← norm_p_zpow, zpow_ofNat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
src✝ : NormedField ℚ_[p] := Padic.normedField p
⊢ 1 < ‖(↑p)⁻¹‖
[PROOFSTEP]
rw [norm_inv, norm_p, inv_inv]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
src✝ : NormedField ℚ_[p] := Padic.normedField p
⊢ 1 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk equiv f ≠ 0
this : ¬f ≈ 0
n : ℤ
hn : PadicSeq.norm f = ↑p ^ (-n)
⊢ ‖Quotient.mk equiv f‖ = ↑(↑p ^ (-n))
[PROOFSTEP]
rw [← hn]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk equiv f ≠ 0
this : ¬f ≈ 0
n : ℤ
hn : PadicSeq.norm f = ↑p ^ (-n)
⊢ ‖Quotient.mk equiv f‖ = ↑(PadicSeq.norm f)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ_[p]
h : q = 0
⊢ ‖q‖ = ↑0
[PROOFSTEP]
simp [h]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : n = 0
⊢ ‖↑(Rat.mk' n d)‖ ≤ 1
[PROOFSTEP]
have : (⟨n, d, hn, hd⟩ : ℚ) = 0 := Rat.zero_iff_num_zero.mpr hnz
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : n = 0
this : Rat.mk' n d = 0
⊢ ‖↑(Rat.mk' n d)‖ ≤ 1
[PROOFSTEP]
rw [this]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : n = 0
this : Rat.mk' n d = 0
⊢ ‖↑0‖ ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
⊢ ‖↑(Rat.mk' n d)‖ ≤ 1
[PROOFSTEP]
have hnz' : (⟨n, d, hn, hd⟩ : ℚ) ≠ 0 := mt Rat.zero_iff_num_zero.1 hnz
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ ‖↑(Rat.mk' n d)‖ ≤ 1
[PROOFSTEP]
rw [padicNormE.eq_padicNorm]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ ↑(padicNorm p (Rat.mk' n d)) ≤ 1
[PROOFSTEP]
norm_cast
  -- Porting note: `Nat.cast_zero` instead of another `norm_cast` call
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ padicNorm p (Rat.mk' n d) ≤ 1
[PROOFSTEP]
rw [padicNorm.eq_zpow_of_nonzero hnz', padicValRat, neg_sub, padicValNat.eq_zero_of_not_dvd hq, Nat.cast_zero, zero_sub,
  zpow_neg, zpow_ofNat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ (↑p ^ padicValInt p (Rat.mk' n d).num)⁻¹ ≤ 1
[PROOFSTEP]
apply inv_le_one
[GOAL]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ 1 ≤ ↑p ^ padicValInt p (Rat.mk' n d).num
[PROOFSTEP]
norm_cast
[GOAL]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ 1 ≤ p ^ padicValInt p (Rat.mk' n d).num
[PROOFSTEP]
apply one_le_pow
[GOAL]
case ha.h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℤ
d : ℕ
hn : d ≠ 0
hd : coprime (Int.natAbs n) d
hq : ¬p ∣ d
hnz : ¬n = 0
hnz' : Rat.mk' n d ≠ 0
⊢ 0 < p
[PROOFSTEP]
exact hp.1.pos
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
⊢ ¬p ∣ (↑z).den
[PROOFSTEP]
simp [hp.1.ne_one]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ
this : ‖↑↑z‖ ≤ 1
⊢ ‖↑z‖ ≤ 1
[PROOFSTEP]
simpa
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ‖↑k‖ < 1 ↔ ↑p ∣ k
[PROOFSTEP]
constructor
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ‖↑k‖ < 1 → ↑p ∣ k
[PROOFSTEP]
intro h
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ‖↑k‖ < 1
⊢ ↑p ∣ k
[PROOFSTEP]
contrapose! h
[GOAL]
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ 1 ≤ ‖↑k‖
[PROOFSTEP]
apply le_of_eq
[GOAL]
case mp.a
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ 1 = ‖↑k‖
[PROOFSTEP]
rw [eq_comm]
[GOAL]
case mp.a
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ ‖↑k‖ = 1
[PROOFSTEP]
calc
  ‖(k : ℚ_[p])‖ = ‖((k : ℚ) : ℚ_[p])‖ := by norm_cast
  _ = padicNorm p k := (padicNormE.eq_padicNorm _)
  _ = 1 := by exact_mod_cast (int_eq_one_iff k).mpr h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ ‖↑k‖ = ‖↑↑k‖
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ ↑(padicNorm p ↑k) = 1
[PROOFSTEP]
exact_mod_cast (int_eq_one_iff k).mpr h
[GOAL]
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ↑p ∣ k → ‖↑k‖ < 1
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑(↑p * x)‖ < 1
[PROOFSTEP]
push_cast
[GOAL]
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p * ↑x‖ < 1
[PROOFSTEP]
rw [padicNormE.mul]
[GOAL]
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p‖ * ‖↑x‖ < 1
[PROOFSTEP]
calc
  _ ≤ ‖(p : ℚ_[p])‖ * 1 := mul_le_mul le_rfl (by simpa using norm_int_le_one _) (norm_nonneg _) (norm_nonneg _)
  _ < 1 := by
    rw [mul_one, padicNormE.norm_p]
    apply inv_lt_one
    exact_mod_cast hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑x‖ ≤ 1
[PROOFSTEP]
simpa using norm_int_le_one _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p‖ * 1 < 1
[PROOFSTEP]
rw [mul_one, padicNormE.norm_p]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ (↑p)⁻¹ < 1
[PROOFSTEP]
apply inv_lt_one
[GOAL]
case ha
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ 1 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
[PROOFSTEP]
have : (p : ℝ) ^ (-n : ℤ) = (p : ℚ) ^ (-n : ℤ) := by simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
[PROOFSTEP]
rw [show (k : ℚ_[p]) = ((k : ℚ) : ℚ_[p]) by norm_cast, eq_padicNorm, this]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ ↑k = ↑↑k
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ ↑(padicNorm p ↑k) ≤ ↑(↑p ^ (-↑n)) ↔ ↑(p ^ n) ∣ k
[PROOFSTEP]
norm_cast
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑(↑p ^ (-↑n))
⊢ padicNorm p ↑k ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k
[PROOFSTEP]
rw [← padicNorm.dvd_iff_norm_le]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1 + z2‖ ≥ ‖z2‖
[PROOFSTEP]
rw [padicNormE.add_eq_max_of_ne hne]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z2‖
hne : ¬‖z1‖ = ‖z2‖
⊢ max ‖z1‖ ‖z2‖ ≥ ‖z2‖
[PROOFSTEP]
apply le_max_right
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1 + z2‖ ≥ ‖z1‖
[PROOFSTEP]
rw [padicNormE.add_eq_max_of_ne hne]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℚ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ max ‖z1‖ ‖z2‖ ≥ ‖z1‖
[PROOFSTEP]
apply le_max_left
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
⊢ ∃ b, f ≈ const norm b
[PROOFSTEP]
have cau_seq_norm_e : IsCauSeq padicNormE f := fun ε hε =>
  by
  have h := isCauSeq f ε (by exact_mod_cast hε)
  dsimp [norm] at h 
  exact_mod_cast h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ↑padicNormE (↑f j - ↑f i) < ε
[PROOFSTEP]
have h := isCauSeq f ε (by exact_mod_cast hε)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
⊢ ↑ε > 0
[PROOFSTEP]
exact_mod_cast hε
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
h : ∃ i, ∀ (j : ℕ), j ≥ i → ‖↑f j - ↑f i‖ < ↑ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ↑padicNormE (↑f j - ↑f i) < ε
[PROOFSTEP]
dsimp [norm] at h 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
ε : ℚ
hε : ε > 0
h : ∃ i, ∀ (j : ℕ), j ≥ i → ↑(↑padicNormE (↑f j - ↑f i)) < ↑ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ↑padicNormE (↑f j - ↑f i) < ε
[PROOFSTEP]
exact_mod_cast h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
⊢ ∃ b, f ≈ const norm b
[PROOFSTEP]
cases' Padic.complete'' ⟨f, cau_seq_norm_e⟩ with q hq
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
⊢ ∃ b, f ≈ const norm b
[PROOFSTEP]
exists q
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
⊢ f ≈ const norm q
[PROOFSTEP]
intro ε hε
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
ε : ℝ
hε : ε > 0
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖↑(f - const norm q) j‖ < ε
[PROOFSTEP]
cases' exists_rat_btwn hε with ε' hε'
[GOAL]
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ↑ε' ∧ ↑ε' < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖↑(f - const norm q) j‖ < ε
[PROOFSTEP]
norm_cast at hε' 
[GOAL]
case intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖↑(f - const norm q) j‖ < ε
[PROOFSTEP]
cases' hq ε' hε'.1 with N hN
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
⊢ ∃ i, ∀ (j : ℕ), j ≥ i → ‖↑(f - const norm q) j‖ < ε
[PROOFSTEP]
exists N
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
⊢ ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm q) j‖ < ε
[PROOFSTEP]
intro i hi
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
i : ℕ
hi : i ≥ N
⊢ ‖↑(f - const norm q) i‖ < ε
[PROOFSTEP]
have h := hN i hi
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
⊢ ‖↑(f - const norm q) i‖ < ε
[PROOFSTEP]
change norm (f i - q) < ε
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
⊢ ‖↑f i - q‖ < ε
[PROOFSTEP]
refine lt_trans ?_ hε'.2
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
⊢ ‖↑f i - q‖ < ↑ε'
[PROOFSTEP]
dsimp [norm]
[GOAL]
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ↑padicNormE ↑f
q : ℚ_[p]
hq : ∀ (ε : ℚ), ε > 0 → ∃ N, ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε
ε : ℝ
hε : ε > 0
ε' : ℚ
hε' : 0 < ε' ∧ ↑ε' < ε
N : ℕ
hN : ∀ (i : ℕ), i ≥ N → ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
i : ℕ
hi : i ≥ N
h : ↑padicNormE (↑{ val := ↑f, property := cau_seq_norm_e } i - q) < ε'
⊢ ↑(↑padicNormE (↑f i - q)) < ↑ε'
[PROOFSTEP]
exact_mod_cast h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
⊢ ‖CauSeq.lim f‖ ≤ a
[PROOFSTEP]
obtain ⟨N, hN⟩ := (CauSeq.equiv_lim f) _ ha
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ ‖CauSeq.lim f‖ ≤ a
[PROOFSTEP]
rw [← sub_add_cancel f.lim (f N)]
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ ‖CauSeq.lim f - ↑f N + ↑f N‖ ≤ a
[PROOFSTEP]
refine le_trans (padicNormE.nonarchimedean _ _) ?_
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ max ‖CauSeq.lim f - ↑f N‖ ‖↑f N‖ ≤ a
[PROOFSTEP]
rw [norm_sub_rev]
[GOAL]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
a : ℝ
ha : 0 < a
hf : ∀ (i : ℕ), ‖↑f i‖ ≤ a
N : ℕ
hN : ∀ (j : ℕ), j ≥ N → ‖↑(f - const norm (CauSeq.lim f)) j‖ < a
⊢ max ‖↑f N - CauSeq.lim f‖ ‖↑f N‖ ≤ a
[PROOFSTEP]
exact
  max_le (le_of_lt (hN _ le_rfl))
    (hf _)
      -- Porting note: the following nice `calc` block does not work
        -- exact calc
        --   ‖f.lim‖ = ‖f.lim - f N + f N‖ := sorry
        --   ‖f.lim - f N + f N‖ ≤ max ‖f.lim - f N‖ ‖f N‖ := sorry -- (padicNormE.nonarchimedean _ _)
        --   max ‖f.lim - f N‖ ‖f N‖ = max ‖f N - f.lim‖ ‖f N‖ := sorry -- by congr; rw [norm_sub_rev]
        --   max ‖f N - f.lim‖ ‖f N‖ ≤ a := sorry -- max_le (le_of_lt (hN _ le_rfl)) (hf _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ CompleteSpace ℚ_[p]
[PROOFSTEP]
apply complete_of_cauchySeq_tendsto
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (u : ℕ → ℚ_[p]), CauchySeq u → ∃ a, Tendsto u atTop (nhds a)
[PROOFSTEP]
intro u hu
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (nhds a)
[PROOFSTEP]
let c : CauSeq ℚ_[p] norm := ⟨u, Metric.cauchySeq_iff'.mp hu⟩
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
⊢ ∃ a, Tendsto u atTop (nhds a)
[PROOFSTEP]
refine' ⟨c.lim, fun s h ↦ _⟩
[GOAL]
case a
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℚ_[p]
h : s ∈ nhds (CauSeq.lim c)
⊢ s ∈ map u atTop
[PROOFSTEP]
rcases Metric.mem_nhds_iff.1 h with ⟨ε, ε0, hε⟩
[GOAL]
case a.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℚ_[p]
h : s ∈ nhds (CauSeq.lim c)
ε : ℝ
ε0 : ε > 0
hε : ball (CauSeq.lim c) ε ⊆ s
⊢ s ∈ map u atTop
[PROOFSTEP]
have := c.equiv_lim ε ε0
[GOAL]
case a.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℚ_[p]
h : s ∈ nhds (CauSeq.lim c)
ε : ℝ
ε0 : ε > 0
hε : ball (CauSeq.lim c) ε ⊆ s
this : ∃ i, ∀ (j : ℕ), j ≥ i → ‖↑(c - const norm (CauSeq.lim c)) j‖ < ε
⊢ s ∈ map u atTop
[PROOFSTEP]
simp only [mem_map, mem_atTop_sets, mem_setOf_eq]
[GOAL]
case a.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
hu : CauchySeq u
c : CauSeq ℚ_[p] norm := { val := u, property := (_ : ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → dist (u n) (u N) < ε) }
s : Set ℚ_[p]
h : s ∈ nhds (CauSeq.lim c)
ε : ℝ
ε0 : ε > 0
hε : ball (CauSeq.lim c) ε ⊆ s
this : ∃ i, ∀ (j : ℕ), j ≥ i → ‖↑(c - const norm (CauSeq.lim c)) j‖ < ε
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → b ∈ u ⁻¹' s
[PROOFSTEP]
exact this.imp fun N hN n hn ↦ hε (hN n hn)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
⊢ PadicSeq.valuation f = PadicSeq.valuation g
[PROOFSTEP]
by_cases hf : f ≈ 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : f ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g
[PROOFSTEP]
have hg : g ≈ 0 := Setoid.trans (Setoid.symm h) hf
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : f ≈ 0
hg : g ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g
[PROOFSTEP]
simp [hf, hg, PadicSeq.valuation]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g
[PROOFSTEP]
have hg : ¬g ≈ 0 := fun hg ↦ hf (Setoid.trans h hg)
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ PadicSeq.valuation f = PadicSeq.valuation g
[PROOFSTEP]
rw [PadicSeq.val_eq_iff_norm_eq hf hg]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
f g : CauSeq ℚ (padicNorm p)
h : f ≈ g
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ PadicSeq.norm f = PadicSeq.norm g
[PROOFSTEP]
exact PadicSeq.norm_equiv h
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation 1 = 0
[PROOFSTEP]
change dite (CauSeq.const (padicNorm p) 1 ≈ _) _ _ = _
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ (if h : const (padicNorm p) 1 ≈ 0 then (fun hf => 0) h
    else (fun hf => padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) h) =
    0
[PROOFSTEP]
have h : ¬CauSeq.const (padicNorm p) 1 ≈ 0 := by
  intro H
  erw [const_equiv p] at H 
  exact one_ne_zero H
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ ¬const (padicNorm p) 1 ≈ 0
[PROOFSTEP]
intro H
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
H : const (padicNorm p) 1 ≈ 0
⊢ False
[PROOFSTEP]
erw [const_equiv p] at H 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
H : 1 = 0
⊢ False
[PROOFSTEP]
exact one_ne_zero H
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
h : ¬const (padicNorm p) 1 ≈ 0
⊢ (if h : const (padicNorm p) 1 ≈ 0 then (fun hf => 0) h
    else (fun hf => padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) h) =
    0
[PROOFSTEP]
rw [dif_neg h]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
h : ¬const (padicNorm p) 1 ≈ 0
⊢ (fun hf => padicValRat p (↑(const (padicNorm p) 1) (PadicSeq.stationaryPoint hf))) h = 0
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x ≠ 0 → ‖x‖ = ↑p ^ (-valuation x)
[PROOFSTEP]
refine Quotient.inductionOn' x fun f hf => ?_
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ‖Quotient.mk'' f‖ = ↑p ^ (-valuation (Quotient.mk'' f))
[PROOFSTEP]
change (PadicSeq.norm _ : ℝ) = (p : ℝ) ^ (-PadicSeq.valuation _)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ↑(PadicSeq.norm f) = ↑p ^ (-PadicSeq.valuation f)
[PROOFSTEP]
rw [PadicSeq.norm_eq_pow_val]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ↑(↑p ^ (-PadicSeq.valuation f)) = ↑p ^ (-PadicSeq.valuation f)
p : ℕ hp : Fact (Nat.Prime p) x : ℚ_[p] f : CauSeq ℚ (padicNorm p) hf : Quotient.mk'' f ≠ 0 ⊢ ¬f ≈ 0
[PROOFSTEP]
change ↑((p : ℚ) ^ (-PadicSeq.valuation f)) = (p : ℝ) ^ (-PadicSeq.valuation f)
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ↑(↑p ^ (-PadicSeq.valuation f)) = ↑p ^ (-PadicSeq.valuation f)
[PROOFSTEP]
rw [Rat.cast_zpow, Rat.cast_coe_nat]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ¬f ≈ 0
[PROOFSTEP]
apply CauSeq.not_limZero_of_not_congr_zero
[GOAL]
case hf
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
⊢ ¬f - 0 ≈ 0
[PROOFSTEP]
intro hf'
[GOAL]
case hf
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
hf' : f - 0 ≈ 0
⊢ False
[PROOFSTEP]
apply hf
[GOAL]
case hf
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
hf' : f - 0 ≈ 0
⊢ Quotient.mk'' f = 0
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case hf.a
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
f : CauSeq ℚ (padicNorm p)
hf : Quotient.mk'' f ≠ 0
hf' : f - 0 ≈ 0
⊢ f ≈ const (padicNorm p) 0
[PROOFSTEP]
simpa using hf'
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ valuation ↑p = 1
[PROOFSTEP]
have h : (1 : ℝ) < p := by exact_mod_cast (Fact.out : p.Prime).one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ↑p
[PROOFSTEP]
exact_mod_cast (Fact.out : p.Prime).one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 < ↑p
⊢ valuation ↑p = 1
[PROOFSTEP]
refine' neg_injective ((zpow_strictMono h).injective <| (norm_eq_pow_val _).symm.trans _)
[GOAL]
case refine'_1
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 < ↑p
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast (Fact.out : p.Prime).ne_zero
[GOAL]
case refine'_2
p : ℕ
hp : Fact (Nat.Prime p)
h : 1 < ↑p
⊢ ‖↑p‖ = (fun x x_1 => x ^ x_1) (↑p) (-1)
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : x = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
[PROOFSTEP]
rw [hx, zero_add]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : x = 0
⊢ min (valuation 0) (valuation y) ≤ valuation y
[PROOFSTEP]
exact min_le_right _ _
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
[PROOFSTEP]
rw [hy, add_zero]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : y = 0
⊢ min (valuation x) (valuation 0) ≤ valuation x
[PROOFSTEP]
exact min_le_left _ _
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
[PROOFSTEP]
have h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := padicNormE.nonarchimedean x y
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
[PROOFSTEP]
have hp_one : (1 : ℝ) < p := by
  rw [← Nat.cast_one, Nat.cast_lt]
  exact Nat.Prime.one_lt hp.elim
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ 1 < ↑p
[PROOFSTEP]
rw [← Nat.cast_one, Nat.cast_lt]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
⊢ 1 < p
[PROOFSTEP]
exact Nat.Prime.one_lt hp.elim
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
hx : ¬x = 0
hy : ¬y = 0
h_norm : ‖x + y‖ ≤ max ‖x‖ ‖y‖
hp_one : 1 < ↑p
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
[PROOFSTEP]
rwa [norm_eq_pow_val hx, norm_eq_pow_val hy, norm_eq_pow_val hxy, zpow_le_max_iff_min_le hp_one] at h_norm 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ valuation (x * y) = valuation x + valuation y
[PROOFSTEP]
have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖ := norm_mul x y
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ valuation (x * y) = valuation x + valuation y
[PROOFSTEP]
have hp_ne_one : (p : ℝ) ≠ 1 := by
  rw [← Nat.cast_one, Ne.def, Nat.cast_inj]
  exact Nat.Prime.ne_one hp.elim
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ ↑p ≠ 1
[PROOFSTEP]
rw [← Nat.cast_one, Ne.def, Nat.cast_inj]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ ¬p = 1
[PROOFSTEP]
exact Nat.Prime.ne_one hp.elim
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ valuation (x * y) = valuation x + valuation y
[PROOFSTEP]
have hp_pos : (0 : ℝ) < p := by
  rw [← Nat.cast_zero, Nat.cast_lt]
  exact Nat.Prime.pos hp.elim
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ 0 < ↑p
[PROOFSTEP]
rw [← Nat.cast_zero, Nat.cast_lt]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ 0 < p
[PROOFSTEP]
exact Nat.Prime.pos hp.elim
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ valuation (x * y) = valuation x + valuation y
[PROOFSTEP]
rw [norm_eq_pow_val hx, norm_eq_pow_val hy, norm_eq_pow_val (mul_ne_zero hx hy), ← zpow_add₀ (ne_of_gt hp_pos),
  zpow_inj hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm 
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : valuation (x * y) = valuation x + valuation y
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ valuation (x * y) = valuation x + valuation y
[PROOFSTEP]
exact h_norm
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ addValuationDef 0 = ⊤
[PROOFSTEP]
rw [addValuationDef, if_pos (Eq.refl _)]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
⊢ addValuationDef 1 = 0
[PROOFSTEP]
rw [addValuationDef, if_neg one_ne_zero, valuation_one, WithTop.coe_zero]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ addValuationDef (x * y) = addValuationDef x + addValuationDef y
[PROOFSTEP]
simp only [addValuationDef]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
[PROOFSTEP]
rw [hx, if_pos (Eq.refl _), zero_mul, if_pos (Eq.refl _), WithTop.top_add]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
[PROOFSTEP]
rw [hy, if_pos (Eq.refl _), mul_zero, if_pos (Eq.refl _), WithTop.add_top]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then ⊤ else ↑(valuation (x * y))) =
    (if x = 0 then ⊤ else ↑(valuation x)) + if y = 0 then ⊤ else ↑(valuation y)
[PROOFSTEP]
rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe, valuation_map_mul hx hy]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ min (addValuationDef x) (addValuationDef y) ≤ addValuationDef (x + y)
[PROOFSTEP]
simp only [addValuationDef]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
[PROOFSTEP]
by_cases hxy : x + y = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
[PROOFSTEP]
rw [hxy, if_pos (Eq.refl _)]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
[PROOFSTEP]
rw [hx, if_pos (Eq.refl _), min_eq_right, zero_add]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : x = 0
⊢ (if y = 0 then ⊤ else ↑(valuation y)) ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
[PROOFSTEP]
rw [hy, if_pos (Eq.refl _), min_eq_left, add_zero]
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ (if x = 0 then ⊤ else ↑(valuation x)) ≤ ⊤
[PROOFSTEP]
exact le_top
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (if x = 0 then ⊤ else ↑(valuation x)) (if y = 0 then ⊤ else ↑(valuation y)) ≤
    if x + y = 0 then ⊤ else ↑(valuation (x + y))
[PROOFSTEP]
rw [if_neg hx, if_neg hy, if_neg hxy, ← WithTop.coe_min, WithTop.coe_le_coe]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ min (valuation x) (valuation y) ≤ valuation (x + y)
[PROOFSTEP]
exact valuation_map_add hxy
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ ↑addValuation x = ↑(valuation x)
[PROOFSTEP]
simp only [Padic.addValuation, AddValuation.of_apply, addValuationDef, if_neg hx]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
[PROOFSTEP]
have aux : ∀ n : ℤ, 0 < ((p : ℝ) ^ n) := by
  apply Nat.zpow_pos_of_pos
  exact hp.1.pos
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ∀ (n : ℤ), 0 < ↑p ^ n
[PROOFSTEP]
apply Nat.zpow_pos_of_pos
[GOAL]
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ 0 < p
[PROOFSTEP]
exact hp.1.pos
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
[PROOFSTEP]
by_cases hx0 : x = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
[PROOFSTEP]
simp [hx0, norm_zero, aux, le_of_lt (aux _)]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ‖x‖ ≤ ↑p ^ n ↔ ‖x‖ < ↑p ^ (n + 1)
[PROOFSTEP]
rw [norm_eq_pow_val hx0]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ n ↔ ↑p ^ (-valuation x) < ↑p ^ (n + 1)
[PROOFSTEP]
have h1p : 1 < (p : ℝ) := by exact_mod_cast hp.1.one_lt
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
⊢ 1 < ↑p
[PROOFSTEP]
exact_mod_cast hp.1.one_lt
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
h1p : 1 < ↑p
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ n ↔ ↑p ^ (-valuation x) < ↑p ^ (n + 1)
[PROOFSTEP]
have H := zpow_strictMono h1p
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
aux : ∀ (n : ℤ), 0 < ↑p ^ n
hx0 : ¬x = 0
h1p : 1 < ↑p
H : StrictMono ((fun x x_1 => x ^ x_1) ↑p)
⊢ ↑p ^ (-valuation x) ≤ ↑p ^ n ↔ ↑p ^ (-valuation x) < ↑p ^ (n + 1)
[PROOFSTEP]
rw [H.le_iff_le, H.lt_iff_lt, Int.lt_add_one_iff]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
n : ℤ
⊢ ‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)
[PROOFSTEP]
rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ valuation x
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ valuation x
[PROOFSTEP]
simp only [hx, norm_zero, valuation_zero, zero_le_one, le_refl]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ valuation x
[PROOFSTEP]
rw [norm_eq_pow_val hx, ← zpow_zero (p : ℝ), zpow_le_iff_le, Right.neg_nonpos_iff]
[GOAL]
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ 1 < ↑p
[PROOFSTEP]
exact Nat.one_lt_cast.2 (Nat.Prime.one_lt' p).1
