awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h :
  (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) ↔
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
⊢ Membership.mem (γ := Filter (Finset ℤ)) (Filter.map (fun (g : ℤ) ↦ Icc (-g) g) atTop) s ↔
    Membership.mem (γ := Filter (Finset ℤ)) (Filter.map (fun (g : ℤ) ↦ Ioo (-g) g) atTop) s

Tactic:
simp only [← Nat.map_cast_int_atTop, Filter.map_map, Filter.mem_map, mem_atTop_sets, ge_iff_le,
    Set.mem_preimage, comp_apply]

Premises used: ge_iff_le, Filter.mem_atTop_sets, Filter.map_map, Function.comp_apply, Nat.map_cast_int_atTop, Filter.mem_map, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
⊢ (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) ↔
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s

Tactic:
⟨fun ⟨a, ha⟩ ↦ ⟨a + 1, fun b hb ↦ ?_⟩, fun ⟨a, ha⟩ ↦ ⟨a - 1, fun b hb ↦ ?_⟩⟩

Premises used: HSub.hSub, Exists, _private.0.SummationFilter.symmetricIcc_eq_symmetricIoo_int.match_5, HAdd.hAdd, _private.0.SummationFilter.symmetricIcc_eq_symmetricIoo_int.match_4, Iff.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h :
  (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) →
    ∀ (a : ℕ) (ha : ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) (b : ℕ) (hb : a + 1 ≤ b),
      Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
h₁ :
  (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s) →
    ∀ (a : ℕ) (ha : ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s) (b : ℕ) (hb : a - 1 ≤ b),
      Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s
⊢ (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) ↔
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s

Tactic:
refine ⟨fun ⟨a, ha⟩ ↦ ⟨a + 1, fun b hb ↦ ?_⟩, fun ⟨a, ha⟩ ↦ ⟨a - 1, fun b hb ↦ ?_⟩⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s
b : ℕ
hb : a + 1 ≤ b
⊢ a ≤ b - 1

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h_1 : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s
b : ℕ
hb : a + 1 ≤ b
h : Eq (α := Finset ℤ) (Ioo (-(↑b : ℤ)) (↑b : ℤ)) (Icc (-(↑(b - 1) : ℤ)) (↑(b - 1) : ℤ))
⊢ Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s

Tactic:
convert! ha (b - 1) (by grind) using 1

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
b : ℕ
hb : a - 1 ≤ b
⊢ a ≤ b + 1

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h_1 : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
b : ℕ
hb : a - 1 ≤ b
h : Eq (α := Finset ℤ) (Icc (-(↑b : ℤ)) (↑b : ℤ)) (Ioo (-(↑(b + 1) : ℤ)) (↑(b + 1) : ℤ))
⊢ Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s

Tactic:
convert! ha (b + 1) (by grind) using 1

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h :
  (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) →
    ∀ (a : ℕ) (ha : ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) (b : ℕ) (hb : a + 1 ≤ b),
      Eq (α := Finset ℤ) (Ioo (-(↑b : ℤ)) (↑b : ℤ)) (Icc (-(↑(b - 1) : ℤ)) (↑(b - 1) : ℤ))
h₁ :
  (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s) →
    ∀ (a : ℕ) (ha : ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s) (b : ℕ) (hb : a - 1 ≤ b),
      Eq (α := Finset ℤ) (Icc (-(↑b : ℤ)) (↑b : ℤ)) (Ioo (-(↑(b + 1) : ℤ)) (↑(b + 1) : ℤ))
⊢ (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) ↔
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s

Tactic:
refine ⟨fun ⟨a, ha⟩ ↦ ⟨a + 1, fun b hb ↦ ?_⟩, fun ⟨a, ha⟩ ↦ ⟨a - 1, fun b hb ↦ ?_⟩⟩ <;>
  [convert! ha (b - 1) (by grind) using 1; convert! ha (b + 1) (by grind) using 1]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h_1 : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s
