Theorem: Function.finite_support_of_tendsto_zero (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

State before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : Tendsto f cofinite (nhds 0)
⊢ (support f).Finite
Tactic:
rw [nhds_discrete, tendsto_pure] at hf
State after:
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
⊢ (support f).Finite

State before:
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
⊢ (support f).Finite
Tactic:
obtain ⟨s, H, p⟩ := Eventually.exists_mem hf
State after:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
⊢ (support f).Finite

State before:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
⊢ (support f).Finite
Tactic:
apply Finite.subset H
State after:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
⊢ support f ⊆ sᶜ

State before:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
⊢ support f ⊆ sᶜ
Tactic:
intro x hx
State after:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
⊢ x ∈ sᶜ

State before:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
⊢ x ∈ sᶜ
Tactic:
rw [mem_compl_iff]
State after:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
⊢ x ∉ s

State before:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
⊢ x ∉ s
Tactic:
by_contra hxs
State after:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
hxs : x ∈ s
⊢ False

State before:
case intro.intro
α : Type u_1
ι : Type u_2
inst✝² : AddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : ι → α
hf : ∀ᶠ (x : ι) in cofinite, f x = 0
s : Set ι
H : s ∈ cofinite
p : ∀ y ∈ s, f y = 0
x : ι
hx : x ∈ support f
hxs : x ∈ s
⊢ False
Tactic:
exact hx (p x hxs)
State after:
no goals