Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: case e'_2.e'_4
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x = ↑(x - 1) + 1

pp: case e'_2.e'_5
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x = ↑(x - 1) + 1

pp: case e'_3.e'_3.e'_4
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x - 1 = ↑(x - 1)

pp: case e'_3.e'_3.e'_5
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x - 1 = ↑(x - 1)

pp: case e'_3.e'_4.e'_4
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x = ↑(x - 1) + 1

pp: case e'_3.e'_4.e'_5
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x = ↑(x - 1) + 1

Tactic:
<;>

Goal state after:
case e'_2.e'_4
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x = ↑(x - 1) + 1

case e'_2.e'_5
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x = ↑(x - 1) + 1

case e'_3.e'_3.e'_4
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x - 1 = ↑(x - 1)

case e'_3.e'_3.e'_5
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x - 1 = ↑(x - 1)

case e'_3.e'_4.e'_4
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x = ↑(x - 1) + 1

case e'_3.e'_4.e'_5
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℕ
hx : 1 ≤ ↑x
⊢ ↑x = ↑(x - 1) + 1