Theorem: MvPowerSeries.variables_tendsto_zero (DividedPowers/ForMathlib/MvPowerSeries/Topology.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ Filter.Tendsto (fun s => X s) Filter.cofinite (nhds 0)
Tactic:
rw [tendsto_pi_nhds]
State after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ∀ (x : σ →₀ ℕ), Filter.Tendsto (fun i => X i x) Filter.cofinite (nhds (0 x))

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
⊢ ∀ (x : σ →₀ ℕ), Filter.Tendsto (fun i => X i x) Filter.cofinite (nhds (0 x))
Tactic:
intro d s hs
State after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
⊢ s ∈ Filter.map (fun i => X i d) Filter.cofinite

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
⊢ s ∈ Filter.map (fun i => X i d) Filter.cofinite
Tactic:
rw [Filter.mem_map, Filter.mem_cofinite, ← Set.preimage_compl]
State after:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite
Tactic:
by_cases h : ∃ i, d = Finsupp.single i 1
State after:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ∃ i, d = Finsupp.single i 1
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite

case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite

State before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite
Tactic:
. convert Set.finite_empty
  rw [Set.eq_empty_iff_forall_not_mem]
  intro x
  rw [Set.mem_preimage, Set.not_mem_compl_iff]
  convert mem_of_mem_nhds hs using 1
  rw [← coeff_eq_apply (X x) d, coeff_X, if_neg]
  rfl
  . intro h'
    apply h
    exact ⟨x, h'⟩
State after:
no goals

State before:
case pos
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ∃ i, d = Finsupp.single i 1
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite
Tactic:
obtain ⟨i, rfl⟩ := h
State after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
⊢ ((fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ).Finite

State before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
⊢ ((fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ).Finite
Tactic:
apply Set.Finite.subset (Set.finite_singleton i)
State after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
⊢ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ ⊆ {i}

State before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
⊢ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ ⊆ {i}
Tactic:
intro x
State after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
x : σ
⊢ x ∈ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ → x ∈ {i}

State before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds (0 (Finsupp.single i 1))
x : σ
⊢ x ∈ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ → x ∈ {i}
Tactic:
simp only [OfNat.ofNat, Zero.zero] at hs
State after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
⊢ x ∈ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ → x ∈ {i}

State before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
⊢ x ∈ (fun i_1 => X i_1 (Finsupp.single i 1)) ⁻¹' sᶜ → x ∈ {i}
Tactic:
rw [Set.mem_preimage, Set.mem_compl_iff, Set.mem_singleton_iff, not_imp_comm]
State after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
⊢ ¬x = i → X x (Finsupp.single i 1) ∈ s

State before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
⊢ ¬x = i → X x (Finsupp.single i 1) ∈ s
Tactic:
intro hx
State after:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ X x (Finsupp.single i 1) ∈ s

State before:
case pos.intro
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ X x (Finsupp.single i 1) ∈ s
Tactic:
convert mem_of_mem_nhds hs
State after:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ X x (Finsupp.single i 1) = Zero.zero

State before:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ X x (Finsupp.single i 1) = Zero.zero
Tactic:
rw [← coeff_eq_apply (X x) (Finsupp.single i 1), coeff_X, if_neg]
State after:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ 0 = Zero.zero

case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ ¬Finsupp.single i 1 = Finsupp.single x 1

State before:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ 0 = Zero.zero

case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ ¬Finsupp.single i 1 = Finsupp.single x 1
Tactic:
rfl
State after:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ ¬Finsupp.single i 1 = Finsupp.single x 1

State before:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
s : Set α
i : σ
hs : s ∈ nhds Zero.zero
x : σ
hx : ¬x = i
⊢ ¬Finsupp.single i 1 = Finsupp.single x 1
Tactic:
simp only [Finsupp.single_eq_single_iff, Ne.symm hx, and_true, one_ne_zero, and_self,
or_self, not_false_eq_true]
State after:
no goals

State before:
case neg
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ ((fun i => X i d) ⁻¹' sᶜ).Finite
Tactic:
convert Set.finite_empty
State after:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ (fun i => X i d) ⁻¹' sᶜ = ∅

State before:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ (fun i => X i d) ⁻¹' sᶜ = ∅
Tactic:
rw [Set.eq_empty_iff_forall_not_mem]
State after:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ ∀ (x : σ), x ∉ (fun i => X i d) ⁻¹' sᶜ

State before:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
⊢ ∀ (x : σ), x ∉ (fun i => X i d) ⁻¹' sᶜ
Tactic:
intro x
State after:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ x ∉ (fun i => X i d) ⁻¹' sᶜ

State before:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ x ∉ (fun i => X i d) ⁻¹' sᶜ
Tactic:
rw [Set.mem_preimage, Set.not_mem_compl_iff]
State after:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ X x d ∈ s

State before:
case h.e'_2
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ X x d ∈ s
Tactic:
convert mem_of_mem_nhds hs using 1
State after:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ X x d = 0 d

State before:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ X x d = 0 d
Tactic:
rw [← coeff_eq_apply (X x) d, coeff_X, if_neg]
State after:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ 0 = 0 d

case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ ¬d = Finsupp.single x 1

State before:
case h.e'_4
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ 0 = 0 d

case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ ¬d = Finsupp.single x 1
Tactic:
rfl
State after:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ ¬d = Finsupp.single x 1

State before:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ ¬d = Finsupp.single x 1
Tactic:
. intro h'
  apply h
  exact ⟨x, h'⟩
State after:
no goals

State before:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
⊢ ¬d = Finsupp.single x 1
Tactic:
intro h'
State after:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
h' : d = Finsupp.single x 1
⊢ False

State before:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
h' : d = Finsupp.single x 1
⊢ False
Tactic:
apply h
State after:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
h' : d = Finsupp.single x 1
⊢ ∃ i, d = Finsupp.single i 1

State before:
case h.e'_4.hnc
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
d : σ →₀ ℕ
s : Set α
hs : s ∈ nhds (0 d)
h : ¬∃ i, d = Finsupp.single i 1
x : σ
h' : d = Finsupp.single x 1
⊢ ∃ i, d = Finsupp.single i 1
Tactic:
exact ⟨x, h'⟩
State after:
no goals