b : ℕ
hb : a + 1 ≤ b
h : ∀ (a : ℤ), -(↑b : ℤ) < a ∧ a < (↑b : ℤ) ↔ -(↑(b - 1) : ℤ) ≤ a ∧ a ≤ (↑(b - 1) : ℤ)
⊢ Eq (α := Finset ℤ) (Ioo (-(↑b : ℤ)) (↑b : ℤ)) (Icc (-(↑(b - 1) : ℤ)) (↑(b - 1) : ℤ))

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h_1 : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
b : ℕ
hb : a - 1 ≤ b
h : ∀ (a : ℤ), -(↑b : ℤ) ≤ a ∧ a ≤ (↑b : ℤ) ↔ -1 < a + (↑b : ℤ) ∧ a < HAdd.hAdd (α := ℤ) (↑b : ℤ) 1
⊢ Eq (α := Finset ℤ) (Icc (-(↑b : ℤ)) (↑b : ℤ)) (Ioo (-(↑(b + 1) : ℤ)) (↑(b + 1) : ℤ))

Tactic:
simp [Finset.ext_iff]

Premises used: Finset.ext_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s
b : ℕ
hb : a + 1 ≤ b
⊢ ∀ (a : ℤ), -(↑b : ℤ) < a ∧ a < (↑b : ℤ) ↔ -(↑(b - 1) : ℤ) ≤ a ∧ a ≤ (↑(b - 1) : ℤ)

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
s : Set (Finset ℤ)
h : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
b : ℕ
hb : a - 1 ≤ b
⊢ ∀ (a : ℤ), -(↑b : ℤ) ≤ a ∧ a ≤ (↑b : ℤ) ↔ -1 < a + (↑b : ℤ) ∧ a < HAdd.hAdd (α := ℤ) (↑b : ℤ) 1

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
α : Type u_1
f : ℤ → α
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
a : α
hf : HasProd f a (symmetricIcc ℤ)
hf2 : Tendsto.{0, u_1} (β := α) (fun (N : ℕ) ↦ (f (↑N : ℤ))⁻¹) atTop (𝓝 1)
simp :
  ∀ (hf : Tendsto (α := ℕ) ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℕ) ↦ Icc (-(↑N : ℤ)) (↑N : ℤ)) atTop (𝓝 a)),
    Tendsto (comp (β := ℤ) ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℤ) ↦ Ico (-N) N) Nat.cast) atTop (𝓝 a)
⊢ HasProd f a (symmetricIco ℤ)

Tactic:
simp only [HasProd, tendsto_map'_iff, symmetricIcc_eq_map_Icc_nat,
    ← Nat.map_cast_int_atTop, symmetricIco] at *

Premises used: SummationFilter.symmetricIco, Filter.tendsto_map'_iff, HasProd, Nat.map_cast_int_atTop, SummationFilter.symmetricIcc_eq_map_Icc_nat, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
α : Type u_1
f : ℤ → α
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
a : α
hf2 : Tendsto.{0, u_1} (β := α) (fun (N : ℕ) ↦ (f (↑N : ℤ))⁻¹) atTop (𝓝 1)
hf : Tendsto (α := ℕ) ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℕ) ↦ Icc (-(↑N : ℤ)) (↑N : ℤ)) atTop (𝓝 a)
apply :
  Tendsto
    (HDiv.hDiv (α := ℕ → α) (comp (β := ℤ) ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℤ) ↦ Ico (-N) N) Nat.cast)
      ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℕ) ↦ Icc (-(↑N : ℤ)) (↑N : ℤ)))
    atTop (𝓝 1)
⊢ Tendsto (comp (β := ℤ) ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℤ) ↦ Ico (-N) N) Nat.cast) atTop (𝓝 a)

Tactic:
apply tendsto_of_div_tendsto_one _ hf

Premises used: Filter.tendsto_of_div_tendsto_one
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
α : Type u_1
f : ℤ → α
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
a : α
hf2 : Tendsto.{0, u_1} (β := α) (fun (N : ℕ) ↦ (f (↑N : ℤ))⁻¹) atTop (𝓝 1)
hf : Tendsto (α := ℕ) ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℕ) ↦ Icc (-(↑N : ℤ)) (↑N : ℤ)) atTop (𝓝 a)
N : ℕ
⊢ LE.le (α := ℤ) (-(↑N : ℤ)) (↑N : ℤ)

