-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_zero_iff (f : PadicSeq p) : f.norm = 0 ↔ f ≈ 0

Proof state:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
⊢ f ≈ 0

Tactic:
intro ε hε

Result:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(f - 0) j) < ε

Proof state:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
⊢ False

Tactic:
apply hf

Result:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
⊢ f ≈ 0

Proof state:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : f.norm = 0
hf : ¬f ≈ 0
⊢ False

Tactic:
unfold norm at h

Result:
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

Proof state:
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : f ≈ 0
⊢ f.norm = 0

Tactic:
simp [norm, h]

Result:
no goals

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

Tactic:
by_contra hf

Result:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : f.norm = 0
hf : ¬f ≈ 0
⊢ False

Proof state:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
j : ℕ
hj : j ≥ stationaryPoint hf
heq : padicNorm p (↑f j) = padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑(f - 0) j) < ε

Tactic:
simpa [h, heq]

Result:
no goals

Proof state:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
⊢ ∀ j ≥ stationaryPoint hf, padicNorm p (↑(f - 0) j) < ε

Tactic:
intro j hj

Result:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
j : ℕ
hj : j ≥ stationaryPoint hf
⊢ padicNorm p (↑(f - 0) j) < ε

Proof state:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑(f - 0) j) < ε

Tactic:
exists stationaryPoint hf

Result:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
⊢ ∀ j ≥ stationaryPoint hf, padicNorm p (↑(f - 0) j) < ε

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
⊢ f.norm = 0 ↔ f ≈ 0

Tactic:
constructor

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

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

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

Tactic:
intro h

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

Proof state:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
j : ℕ
hj : j ≥ stationaryPoint hf
⊢ padicNorm p (↑(f - 0) j) < ε

Tactic:
have heq := stationaryPoint_spec hf le_rfl hj

Result:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
ε : ℚ
hε : ε > 0
j : ℕ
hj : j ≥ stationaryPoint hf
heq : padicNorm p (↑f j) = padicNorm p (↑f (stationaryPoint hf))
⊢ padicNorm p (↑(f - 0) j) < ε

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

Tactic:
intro h

Result:
case mpr
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
h : f ≈ 0
⊢ f.norm = 0

Proof state:
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

Tactic:
split_ifs at h

Result:
case mp
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
h : padicNorm p (↑f (stationaryPoint hf)) = 0
⊢ False