-- Mathlib/NumberTheory/LSeries/Basic.lean
/-- If `f` and `g` agree on large `n : ℕ` and the `LSeries` of `f` converges at `s`,
then so does that of `g`. -/
lemma LSeriesSummable.congr' {f g : ℕ → ℂ} (s : ℂ) (h : f =ᶠ[atTop] g) (hf : LSeriesSummable f s) :
    LSeriesSummable g s

Proof state:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖

Tactic:
have : term f s =ᶠ[cofinite] term g s := by
  rw [eventuallyEq_iff_exists_mem] at h ⊢
  obtain ⟨S, hS, hS'⟩ := h
  refine ⟨S \ {0}, diff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩
  rw [Set.mem_diff, Set.mem_singleton_iff] at hn
  simp [hn.2, hS' hn.1]

Result:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
this : term f s =ᶠ[cofinite] term g s
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖

Proof state:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
this : term f s =ᶠ[cofinite] term g s
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖

Tactic:
exact this.symm.mono fun n hn ↦ by simp [hn]

Result:
no goals

Proof state:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ LSeriesSummable g s

Tactic:
refine (summable_norm_iff.mpr hf).of_norm_bounded_eventually _ ?_

Result:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ ∀ᶠ (i : ℕ) in cofinite, ‖term g s i‖ ≤ ‖term f s i‖

Proof state:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
this : term f s =ᶠ[cofinite] term g s
n : ℕ
hn : term g s n = term f s n
⊢ ‖term g s n‖ ≤ ‖term f s n‖

Tactic:
simp [hn]

Result:
no goals

Proof state:
f g : ℕ → ℂ
s : ℂ
h : ∃ s ∈ cofinite, Set.EqOn f g s
hf : LSeriesSummable f s
⊢ ∃ s_1 ∈ cofinite, Set.EqOn (term f s) (term g s) s_1

Tactic:
obtain ⟨S, hS, hS'⟩ := h

Result:
case intro.intro
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : S ∈ cofinite
hS' : Set.EqOn f g S
⊢ ∃ s_1 ∈ cofinite, Set.EqOn (term f s) (term g s) s_1

Proof state:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[atTop] g
hf : LSeriesSummable f s
⊢ LSeriesSummable g s

Tactic:
rw [← Nat.cofinite_eq_atTop] at h

Result:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ LSeriesSummable g s

Proof state:
case intro.intro
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : S ∈ cofinite
hS' : Set.EqOn f g S
n : ℕ
hn : n ∈ S \ {0}
⊢ term f s n = term g s n

Tactic:
rw [Set.mem_diff, Set.mem_singleton_iff] at hn

Result:
case intro.intro
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : S ∈ cofinite
hS' : Set.EqOn f g S
n : ℕ
hn : n ∈ S ∧ ¬n = 0
⊢ term f s n = term g s n

Proof state:
f g : ℕ → ℂ
s : ℂ
h : f =ᶠ[cofinite] g
hf : LSeriesSummable f s
⊢ term f s =ᶠ[cofinite] term g s

Tactic:
rw [eventuallyEq_iff_exists_mem] at h ⊢

Result:
f g : ℕ → ℂ
s : ℂ
h : ∃ s ∈ cofinite, Set.EqOn f g s
hf : LSeriesSummable f s
⊢ ∃ s_1 ∈ cofinite, Set.EqOn (term f s) (term g s) s_1

Proof state:
case intro.intro
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : S ∈ cofinite
hS' : Set.EqOn f g S
⊢ ∃ s_1 ∈ cofinite, Set.EqOn (term f s) (term g s) s_1

Tactic:
refine ⟨S \ {0}, diff_mem hS <| (Set.finite_singleton 0).compl_mem_cofinite, fun n hn ↦ ?_⟩

Result:
case intro.intro
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : S ∈ cofinite
hS' : Set.EqOn f g S
n : ℕ
hn : n ∈ S \ {0}
⊢ term f s n = term g s n

Proof state:
case intro.intro
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
S : Set ℕ
hS : S ∈ cofinite
hS' : Set.EqOn f g S
n : ℕ
hn : n ∈ S ∧ ¬n = 0
⊢ term f s n = term g s n

Tactic:
simp [hn.2, hS' hn.1]

Result:
no goals