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

Proof state:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval y)

Tactic:
simp only [smeval_monomial]

Result:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval y)

Proof state:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval y)
⊢ Commute (x ^ (n + 1)) (q.smeval y)

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

Result:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval y)
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)

Proof state:
case h_monomial.zero
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval y)

Tactic:
simp only [npow_zero, Commute.one_left]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval 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)) (q.smeval y)).mpr ?_
    rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
    have hxq : x * q.smeval y = q.smeval y * x := by
      refine (commute_iff_eq x (q.smeval y)).mp ?_
      exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
    rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
p q : 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 * q.smeval y = q.smeval y * x ^ n
⊢ x * q.smeval y = q.smeval y * x

Tactic:
refine (commute_iff_eq x (q.smeval y)).mp ?_

Result:
R : Type u_1
inst✝⁴ : Semiring R
p q : 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 * q.smeval y = q.smeval y * x ^ n
⊢ Commute x (q.smeval y)

Proof state:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval y)

Tactic:
induction n with
| zero => simp only [npow_zero, Commute.one_left]
| succ n ih =>
  refine (commute_iff_eq (x ^ (n + 1)) (q.smeval y)).mpr ?_
  rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
  have hxq : x * q.smeval y = q.smeval y * x := by
    refine (commute_iff_eq x (q.smeval y)).mp ?_
    exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
  rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]

Result:
no goals

Proof state:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : 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 * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)

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

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Semiring R
p q : 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 * q.smeval y = q.smeval y * x ^ n
⊢ Commute x (q.smeval y)

Tactic:
exact Commute.symm (smeval_commute_left R q (Commute.symm hc))

Result:
no goals

Proof state:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval y)
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)

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

Result:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : 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 * q.smeval y = q.smeval y * x ^ n
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)

Proof state:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval y)

Tactic:
refine Commute.smul_left ?_ a

Result:
case h_monomial
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval y)

Proof state:
case h_add
R : Type u_1
inst✝⁴ : Semiring R
p q : 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) (q.smeval y)
hs : Commute (s.smeval x) (q.smeval y)
⊢ Commute ((r + s).smeval x) (q.smeval 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 q : 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 * q.smeval y = q.smeval y * x ^ n
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)

Tactic:
have hxq : x * q.smeval y = q.smeval y * x := by
  refine (commute_iff_eq x (q.smeval y)).mp ?_
  exact Commute.symm (smeval_commute_left R q (Commute.symm hc))

Result:
case h_monomial.succ
R : Type u_1
inst✝⁴ : Semiring R
p q : 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 * q.smeval y = q.smeval y * x ^ n
hxq : x * q.smeval y = q.smeval y * x
⊢ x ^ (n + 1) * q.smeval y = q.smeval y * x ^ (n + 1)