awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : L.NeBot
hf : Multipliable f L
n : ℕ
zero : ∏'[L] (b : β), HPow.hPow (β := ℕ) (f b) 0 = HPow.hPow (α := α) (β := ℕ) (∏'[L] (b : β), f b) 0
⊢ ∏'[L] (b : β), f b ^ n = HPow.hPow (α := α) (∏'[L] (b : β), f b) n
have succ : ∀ (n : ℕ) (hn : ∏'[L] (b : β), f b ^ n = HPow.hPow (α := α) (∏'[L] (b : β), f b) n),
  ∏'[L] (b : β), f b ^ (n + 1) = HPow.hPow (α := α) (∏'[L] (b : β), f b) (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n hn => simp [pow_succ, (hf.pow n).tprod_mul hf, hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : DecidableEq β
inst_5 : L.LeAtTop
inst_6 : L.NeBot
f : β → α
b : β
hf : Multipliable (update (β := fun (a : β) ↦ α) f b 1) L
n : β
⊢ f n = (if n = b then f n else 1) * update (β := fun (a : β) ↦ α) f b 1 n
have pos : ∀ (h : n = b), f n = f n * update (β := fun (a : β) ↦ α) f b 1 n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : DecidableEq β
inst_5 : L.LeAtTop
inst_6 : L.NeBot
f : β → α
b : β
hf : Multipliable (update (β := fun (a : β) ↦ α) f b 1) L
n : β
pos : ∀ (h : n = b), f n = f n * update (β := fun (a : β) ↦ α) f b 1 n
⊢ f n = (if n = b then f n else 1) * update (β := fun (a : β) ↦ α) f b 1 n
have neg : ∀ (h : ¬n = b), f n = 1 * update (β := fun (a : β) ↦ α) f b 1 n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
inst_2 : T2Space α
inst_3 : ContinuousMul α
inst_4 : DecidableEq β
inst_5 : L.LeAtTop
inst_6 : L.NeBot
f : β → α
b : β
hf : Multipliable (update (β := fun (a : β) ↦ α) f b 1) L
⊢ HMul.hMul (α := α) (∏'[L] (x : β), if x = b then f x else 1) (∏'[L] (x : β), update (β := fun (a : β) ↦ α) f b 1 x) =
    (if b = b then f b else 1) * ∏'[L] (x : β), update (β := fun (a : β) ↦ α) f b 1 x
have e_a : (∏'[L] (x : β), if x = b then f x else 1) = if b = b then f b else 1
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
hf : ∃ (b : β), f b = 0
inst_2 : L.LeAtTop
⊢ HasProd f 0 L
have obtain : ∀ (b : β) (hb : f b = 0), HasProd f 0 L
Tactic: obtain ⟨b, hb⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.LeAtTop
b : β
hb : f b = 0
⊢ HasProd f 0 L
have apply : EventuallyEq.{u_2, u_1} (β := α) L.filter (fun (x : Finset β) ↦ 0) fun (s : Finset β) ↦ ∏ b ∈ s, f b
Tactic: apply tendsto_const_nhds.congr'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoidWithZero α
inst_1 : TopologicalSpace α
f : β → α
L : SummationFilter β
inst_2 : L.LeAtTop
b : β
hb : f b = 0
⊢ EventuallyEq.{u_2, u_1} (β := α) L.filter (fun (x : Finset β) ↦ 0) fun (s : Finset β) ↦ ∏ b ∈ s, f b
have h : ∀ (s : Finset β) (hs : {b} ≤ s), Eq.{u_1 + 1} (α := α) 0 (∏ b ∈ s, f b)
Tactic: filter_upwards [(eventually_ge_atTop {b}).filter_mono L.le_atTop] with s hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
Goal:
⊢ symmetricIcc ℤ = symmetricIoo ℤ
have simp : Eq (α := Filter (Finset ℤ)) (Filter.map (fun (g : ℤ) ↦ Icc (-g) g) atTop) (Filter.map (fun (g : ℤ) ↦ Ioo (-g) g) atTop)
Tactic: simp only [symmetricIcc, symmetricIoo, mk.injEq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
Goal:
⊢ Eq (α := Filter (Finset ℤ)) (Filter.map (fun (g : ℤ) ↦ Icc (-g) g) atTop)
    (Filter.map (fun (g : ℤ) ↦ Ioo (-g) g) atTop)
have h : ∀ (s : Set (Finset ℤ)),
  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: ext s
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
Goal:
s : Set (Finset ℤ)
⊢ 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
have h : (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) ↔
  ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
Goal:
s : Set (Finset ℤ)
⊢ (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) ↔
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
have 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
Tactic: refine ⟨fun ⟨a, ha⟩ ↦ ⟨a + 1, fun b hb ↦ ?_⟩, fun ⟨a, ha⟩ ↦ ⟨a - 1, fun b hb ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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
⊢ (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) ↔
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
have 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
Tactic: refine ⟨fun ⟨a, ha⟩ ↦ ⟨a + 1, fun b hb ↦ ?_⟩, fun ⟨a, ha⟩ ↦ ⟨a - 1, fun b hb ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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
have h : Eq (α := Finset ℤ) (Ioo (-(↑b : ℤ)) (↑b : ℤ)) (Icc (-(↑(b - 1) : ℤ)) (↑(b - 1) : ℤ))
Tactic: convert! ha (b - 1) (by grind) using 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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
⊢ Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s
have h : Eq (α := Finset ℤ) (Icc (-(↑b : ℤ)) (↑b : ℤ)) (Ioo (-(↑(b + 1) : ℤ)) (↑(b + 1) : ℤ))
Tactic: convert! ha (b + 1) (by grind) using 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
Goal:
s : Set (Finset ℤ)
⊢ (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) ↔
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
have 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) : ℤ))
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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) : ℤ))
⊢ (∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Icc (-(↑b : ℤ)) (↑b : ℤ) ∈ s) ↔
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → Ioo (-(↑b : ℤ)) (↑b : ℤ) ∈ s
have 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) : ℤ))
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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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) : ℤ))
have h : ∀ (a : ℤ), -(↑b : ℤ) < a ∧ a < (↑b : ℤ) ↔ -(↑(b - 1) : ℤ) ≤ a ∧ a ≤ (↑(b - 1) : ℤ)
Tactic: simp [Finset.ext_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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
⊢ Eq (α := Finset ℤ) (Icc (-(↑b : ℤ)) (↑b : ℤ)) (Ioo (-(↑(b + 1) : ℤ)) (↑(b + 1) : ℤ))
have h : ∀ (a : ℤ), -(↑b : ℤ) ≤ a ∧ a ≤ (↑b : ℤ) ↔ -1 < a + (↑b : ℤ) ∧ a < HAdd.hAdd (α := ℤ) (↑b : ℤ) 1
Tactic: simp [Finset.ext_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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)
⊢ HasProd f a (symmetricIco ℤ)
have 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)
Tactic: simp only [HasProd, tendsto_map'_iff, symmetricIcc_eq_map_Icc_nat,
    ← Nat.map_cast_int_atTop, symmetricIco] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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 (comp (β := ℤ) ((fun (s : Finset ℤ) ↦ ∏ b ∈ s, f b) ∘ fun (N : ℤ) ↦ Ico (-N) N) Nat.cast) atTop (𝓝 a)
