case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ norm f = 0 → f ≈ 0

case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ f ≈ 0 → norm f = 0
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ norm f = 0 ↔ f ≈ 0
constructor
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : norm f = 0
⊢ f ≈ 0
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ norm f = 0 → f ≈ 0
intro h
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : norm f = 0
hf : ¬f ≈ 0
⊢ False
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : norm f = 0
⊢ f ≈ 0
by_contra hf
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
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : norm f = 0
hf : ¬f ≈ 0
⊢ False
unfold norm at h
case mp.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h✝ : f ≈ 0
h : 0 = 0
⊢ False

case mp.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
⊢ False
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
split_ifs at h
case mp.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
⊢ False
case mp.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h✝ : f ≈ 0
h : 0 = 0
⊢ False

case mp.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
⊢ False
contradiction
case mp.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
⊢ f ≈ 0
case mp.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
⊢ False
apply hf
case mp.inr
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) < ε
case mp.inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf h✝ : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint h✝)) = 0
⊢ f ≈ 0
intro ε hε
case mp.inr
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) < ε
case mp.inr
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) < ε
exists stationaryPoint hf
case mp.inr
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) < ε
case mp.inr
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) < ε
intro j hj
case mp.inr
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) < ε
case mp.inr
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) < ε
have heq := stationaryPoint_spec hf le_rfl hj
no goals
case mp.inr
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) < ε
simpa [h, heq]
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : f ≈ 0
⊢ norm f = 0
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ f ≈ 0 → norm f = 0
intro h
no goals
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : f ≈ 0
⊢ norm f = 0
simp [norm, h]