-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_commute_left (hc : Commute x y) : Commute (p.smeval x) y

Proof state:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
⊢ Commute (a • x ^ n) y

Tactic:
refine Commute.smul_left ?_ a

Result:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
⊢ Commute (x ^ n) y

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
⊢ Commute (p.smeval x) y

Tactic:
induction p using Polynomial.induction_on' with
| h_add r s hr hs => exact (smeval_add R r s x) ▸ Commute.add_left hr hs
| h_monomial n a =>
  simp only [smeval_monomial]
  refine Commute.smul_left ?_ a
  induction n with
  | zero => simp only [npow_zero, Commute.one_left]
  | succ n ih =>
    refine (commute_iff_eq (x ^ (n + 1)) y).mpr ?_
    rw [commute_iff_eq (x ^ n) y] at ih
    rw [pow_succ, ← mul_assoc, ← ih]
    exact Commute.right_comm hc (x ^ n)

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
⊢ Commute (((monomial n) a).smeval x) y

Tactic:
simp only [smeval_monomial]

Result:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
⊢ Commute (a • x ^ n) y

Proof state:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * y = y * x ^ n
⊢ x ^ n * x * y = x ^ n * y * x

Tactic:
exact Commute.right_comm hc (x ^ n)

Result:
no goals

Proof state:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
n : ℕ
a : R
⊢ Commute (x ^ n) y

Tactic:
induction n with
| zero => simp only [npow_zero, Commute.one_left]
| succ n ih =>
  refine (commute_iff_eq (x ^ (n + 1)) y).mpr ?_
  rw [commute_iff_eq (x ^ n) y] at ih
  rw [pow_succ, ← mul_assoc, ← ih]
  exact Commute.right_comm hc (x ^ n)

Result:
no goals

Proof state:
case h_add
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
r s : R[X]
hr : Commute (r.smeval x) y
hs : Commute (s.smeval x) y
⊢ Commute ((r + s).smeval x) y

Tactic:
exact (smeval_add R r s x) ▸ Commute.add_left hr hs

Result:
no goals

Proof state:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * y = y * x ^ n
⊢ x ^ (n + 1) * y = y * x ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, ← ih]

Result:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * y = y * x ^ n
⊢ x ^ n * x * y = x ^ n * y * x

Proof state:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : Commute (x ^ n) y
⊢ x ^ (n + 1) * y = y * x ^ (n + 1)

Tactic:
rw [commute_iff_eq (x ^ n) y] at ih

Result:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : x ^ n * y = y * x ^ n
⊢ x ^ (n + 1) * y = y * x ^ (n + 1)

Proof state:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : Commute (x ^ n) y
⊢ Commute (x ^ (n + 1)) y

Tactic:
refine (commute_iff_eq (x ^ (n + 1)) y).mpr ?_

Result:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
n : ℕ
ih : Commute (x ^ n) y
⊢ x ^ (n + 1) * y = y * x ^ (n + 1)

Proof state:
case h_monomial.zero
R : Type u_1
inst✝⁴ : Semiring R
p : R[X]
S : Type u_2
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : IsScalarTower R S S
inst✝ : SMulCommClass R S S
x y : S
hc : Commute x y
a : R
⊢ Commute (x ^ 0) y

Tactic:
simp only [npow_zero, Commute.one_left]

Result:
no goals