-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem commute_monomial {a : R} {n} :
    Commute φ (monomial R n a) ↔ ∀ m, Commute (coeff R m φ) a

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ Commute φ ((monomial R n) a) ↔ ∀ (m : σ →₀ ℕ), Commute ((coeff R m) φ) a

Tactic:
rw [commute_iff_eq, MvPowerSeries.ext_iff]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ (∀ (n_1 : σ →₀ ℕ), (coeff R n_1) (φ * (monomial R n) a) = (coeff R n_1) ((monomial R n) a * φ)) ↔
    ∀ (m : σ →₀ ℕ), Commute ((coeff R m) φ) a

Proof state:
case refine_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : 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

Tactic:
split_ifs <;> [apply h; rfl]

Result:
no goals

Proof state:
case refine_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : 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

Tactic:
rwa [coeff_add_mul_monomial, add_comm, coeff_add_monomial_mul] at this

Result:
no goals

Proof state:
case refine_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : 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 * φ)

Tactic:
rw [coeff_mul_monomial, coeff_monomial_mul]

Result:
case refine_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : 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

Proof state:
case refine_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : 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

Tactic:
have := h (m + n)

Result:
case refine_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : 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

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : MvPowerSeries σ R
a : R
n : σ →₀ ℕ
⊢ (∀ (n_1 : σ →₀ ℕ), (coeff R n_1) (φ * (monomial R n) a) = (coeff R n_1) ((monomial R n) a * φ)) ↔
    ∀ (m : σ →₀ ℕ), Commute ((coeff R m) φ) a

Tactic:
refine ⟨fun h m => ?_, fun h m => ?_⟩

Result:
case refine_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ : 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
φ : 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 * φ)