Theorem: LSeries_eq_zero_iff (EulerProducts/LSeriesUnique.lean)

State before:
f : ℕ → ℂ
hf : f 0 = 0
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤
Tactic:
by_cases h : abscissaOfAbsConv f = ⊤ <;> simp only [h, or_true, or_false, iff_true]
State after:
case pos
f : ℕ → ℂ
hf : f 0 = 0
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0

case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0

State before:
case pos
f : ℕ → ℂ
hf : f 0 = 0
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0
Tactic:
exact LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h
State after:
no goals

State before:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0
Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H ▸ LSeries_zero⟩
State after:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0

State before:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0
Tactic:
convert (LSeries_eventually_eq_zero_iff'.mp ?_).resolve_right h
State after:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0

case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] 0

State before:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ f = 0 ↔ ∀ (n : ℕ), n ≠ 0 → f n = 0
Tactic:
refine ⟨fun H' _ _ ↦ by rw [H', Pi.zero_apply], fun H' ↦ ?_⟩
State after:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f = 0

State before:
case a
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f = 0
Tactic:
ext ⟨- | m⟩
State after:
case a.h.zero
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f 0 = 0 0

case a.h.succ
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
n✝ : ℕ
⊢ f (n✝ + 1) = 0 (n✝ + 1)

State before:
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : f = 0
x✝¹ : ℕ
x✝ : x✝¹ ≠ 0
⊢ f x✝¹ = 0
Tactic:
rw [H', Pi.zero_apply]
State after:
no goals

State before:
case a.h.zero
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f 0 = 0 0
Tactic:
simp only [zero_eq, hf, Pi.zero_apply]
State after:
no goals

State before:
case a.h.succ
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
n✝ : ℕ
⊢ f (n✝ + 1) = 0 (n✝ + 1)
Tactic:
simp only [ne_eq, succ_ne_zero, not_false_eq_true, H', Pi.zero_apply]
State after:
no goals

State before:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] 0
Tactic:
simp only [H, Pi.zero_apply]
State after:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ (fun x => 0) =ᶠ[Filter.atTop] 0

State before:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
⊢ (fun x => 0) =ᶠ[Filter.atTop] 0
Tactic:
exact Filter.EventuallyEq.rfl
State after:
no goals