Tactic:
lia
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
α : Type u_1
f : ℤ → α
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
a : α
hf2 : Tendsto.{0, u_1} (β := α) (fun (N : ℕ) ↦ (f (↑N : ℤ))⁻¹) atTop (𝓝 1)
hf : Tendsto (α := ℕ) ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℕ) ↦ Icc (-(↑N : ℤ)) (↑N : ℤ)) atTop (𝓝 a)
⊢ Tendsto
    (HDiv.hDiv (α := ℕ → α) (comp (β := ℤ) ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℤ) ↦ Ico (-N) N) Nat.cast)
      ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℕ) ↦ Icc (-(↑N : ℤ)) (↑N : ℤ)))
    atTop (𝓝 1)

Tactic:
simpa [Pi.div_def, fun N : ℕ ↦ prod_Icc_eq_prod_Ico_mul f (show (-N : ℤ) ≤ N by lia)]
    using hf2

Premises used: Pi.div_def, Finset.prod_Icc_eq_prod_Ico_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
α : Type u_1
f : ℤ → α
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
hf : Multipliable f (symmetricIcc ℤ)
hf2 : Tendsto.{0, u_1} (β := α) (fun (N : ℕ) ↦ (f (↑N : ℤ))⁻¹) atTop (𝓝 1)
⊢ Multipliable f (symmetricIco ℤ)

Tactic:
(hf.hasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc hf2).multipliable

Premises used: Multipliable.hasProd, HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
α : Type u_1
f : ℤ → α
inst : CommGroup α
inst_1 : TopologicalSpace α
inst_2 : ContinuousMul α
inst_3 : T2Space α
hf : Multipliable f (symmetricIcc ℤ)
hf2 : Tendsto.{0, u_1} (β := α) (fun (N : ℕ) ↦ (f (↑N : ℤ))⁻¹) atTop (𝓝 1)
⊢ Eq.{u_1 + 1} (α := α) (∏'[symmetricIco ℤ] (b : ℤ), f b) (∏'[symmetricIcc ℤ] (b : ℤ), f b)

Tactic:
(hf.hasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc hf2).tprod_eq

Premises used: HasProd.tprod_eq, Multipliable.hasProd, HasProd.hasProd_symmetricIco_of_hasProd_symmetricIcc
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : ℤ → α
a : α
⊢ HasProd f a (symmetricIcc ℤ) ↔ Tendsto (fun (N : ℕ) ↦ ∏ n ∈ Icc (-(↑N : ℤ)) (↑N : ℤ), f n) atTop (𝓝 a)

Tactic:
simp [HasProd, symmetricIcc, ← Nat.map_cast_int_atTop, comp_def]

Premises used: SummationFilter.symmetricIcc, HasProd, Function.comp_def, Nat.map_cast_int_atTop, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : ℤ → α
a : α
⊢ HasProd f a (symmetricIco ℤ) ↔ Tendsto (fun (N : ℕ) ↦ ∏ n ∈ Ico (-(↑N : ℤ)) (↑N : ℤ), f n) atTop (𝓝 a)

Tactic:
simp [HasProd, symmetricIco, ← Nat.map_cast_int_atTop, comp_def]

Premises used: SummationFilter.symmetricIco, HasProd, Function.comp_def, Nat.map_cast_int_atTop, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : ℤ → α
a : α
⊢ HasProd f a (symmetricIoc ℤ) ↔ Tendsto (fun (N : ℕ) ↦ ∏ n ∈ Ioc (-(↑N : ℤ)) (↑N : ℤ), f n) atTop (𝓝 a)

Tactic:
simp [HasProd, symmetricIoc, ← Nat.map_cast_int_atTop, comp_def]

