-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem scaleRoots_eval₂_mul_of_commute {p : S[X]} (f : S →+* A) (a : A) (s : S)
    (hsa : Commute (f s) a) (hf : ∀ s₁ s₂, Commute (f s₁) (f s₂)) :
    eval₂ f (f s * a) (scaleRoots p s) = f s ^ p.natDegree * eval₂ f a p

Proof state:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
⊢ f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i = f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i

Tactic:
simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc]

Result:
no goals

Proof state:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
⊢ eval₂ f (f s * a) (p.scaleRoots s) =
    ∑ i ∈ (p.scaleRoots s).support, f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i

Tactic:
simp [eval₂_eq_sum, sum_def]

Result:
no goals

Proof state:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
hi' : i ∉ (p.scaleRoots s).support
⊢ p.coeff i * s ^ (p.natDegree - i) = 0

Tactic:
simpa using hi'

Result:
no goals

Proof state:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
⊢ eval₂ f (f s * a) (p.scaleRoots s) = f s ^ p.natDegree * eval₂ f a p

Tactic:
calc
 _ = (scaleRoots p s).support.sum fun i =>
       f (coeff p i * s ^ (p.natDegree - i)) * (f s * a) ^ i := by
   simp [eval₂_eq_sum, sum_def]
 _ = p.support.sum fun i => f (coeff p i * s ^ (p.natDegree - i)) * (f s * a) ^ i :=
   (Finset.sum_subset (support_scaleRoots_le p s) fun i _hi hi' => by
     let this : coeff p i * s ^ (p.natDegree - i) = 0 := by simpa using hi'
     simp [this])
 _ = p.support.sum fun i : ℕ => f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i :=
   (Finset.sum_congr rfl fun i _hi => by
     simp_rw [f.map_mul, f.map_pow, pow_add, hsa.mul_pow, mul_assoc])
 _ = p.support.sum fun i : ℕ => f s ^ p.natDegree * (f (p.coeff i) * a ^ i) :=
   Finset.sum_congr rfl fun i hi => by
     rw [mul_assoc, ← map_pow, (hf _ _).left_comm, map_pow, tsub_add_cancel_of_le]
     exact le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)
 _ = f s ^ p.natDegree * eval₂ f a p := by simp [← Finset.mul_sum, eval₂_eq_sum, sum_def]

Result:
no goals

Proof state:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
hi' : i ∉ (p.scaleRoots s).support
⊢ f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i = 0

Tactic:
let this : coeff p i * s ^ (p.natDegree - i) = 0 := by simpa using hi'

Result:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
hi' : i ∉ (p.scaleRoots s).support
this : p.coeff i * s ^ (p.natDegree - i) = 0 :=
  Eq.mp
    (Eq.trans
      (congrArg Not
        (Eq.trans Mathlib.Algebra.Polynomial.Basic._auxLemma.18 (congrArg (fun x => x ≠ 0) (coeff_scaleRoots p s i))))
      Init.Classical._auxLemma.2)
    hi'
⊢ f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i = 0

Proof state:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
hi : i ∈ p.support
⊢ i ≤ p.natDegree

Tactic:
exact le_natDegree_of_ne_zero (Polynomial.mem_support_iff.mp hi)

Result:
no goals

Proof state:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
_hi : i ∈ p.support
hi' : i ∉ (p.scaleRoots s).support
this : p.coeff i * s ^ (p.natDegree - i) = 0 :=
  Eq.mp
    (Eq.trans
      (congrArg Not
        (Eq.trans Mathlib.Algebra.Polynomial.Basic._auxLemma.18 (congrArg (fun x => x ≠ 0) (coeff_scaleRoots p s i))))
      Init.Classical._auxLemma.2)
    hi'
⊢ f (p.coeff i * s ^ (p.natDegree - i)) * (f s * a) ^ i = 0

Tactic:
simp [this]

Result:
no goals

Proof state:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
hi : i ∈ p.support
⊢ f (p.coeff i) * f s ^ (p.natDegree - i + i) * a ^ i = f s ^ p.natDegree * (f (p.coeff i) * a ^ i)

Tactic:
rw [mul_assoc, ← map_pow, (hf _ _).left_comm, map_pow, tsub_add_cancel_of_le]

Result:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
i : ℕ
hi : i ∈ p.support
⊢ i ≤ p.natDegree

Proof state:
S : Type u_2
A : Type u_3
inst✝¹ : Semiring S
inst✝ : Semiring A
p : S[X]
f : S →+* A
a : A
s : S
hsa : Commute (f s) a
hf : ∀ (s₁ s₂ : S), Commute (f s₁) (f s₂)
⊢ ∑ i ∈ p.support, f s ^ p.natDegree * (f (p.coeff i) * a ^ i) = f s ^ p.natDegree * eval₂ f a p

Tactic:
simp [← Finset.mul_sum, eval₂_eq_sum, sum_def]

Result:
no goals