case refine'_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m✝ n✝ : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (n_1 : σ →₀ ℕ), ↑(coeff R n_1) (φ * ↑(monomial R n) a) = ↑(coeff R n_1) (↑(monomial R n) a * φ)
m : σ →₀ ℕ
⊢ Commute (↑(coeff R m) φ) a

case refine'_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m✝ n✝ : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute (↑(coeff R m) φ) a
m : σ →₀ ℕ
⊢ ↑(coeff R m) (φ * ↑(monomial R n) a) = ↑(coeff R m) (↑(monomial R n) a * φ)
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ Commute φ (↑(monomial R n) a) ↔ ∀ (m : σ →₀ ℕ), Commute (↑(coeff R m) φ) a
refine' ext_iff.trans ⟨fun h m => _, fun h m => _⟩
case refine'_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m✝ n✝ : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (n_1 : σ →₀ ℕ), ↑(coeff R n_1) (φ * ↑(monomial R n) a) = ↑(coeff R n_1) (↑(monomial R n) a * φ)
m : σ →₀ ℕ
this : ↑(coeff R (m + n)) (φ * ↑(monomial R n) a) = ↑(coeff R (m + n)) (↑(monomial R n) a * φ)
⊢ Commute (↑(coeff R m) φ) a
case refine'_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m✝ n✝ : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (n_1 : σ →₀ ℕ), ↑(coeff R n_1) (φ * ↑(monomial R n) a) = ↑(coeff R n_1) (↑(monomial R n) a * φ)
m : σ →₀ ℕ
⊢ Commute (↑(coeff R m) φ) a
have := h (m + n)
no goals
case refine'_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m✝ n✝ : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (n_1 : σ →₀ ℕ), ↑(coeff R n_1) (φ * ↑(monomial R n) a) = ↑(coeff R n_1) (↑(monomial R n) a * φ)
m : σ →₀ ℕ
this : ↑(coeff R (m + n)) (φ * ↑(monomial R n) a) = ↑(coeff R (m + n)) (↑(monomial R n) a * φ)
⊢ Commute (↑(coeff R m) φ) a
rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this
case refine'_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m✝ n✝ : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute (↑(coeff R m) φ) a
m : σ →₀ ℕ
⊢ (if n ≤ m then ↑(coeff R (m - n)) φ * a else 0) = if n ≤ m then a * ↑(coeff R (m - n)) φ else 0
case refine'_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m✝ n✝ : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute (↑(coeff R m) φ) a
m : σ →₀ ℕ
⊢ ↑(coeff R m) (φ * ↑(monomial R n) a) = ↑(coeff R m) (↑(monomial R n) a * φ)
rw [coeff_mul_monomial, coeff_monomial_mul]
no goals
case refine'_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m✝ n✝ : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
h : ∀ (m : σ →₀ ℕ), Commute (↑(coeff R m) φ) a
m : σ →₀ ℕ
⊢ (if n ≤ m then ↑(coeff R (m - n)) φ * a else 0) = if n ≤ m then a * ↑(coeff R (m - n)) φ else 0
split_ifs <;> [apply h; rfl]