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

State before:
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f ∈ basis σ α d ↔ ∀ e ≤ d, (coeff α e) f = 0
Tactic:
simp only [basis, Submodule.mem_mk, AddSubmonoid.mem_mk, Set.mem_setOf_eq]
State after:
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f ∈ { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ↔ ∀ e ≤ d, (coeff α e) f = 0

State before:
σ : Type u_1
α : Type u_2
inst✝ : CommRing α
f : MvPowerSeries σ α
d : σ →₀ ℕ
⊢ f ∈ { carrier := {f | ∀ e ≤ d, (coeff α e) f = 0}, add_mem' := ⋯ } ↔ ∀ e ≤ d, (coeff α e) f = 0
Tactic:
rfl
State after:
no goals