have 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)
Tactic: apply tendsto_of_div_tendsto_one _ hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hf : Summable f (symmetricIcc ℤ)
hs : Function.Even f
⊢ Tendsto f atTop (𝓝 0)
have rw : Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖f x‖) atTop (𝓝 0)
Tactic: rw [tendsto_zero_iff_norm_tendsto_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormSMulClass ℤ F
f : ℤ → F
hf : Summable f (symmetricIcc ℤ)
hs : Function.Even f
⊢ Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖f x‖) atTop (𝓝 0)
have obtain : ∀ (L : F) (hL : HasSum f L (symmetricIcc ℤ)), Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖f x‖) atTop (𝓝 0)
Tactic: obtain ⟨L, hL⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (hypothesis)
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 : ℤ) ↦ ‖f x‖) atTop (𝓝 0)
have hL₁ : Tendsto (fun (x : ℤ) ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
Tactic: rw [HasSum, symmetricIcc_filter, tendsto_map'_iff, Function.comp_def] at hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (hypothesis)
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 : ℤ) ↦ ‖f x‖) atTop (𝓝 0)
have 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))
Tactic: have := hL.sub (hL.comp (tendsto_atTop_add_const_right _ (-1) tendsto_id))
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (hypothesis)
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 (β := ℝ) (fun (x : ℤ) ↦ ‖f x‖) atTop (𝓝 0)
have 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)
Tactic: simp only [id_eq, Int.reduceNeg, Function.comp_apply, sub_self, ← sub_eq_add_neg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (hypothesis)
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 : ℤ) ↦ ‖f x‖) atTop (𝓝 0)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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)
⊢ Tendsto (β := ℝ) (fun (x : ℤ) ↦ ‖f x‖) atTop (𝓝 0)
have 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‖
Tactic: refine (mul_zero (_ : ℝ) ▸ this.const_mul 2⁻¹).congr' ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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)
⊢ 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‖
have 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‖
Tactic: filter_upwards [eventually_ge_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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}
have lift : ∀ (x : ℕ) (hx : LE.le (α := ℤ) 1 (↑x : ℤ)),
  Icc (-(↑x : ℤ)) (↑x : ℤ) =
    Icc (-HSub.hSub (α := ℤ) (↑x : ℤ) 1) (HSub.hSub (α := ℤ) (↑x : ℤ) 1) ∪ {-(↑x : ℤ), (↑x : ℤ)}