Premises used: HasProd, Function.comp_def, Nat.map_cast_int_atTop, SummationFilter.symmetricIoc, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hf : Summable f (symmetricIcc ℤ)
hs : Function.Even f
rw : Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖f x‖) atTop (𝓝 0)
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hf : Summable f (symmetricIcc ℤ)
hs : Function.Even f
obtain : ∀ (L : F) (hL : HasSum f L (symmetricIcc ℤ)), Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖f x‖) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖f x‖) atTop (𝓝 0)

Tactic:
obtain ⟨L, hL⟩ := hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : HasSum f L (symmetricIcc ℤ)
⊢ Tendsto (fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)

Tactic:
rw [HasSum, symmetricIcc_filter, tendsto_map'_iff, Function.comp_def] at hL

Premises used: Filter.tendsto_map'_iff, Function.comp_def, HasSum, SummationFilter.symmetricIcc_filter, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
⊢ Tendsto
    (fun (x : ℤ) ↦
      HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (((fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) ∘ fun (x : ℤ) ↦ id x + -1) x))
    atTop (𝓝 (L - L))

Tactic:
have := hL.sub (hL.comp (tendsto_atTop_add_const_right _ (-1) tendsto_id))
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : 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 : ℤ) ↦
      HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (((fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) ∘ fun (x : ℤ) ↦ id x + -1) x))
    atTop (𝓝 (L - L))
⊢ Tendsto.{0, u_2} (β := F)
    (fun (x : ℤ) ↦ HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)) atTop (𝓝 0)

Tactic:
simp only [id_eq, Int.reduceNeg, Function.comp_apply, sub_self, ← sub_eq_add_neg] at this

Premises used: sub_self, Int.reduceNeg, sub_eq_add_neg, Function.comp_apply, id_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this :
  Tendsto.{0, u_2} (β := F)
    (fun (x : ℤ) ↦ HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero] at this

Premises used: tendsto_zero_iff_norm_tendsto_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : 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 : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
refine :
  EventuallyEq (β := ℝ) atTop
    (fun (x : ℤ) ↦ 2⁻¹ * ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖) fun (x : ℤ) ↦
    ‖f x‖
⊢ Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖f x‖) atTop (𝓝 0)

Tactic:
refine (mul_zero (_ : ℝ) ▸ this.const_mul 2⁻¹).congr' ?_
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : 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 : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
h :
  ∀ (x : ℤ) (hx : 1 ≤ x), 2⁻¹ * ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖ = ‖f x‖
⊢ EventuallyEq (β := ℝ) atTop
    (fun (x : ℤ) ↦ 2⁻¹ * ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖) fun (x : ℤ) ↦
    ‖f x‖

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : 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 : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
⊢ 0 ≤ x

Tactic:
positivity
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : 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 : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
lift :
  ∀ (x : ℕ) (hx : LE.le (α := ℤ) 1 (↑x : ℤ)),
    Icc (-(↑x : ℤ)) (↑x : ℤ) =
      Icc (-HSub.hSub (α := ℤ) (↑x : ℤ) 1) (HSub.hSub (α := ℤ) (↑x : ℤ) 1) ∪ {-(↑x : ℤ), (↑x : ℤ)}
⊢ Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}

Tactic:
lift x to ℕ using by positivity
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : 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 : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℕ
hx : LE.le (α := ℤ) 1 (↑x : ℤ)
⊢ Icc (-HAdd.hAdd (α := ℤ) (↑(x - 1) : ℤ) 1) (HAdd.hAdd (α := ℤ) (↑(x - 1) : ℤ) 1) =
    Icc (-(↑(x - 1) : ℤ)) (↑(x - 1) : ℤ) ∪ {-HAdd.hAdd (α := ℤ) (↑(x - 1) : ℤ) 1, HAdd.hAdd (α := ℤ) (↑(x - 1) : ℤ) 1}

Tactic:
Finset.Icc_succ_succ (x - 1) (x - 1)

