Theorem: MvPowerSeries.basis_mem_nhds_zero (DividedPowers/ForMathlib/MvPowerSeries/LinearTopology.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ↑(basis σ α d) ∈ nhds 0
Tactic:
rw [nhds_pi, Filter.mem_pi]
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ ↑(basis σ α d)

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ∃ I, I.Finite ∧ ∃ t, (∀ (i : σ →₀ ℕ), t i ∈ nhds (0 i)) ∧ I.pi t ⊆ ↑(basis σ α d)
Tactic:
use Finset.Iic d, Finset.finite_toSet _, (fun e => if e ≤ d then {0} else univ)
State after:
case h
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ (∀ (i : σ →₀ ℕ), (if i ≤ d then {0} else univ) ∈ nhds (0 i)) ∧
    ((↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) ⊆ ↑(basis σ α d)

State before:
case h
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ (∀ (i : σ →₀ ℕ), (if i ≤ d then {0} else univ) ∈ nhds (0 i)) ∧
    ((↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) ⊆ ↑(basis σ α d)
Tactic:
constructor
State after:
case h.left
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ∀ (i : σ →₀ ℕ), (if i ≤ d then {0} else univ) ∈ nhds (0 i)

case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ((↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) ⊆ ↑(basis σ α d)

State before:
case h.left
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ∀ (i : σ →₀ ℕ), (if i ≤ d then {0} else univ) ∈ nhds (0 i)
Tactic:
intro e
State after:
case h.left
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
⊢ (if e ≤ d then {0} else univ) ∈ nhds (0 e)

State before:
case h.left
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
⊢ (if e ≤ d then {0} else univ) ∈ nhds (0 e)
Tactic:
split_ifs with h
State after:
case pos
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : e ≤ d
⊢ {0} ∈ nhds (0 e)

case neg
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : ¬e ≤ d
⊢ univ ∈ nhds (0 e)

State before:
case pos
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : e ≤ d
⊢ {0} ∈ nhds (0 e)

case neg
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : ¬e ≤ d
⊢ univ ∈ nhds (0 e)
Tactic:
. simp only [nhds_discrete, Filter.mem_pure, mem_singleton_iff]
  rfl
State after:
case neg
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : ¬e ≤ d
⊢ univ ∈ nhds (0 e)

State before:
case neg
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : ¬e ≤ d
⊢ univ ∈ nhds (0 e)
Tactic:
. simp only [Filter.univ_mem]
State after:
no goals

State before:
case pos
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : e ≤ d
⊢ {0} ∈ nhds (0 e)
Tactic:
simp only [nhds_discrete, Filter.mem_pure, mem_singleton_iff]
State after:
case pos
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : e ≤ d
⊢ OfNat.ofNat 0 e = 0

State before:
case pos
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : e ≤ d
⊢ OfNat.ofNat 0 e = 0
Tactic:
rfl
State after:
no goals

State before:
case neg
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
h : ¬e ≤ d
⊢ univ ∈ nhds (0 e)
Tactic:
simp only [Filter.univ_mem]
State after:
no goals

State before:
case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
⊢ ((↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) ⊆ ↑(basis σ α d)
Tactic:
intro f
State after:
case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
f : (σ →₀ ℕ) → α
⊢ (f ∈ (↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) → f ∈ ↑(basis σ α d)

State before:
case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
f : (σ →₀ ℕ) → α
⊢ (f ∈ (↑(Finset.Iic d)).pi fun e => if e ≤ d then {0} else univ) → f ∈ ↑(basis σ α d)
Tactic:
simp only [Finset.coe_Iic, mem_pi, mem_Iic, mem_ite_univ_right, mem_singleton_iff, mem_coe]
State after:
case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
f : (σ →₀ ℕ) → α
⊢ (∀ i ≤ d, i ≤ d → f i = 0) → f ∈ basis σ α d

State before:
case h.right
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d : σ →₀ ℕ
f : (σ →₀ ℕ) → α
⊢ (∀ i ≤ d, i ≤ d → f i = 0) → f ∈ basis σ α d
Tactic:
exact forall_imp (fun e h he => h he he)
State after:
no goals