Theorem: Finset.sum_Ioc_add_sum_Ioc (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ ∑ n ∈ Ioc a b, f n + ∑ n ∈ Ioc b c, f n = ∑ n ∈ Ioc a c, f n
Tactic:
convert Finset.sum_sdiff (s₁ := Finset.Ioc b c) (s₂ := Finset.Ioc a c) ?_
State after:
case h.e'_2.h.e'_5.h
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ Ioc a b = Ioc a c \ Ioc b c

case convert_4
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ Ioc b c ⊆ Ioc a c

State before:
case h.e'_2.h.e'_5.h
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ Ioc a b = Ioc a c \ Ioc b c
Tactic:
exact Finset.Ioc_diff_Ioc hb
State after:
no goals

State before:
case convert_4
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ Ioc b c ⊆ Ioc a c
Tactic:
exact Finset.Ioc_subset_Ioc (mem_Icc.mp hb).1 (by rfl)
State after:
no goals

State before:
a b c : ℤ
f : ℤ → ℂ
hb : b ∈ Icc a c
⊢ c ≤ c
Tactic:
rfl
State after:
no goals