Tactic: lift x to ℕ using by positivity
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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 (-(↑x : ℤ)) (↑x : ℤ) =
    Icc (-HSub.hSub (α := ℤ) (↑x : ℤ) 1) (HSub.hSub (α := ℤ) (↑x : ℤ) 1) ∪ {-(↑x : ℤ), (↑x : ℤ)}
have h : (↑x : ℤ) = HAdd.hAdd (α := ℤ) (↑(x - 1) : ℤ) 1
Tactic: convert! Finset.Icc_succ_succ (x - 1) (x - 1)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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
⊢ Icc (-(↑x : ℤ)) (↑x : ℤ) =
    Icc (-HSub.hSub (α := ℤ) (↑x : ℤ) 1) (HSub.hSub (α := ℤ) (↑x : ℤ) 1) ∪ {-(↑x : ℤ), (↑x : ℤ)}
have h₂ : HSub.hSub (α := ℤ) (↑x : ℤ) 1 = (↑(x - 1) : ℤ)
Tactic: convert! Finset.Icc_succ_succ (x - 1) (x - 1)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (hypothesis)
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
⊢ 2⁻¹ * ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖ = ‖f x‖
have this₁ : 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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}
⊢ 2⁻¹ * ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖ = ‖f x‖
have h : -x ∉ {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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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}
⊢ 2⁻¹ * ‖HSub.hSub (α := F) (∑ b ∈ Icc (-x) x, f b) (∑ b ∈ Icc (-(x - 1)) (x - 1), f b)‖ = ‖f x‖
have h₁ : Disjoint (Icc (-(x - 1)) (x - 1)) {-x, 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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}
have h : ¬-x = x
Tactic: simp only [disjoint_iff_ne, mem_insert, mem_singleton, mem_Icc]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt (goal)
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}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}
have h : ∀ (a : ℤ), -(x - 1) ≤ a ∧ a ≤ x - 1 → ∀ (b : ℤ), b = -x ∨ b = x → a ≠ b
Tactic: simp only [disjoint_iff_ne, mem_insert, mem_singleton, mem_Icc]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
⊢ L.filter = ⊥
have contrapose! : ∀ (hL : L.filter.NeBot), L.NeBot
Tactic: contrapose! hL
Cleared hypotheses: hL
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
⊢ HasProd f a L
have this : L.filter = ⊥
Tactic: have : L.filter = ⊥ := by contrapose! hL; exact ⟨hL⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
this : L.filter = ⊥
⊢ HasProd f a L
have rw : Tendsto (fun (s : Finset β) ↦ ∏ b ∈ s, f b) ⊥ (𝓝 a)
Tactic: rw [HasProd, this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
⊢ Eq.{u_1 + 1} (α := α) (∏'[L] (b : β), f b) (∏ᶠ (b : β), f b)
have simp : (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
    finprod (L.support.mulIndicator fun (b : β) ↦ f b)
  else
    if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
    else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) sorry) =
  ∏ᶠ (b : β), f b
Tactic: simp only [tprod_def, dif_pos (multipliable_bot hL f)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Defs (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
⊢ (if L.HasSupport ∧ ((mulSupport.{u_2, u_1} (M := α) fun (b : β) ↦ f b) ∩ L.support).Finite then
      finprod (L.support.mulIndicator fun (b : β) ↦ f b)
    else
      if HasProd.{u_1, u_2} (α := α) (fun (b : β) ↦ f b) 1 L then 1
      else Exists.choose (p := fun (a : α) ↦ HasProd (fun (b : β) ↦ f b) a L) ⋯) =
    ∏ᶠ (b : β), f b
have this : L.LeAtTop
Tactic: haveI : L.LeAtTop := L.leAtTop_of_not_NeBot hL