Theorem: MvPowerSeries.coeff_mul_one_sub_of_lt_weightedOrder (DividedPowers/ForMathlib/MvPowerSeries/Order.lean)

State before:
σ : Type u_1
α✝ : Type ?u.58468
inst✝² : Semiring α✝
w : σ → ℕ
f✝ : MvPowerSeries σ α✝
inst✝¹ : DecidableEq σ
α : Type u_2
inst✝ : CommRing α
f g : MvPowerSeries σ α
d : σ →₀ ℕ
h : ↑((weight w) d) < weightedOrder w g
⊢ (coeff α d) (f * (1 - g)) = (coeff α d) f
Tactic:
simp only [coeff_mul_of_lt_weightedOrder w f h, mul_sub, mul_one, _root_.map_sub, sub_zero]
State after:
no goals