Theorem: Set.Finite.support_of_summable (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
h : Summable f
⊢ (Function.support f).Finite
Tactic:
obtain ⟨a, ha⟩ := h
State after:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : HasSum f a
⊢ (Function.support f).Finite

State before:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : HasSum f a
⊢ (Function.support f).Finite
Tactic:
simp only [HasSum] at ha
State after:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : Filter.Tendsto (fun s => ∑ b ∈ s, f b) Filter.atTop (nhds a)
⊢ (Function.support f).Finite

State before:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : Filter.Tendsto (fun s => ∑ b ∈ s, f b) Filter.atTop (nhds a)
⊢ (Function.support f).Finite
Tactic:
classical
simp_rw [tendsto_atTop_nhds] at ha
obtain ⟨s, hs⟩ := ha {a} rfl (isOpen_discrete _)
apply Set.Finite.subset s.finite_toSet
intro b
rw [Function.mem_support, not_imp_comm]
intro hb
let hs' := hs (insert b s) (s.subset_insert b)
specialize hs s (subset_of_eq rfl)
simp only [Set.mem_singleton_iff] at hs hs'
simpa [Finset.sum_insert hb, hs, add_left_eq_self] using hs'
State after:
no goals

State before:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : Filter.Tendsto (fun s => ∑ b ∈ s, f b) Filter.atTop (nhds a)
⊢ (Function.support f).Finite
Tactic:
simp_rw [tendsto_atTop_nhds] at ha
State after:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ (Function.support f).Finite

State before:
case intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
⊢ (Function.support f).Finite
Tactic:
obtain ⟨s, hs⟩ := ha {a} rfl (isOpen_discrete _)
State after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
⊢ (Function.support f).Finite

State before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
⊢ (Function.support f).Finite
Tactic:
apply Set.Finite.subset s.finite_toSet
State after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
⊢ Function.support f ⊆ ↑s

State before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
⊢ Function.support f ⊆ ↑s
Tactic:
intro b
State after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
⊢ b ∈ Function.support f → b ∈ ↑s

State before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
⊢ b ∈ Function.support f → b ∈ ↑s
Tactic:
rw [Function.mem_support, not_imp_comm]
State after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
⊢ b ∉ ↑s → f b = 0

State before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
⊢ b ∉ ↑s → f b = 0
Tactic:
intro hb
State after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
⊢ f b = 0

State before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
⊢ f b = 0
Tactic:
let hs' := hs (insert b s) (s.subset_insert b)
State after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs' : ∑ b ∈ insert b s, f b ∈ {a} := hs (insert b s) (Finset.subset_insert b s)
⊢ f b = 0

State before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs' : ∑ b ∈ insert b s, f b ∈ {a} := hs (insert b s) (Finset.subset_insert b s)
⊢ f b = 0
Tactic:
specialize hs s (subset_of_eq rfl)
State after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs✝ : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs' : ∑ b ∈ insert b s, f b ∈ {a} := hs✝ (insert b s) (Finset.subset_insert b s)
hs : ∑ b ∈ s, f b ∈ {a}
⊢ f b = 0

State before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs✝ : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs' : ∑ b ∈ insert b s, f b ∈ {a} := hs✝ (insert b s) (Finset.subset_insert b s)
hs : ∑ b ∈ s, f b ∈ {a}
⊢ f b = 0
Tactic:
simp only [Set.mem_singleton_iff] at hs hs'
State after:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs✝ : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs : ∑ b ∈ s, f b = a
hs' : ∑ b ∈ insert b s, f b = a
⊢ f b = 0

State before:
case intro.intro
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
β : Type u_2
f : β → α
a : α
ha : ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : Finset β), N ≤ n → ∑ b ∈ n, f b ∈ U
s : Finset β
hs✝ : ∀ (n : Finset β), s ≤ n → ∑ b ∈ n, f b ∈ {a}
b : β
hb : b ∉ ↑s
hs : ∑ b ∈ s, f b = a
hs' : ∑ b ∈ insert b s, f b = a
⊢ f b = 0
Tactic:
simpa [Finset.sum_insert hb, hs, add_left_eq_self] using hs'
State after:
no goals