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

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
⊢ ∃ k, basis σ α k ≤ basis σ α d ⊓ basis σ α e
Tactic:
simp_rw [le_inf_iff]
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
⊢ ∃ k, basis σ α k ≤ basis σ α d ∧ basis σ α k ≤ basis σ α e

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
d e : σ →₀ ℕ
⊢ ∃ k, basis σ α k ≤ basis σ α d ∧ basis σ α k ≤ basis σ α e
Tactic:
exact ⟨d + e, basis_antitone _ _ (le_self_add), basis_antitone _ _ (le_add_self)⟩
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ᶠ (a : MvPowerSeries σ α) in nhds 0, a • f ∈ basis σ α d
Tactic:
rw [Filter.eventually_iff_exists_mem]
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∃ v ∈ nhds 0, ∀ y ∈ v, y • f ∈ basis σ α d

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∃ v ∈ nhds 0, ∀ y ∈ v, y • f ∈ basis σ α d
Tactic:
refine ⟨↑(basis σ α d), (basis_mem_nhds_zero σ α d), ?_⟩
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ y ∈ ↑(basis σ α d), y • f ∈ basis σ α d

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ ∀ y ∈ ↑(basis σ α d), y • f ∈ basis σ α d
Tactic:
intros g hg
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
g : MvPowerSeries σ α
hg : g ∈ ↑(basis σ α d)
⊢ g • f ∈ basis σ α d

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
g : MvPowerSeries σ α
hg : g ∈ ↑(basis σ α d)
⊢ g • f ∈ basis σ α d
Tactic:
rw [smul_eq_mul, mul_comm]
State after:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
g : MvPowerSeries σ α
hg : g ∈ ↑(basis σ α d)
⊢ f * g ∈ basis σ α d

State before:
σ : Type u_1
α : Type u_2
inst✝² : CommRing α
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
f : MvPowerSeries σ α
d : σ →₀ ℕ
g : MvPowerSeries σ α
hg : g ∈ ↑(basis σ α d)
⊢ f * g ∈ basis σ α d
Tactic:
exact Ideal.mul_mem_left _ f (SetLike.mem_coe.mp hg)
State after:
no goals