Premises used: Finset.Icc_succ_succ, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : 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 : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℕ
hx : LE.le (α := ℤ) 1 (↑x : ℤ)
h h₁ : (↑x : ℤ) = HAdd.hAdd (α := ℤ) (↑(x - 1) : ℤ) 1
h₂ h₃ : HSub.hSub (α := ℤ) (↑x : ℤ) 1 = (↑(x - 1) : ℤ)
h₄ h₅ : (↑x : ℤ) = HAdd.hAdd (α := ℤ) (↑(x - 1) : ℤ) 1
⊢ Icc (-(↑x : ℤ)) (↑x : ℤ) =
    Icc (-HSub.hSub (α := ℤ) (↑x : ℤ) 1) (HSub.hSub (α := ℤ) (↑x : ℤ) 1) ∪ {-(↑x : ℤ), (↑x : ℤ)}

Tactic:
convert! Finset.Icc_succ_succ (x - 1) (x - 1)

Premises used: Finset.Icc_succ_succ, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : 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 : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℕ
hx : LE.le (α := ℤ) 1 (↑x : ℤ)
⊢ (↑x : ℤ) = HAdd.hAdd (α := ℤ) (↑(x - 1) : ℤ) 1

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : 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 : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℕ
hx : LE.le (α := ℤ) 1 (↑x : ℤ)
⊢ HSub.hSub (α := ℤ) (↑x : ℤ) 1 = (↑(x - 1) : ℤ)

Tactic:
grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : 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 : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
⊢ Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}

Tactic:
have : Finset.Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x} := by
    lift x to ℕ using by positivity
    convert! Finset.Icc_succ_succ (x - 1) (x - 1) <;> grind
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this_1 :
  Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
h : -x ∉ {x}
h₁ : Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}
⊢ 2⁻¹ * ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖ = ‖f x‖

Tactic:
rw [this, Finset.sum_union, Finset.sum_insert, Finset.sum_singleton,
    hs x, add_comm, add_sub_cancel_right, ← two_zsmul, norm_smul, Int.norm_eq_abs,
    Int.cast_two, abs_two, inv_mul_cancel_left₀ two_ne_zero]

Premises used: norm_smul, inv_mul_cancel_left₀, Int.cast_two, Int.norm_eq_abs, Finset.sum_union, add_comm, Finset.sum_singleton, two_ne_zero, two_zsmul, add_sub_cancel_right, Finset.sum_insert, abs_two
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this_1 :
  Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
h : ¬-x = x
⊢ -x ∉ {x}

Tactic:
simp only [disjoint_iff_ne, mem_insert, mem_singleton, mem_Icc]

Premises used: Finset.mem_singleton, Finset.mem_Icc, Finset.mem_insert, Finset.disjoint_iff_ne
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this_1 :
  Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ ¬-x = x

Tactic:
omega
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this_1 :
  Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
h : ∀ (a : ℤ), -(x - 1) ≤ a ∧ a ≤ x - 1 → ∀ (b : ℤ), b = -x ∨ b = x → a ≠ b
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}

Tactic:
simp only [disjoint_iff_ne, mem_insert, mem_singleton, mem_Icc]

Premises used: Finset.mem_singleton, Finset.mem_Icc, Finset.mem_insert, Finset.disjoint_iff_ne
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this_1 :
  Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖)
    atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ ∀ (a : ℤ), -(x - 1) ≤ a ∧ a ≤ x - 1 → ∀ (b : ℤ), b = -x ∨ b = x → a ≠ b

Tactic:
omega
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L₁ L₂ : SummationFilter β
hf : Multipliable f L₂
h : L₁.filter ≤ L₂.filter
⊢ Multipliable f L₁

Tactic:
match hf with | ⟨a, ha⟩ => ⟨a, ha.mono_left h⟩

Premises used: Multipliable, Exists.intro, Filter.Tendsto.mono_left, _private.0.Multipliable.mono_filter.match_1
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
contrapose! : ∀ (hL : L.filter.NeBot), L.NeBot
⊢ L.filter = ⊥

Tactic:
contrapose! hL
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
hL : L.filter.NeBot
⊢ L.NeBot

Tactic:
⟨hL⟩

Premises used: SummationFilter.NeBot.mk
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
f : β → α
a : α
hL : L.filter.NeBot
⊢ L.NeBot

Tactic:
exact ⟨hL⟩