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

State before:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
let τ := MvPowerSeries.WithPiTopology.topologicalSpace σ α
State after:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ topologicalSpace σ α = ⋯.topology

State before:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
let τ' := (toSubmodulesBasis σ α).topology
State after:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ topologicalSpace σ α = ⋯.topology

State before:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ topologicalSpace σ α = ⋯.topology
Tactic:
rw [TopologicalAddGroup.ext_iff_nhds_zero τ τ']
State after:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ nhds 0 = nhds 0

State before:
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
⊢ nhds 0 = nhds 0
Tactic:
ext s
State after:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ s ∈ nhds 0

State before:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ s ∈ nhds 0
Tactic:
rw [(RingSubgroupsBasis.hasBasis_nhds (toRingSubgroupsBasis σ α) 0).mem_iff]
State after:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, True ∧ {b | b - 0 ∈ Submodule.toAddSubgroup (basis σ α i)} ⊆ s

State before:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, True ∧ {b | b - 0 ∈ Submodule.toAddSubgroup (basis σ α i)} ⊆ s
Tactic:
simp only [sub_zero, Submodule.mem_toAddSubgroup, true_and]
State after:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ s

State before:
case a
σ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : TopologicalSpace α
inst✝¹ inst✝ : DiscreteTopology α
τ : TopologicalSpace (MvPowerSeries σ α) := topologicalSpace σ α
τ' : TopologicalSpace (MvPowerSeries σ α) := ⋯.topology
s : Set (MvPowerSeries σ α)
⊢ s ∈ nhds 0 ↔ ∃ i, {b | b ∈ basis σ α i} ⊆ s
Tactic:
exact mem_nhds_zero_iff σ α s
State after:
no goals