α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ (∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s) ↔
    ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ Tendsto (fun x => ∑ b in x.snd, f b - ∑ b in x.fst, f b) atTop (𝓝 0) ↔
    ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
rw [tendsto_atTop']
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ (∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s) →
    ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ (∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e) →
    ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ (∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s) ↔
    ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
constructor
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ (∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s) →
    ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
intro h e he
case mp.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), b ≥ (s₁, s₂) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
obtain ⟨⟨s₁, s₂⟩, h⟩ := h e he
case mp.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), b ≥ (s₁, s₂) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
⊢ ∀ (t : Finset β), Disjoint t (s₁ ∪ s₂) → ∑ b in t, f b ∈ e
case mp.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), b ≥ (s₁, s₂) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
⊢ ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
use s₁ ∪ s₂
case mp.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), b ≥ (s₁, s₂) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
⊢ ∑ b in t, f b ∈ e
case mp.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), b ≥ (s₁, s₂) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
⊢ ∀ (t : Finset β), Disjoint t (s₁ ∪ s₂) → ∑ b in t, f b ∈ e
intro t ht
case mp.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
h : ∑ b in (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).snd, f b - ∑ b in (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).fst, f b ∈ e
⊢ ∑ b in t, f b ∈ e
case mp.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ : Finset β
h : ∀ (b : Finset β × Finset β), b ≥ (s₁, s₂) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
⊢ ∑ b in t, f b ∈ e
specialize h (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t) ⟨le_sup_left, le_sup_of_le_left le_sup_right⟩
no goals
case mp.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
e : Set α
he : e ∈ 𝓝 0
s₁ s₂ t : Finset β
ht : Disjoint t (s₁ ∪ s₂)
h : ∑ b in (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).snd, f b - ∑ b in (s₁ ∪ s₂, s₁ ∪ s₂ ∪ t).fst, f b ∈ e
⊢ ∑ b in t, f b ∈ e
simpa only [Finset.sum_union ht.symm, add_sub_cancel'] using h
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
⊢ ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
⊢ (∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e) →
    ∀ (s : Set α), s ∈ 𝓝 0 → ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ s
rintro h e he
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
⊢ ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
⊢ ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
rcases exists_nhds_half_neg he with ⟨d, hd, hde⟩
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
⊢ ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
case mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
⊢ ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
rcases h d hd with ⟨s, h⟩
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
⊢ ∀ (b : Finset β × Finset β), b ≥ (s, s) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
⊢ ∃ a, ∀ (b : Finset β × Finset β), b ≥ a → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
use (s, s)
case mpr.intro.intro.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
⊢ ∑ b in (t₁, t₂).snd, f b - ∑ b in (t₁, t₂).fst, f b ∈ e
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
⊢ ∀ (b : Finset β × Finset β), b ≥ (s, s) → ∑ b in b.snd, f b - ∑ b in b.fst, f b ∈ e
rintro ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩
case mpr.intro.intro.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
this : ∑ b in t₂, f b - ∑ b in t₁, f b = ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b
⊢ ∑ b in (t₁, t₂).snd, f b - ∑ b in (t₁, t₂).fst, f b ∈ e
case mpr.intro.intro.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
⊢ ∑ b in (t₁, t₂).snd, f b - ∑ b in (t₁, t₂).fst, f b ∈ e
have : ((∑ b in t₂, f b) - ∑ b in t₁, f b) = (∑ b in t₂ \ s, f b) - ∑ b in t₁ \ s, f b := by
  rw [← Finset.sum_sdiff ht₁, ← Finset.sum_sdiff ht₂, add_sub_add_right_eq_sub]
case mpr.intro.intro.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
this : ∑ b in t₂, f b - ∑ b in t₁, f b = ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b
⊢ ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b ∈ e
case mpr.intro.intro.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
this : ∑ b in t₂, f b - ∑ b in t₁, f b = ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b
⊢ ∑ b in (t₁, t₂).snd, f b - ∑ b in (t₁, t₂).fst, f b ∈ e
simp only [this]
no goals
case mpr.intro.intro.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
this : ∑ b in t₂, f b - ∑ b in t₁, f b = ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b
⊢ ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b ∈ e
exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.669264
δ : Type ?u.669267
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
f g : β → α
a a₁ a₂ : α
h✝ : ∀ (e : Set α), e ∈ 𝓝 0 → ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ e
e : Set α
he : e ∈ 𝓝 0
d : Set α
hd : d ∈ 𝓝 0
hde : ∀ (v : α), v ∈ d → ∀ (w : α), w ∈ d → v - w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∑ b in t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).fst ≤ (t₁, t₂).fst
ht₂ : (s, s).snd ≤ (t₁, t₂).snd
⊢ ∑ b in t₂, f b - ∑ b in t₁, f b = ∑ b in t₂ \ s, f b - ∑ b in t₁ \ s, f b
rw [← Finset.sum_sdiff ht₁, ← Finset.sum_sdiff ht₂, add_sub_add_right_eq_sub]