[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ : R →+* S
x✝ : S
f : R →+* S
x : S
⊢ eval₂ f x p = sum p fun e a => ↑f a * x ^ e
[PROOFSTEP]
rw [eval₂_def]
[GOAL]
R✝ : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p q r : R✝[X]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
x : S✝
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f g : R →+* S
s t : S
φ ψ : R[X]
⊢ f = g → s = t → φ = ψ → eval₂ f s φ = eval₂ g t ψ
[PROOFSTEP]
rintro rfl rfl rfl
[GOAL]
R✝ : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p q r : R✝[X]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
x : S✝
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
s : S
φ : R[X]
⊢ eval₂ f s φ = eval₂ f s φ
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f 0 p = ↑f (coeff p 0)
[PROOFSTEP]
simp (config := { contextual := true }) only [eval₂_eq_sum, zero_pow_eq, mul_ite, mul_zero, mul_one, sum,
  Classical.not_not, mem_support_iff, sum_ite_eq', ite_eq_left_iff, RingHom.map_zero, imp_true_iff, eq_self_iff_true]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x 0 = 0
[PROOFSTEP]
simp [eval₂_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (↑C a) = ↑f a
[PROOFSTEP]
simp [eval₂_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x X = x
[PROOFSTEP]
simp [eval₂_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
r : R
⊢ eval₂ f x (↑(monomial n) r) = ↑f r * x ^ n
[PROOFSTEP]
simp [eval₂_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x (X ^ n) = x ^ n
[PROOFSTEP]
rw [X_pow_eq_monomial]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x (↑(monomial n) 1) = x ^ n
[PROOFSTEP]
convert eval₂_monomial f x (n := n) (r := 1)
[GOAL]
case h.e'_3
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ x ^ n = ↑f 1 * x ^ n
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q
[PROOFSTEP]
simp only [eval₂_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ (sum (p + q) fun e a => ↑f a * x ^ e) = (sum p fun e a => ↑f a * x ^ e) + sum q fun e a => ↑f a * x ^ e
[PROOFSTEP]
apply sum_add_index
[GOAL]
case hf
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ∀ (i : ℕ), ↑f 0 * x ^ i = 0
[PROOFSTEP]
simp [add_mul]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ ∀ (a : ℕ) (b₁ b₂ : R), ↑f (b₁ + b₂) * x ^ a = ↑f b₁ * x ^ a + ↑f b₂ * x ^ a
[PROOFSTEP]
simp [add_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x 1 = 1
[PROOFSTEP]
rw [← C_1, eval₂_C, f.map_one]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (bit0 p) = bit0 (eval₂ f x p)
[PROOFSTEP]
rw [bit0, eval₂_add, bit0]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (bit1 p) = bit1 (eval₂ f x p)
[PROOFSTEP]
rw [bit1, eval₂_add, eval₂_bit0, eval₂_one, bit1]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
⊢ eval₂ g x (s • p) = ↑g s * eval₂ g x p
[PROOFSTEP]
have A : p.natDegree < p.natDegree.succ := Nat.lt_succ_self _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
A : natDegree p < Nat.succ (natDegree p)
⊢ eval₂ g x (s • p) = ↑g s * eval₂ g x p
[PROOFSTEP]
have B : (s • p).natDegree < p.natDegree.succ := (natDegree_smul_le _ _).trans_lt A
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
A : natDegree p < Nat.succ (natDegree p)
B : natDegree (s • p) < Nat.succ (natDegree p)
⊢ eval₂ g x (s • p) = ↑g s * eval₂ g x p
[PROOFSTEP]
rw [eval₂_eq_sum, eval₂_eq_sum, sum_over_range' _ _ _ A, sum_over_range' _ _ _ B]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
A : natDegree p < Nat.succ (natDegree p)
B : natDegree (s • p) < Nat.succ (natDegree p)
⊢ ∑ a in range (Nat.succ (natDegree p)), ↑g (coeff (s • p) a) * x ^ a =
    ↑g s * ∑ a in range (Nat.succ (natDegree p)), ↑g (coeff p a) * x ^ a
[PROOFSTEP]
simp [mul_sum, mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
A : natDegree p < Nat.succ (natDegree p)
B : natDegree (s • p) < Nat.succ (natDegree p)
⊢ ∀ (n : ℕ), ↑g 0 * x ^ n = 0
[PROOFSTEP]
simp [mul_sum, mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
g : R →+* S
p : R[X]
x : S
s : R
A : natDegree p < Nat.succ (natDegree p)
B : natDegree (s • p) < Nat.succ (natDegree p)
⊢ ∀ (n : ℕ), ↑g 0 * x ^ n = 0
[PROOFSTEP]
simp [mul_sum, mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[X]
hp : eval₂ C X p = p
hq : eval₂ C X q = q
⊢ eval₂ C X (p + q) = p + q
[PROOFSTEP]
simp [hp, hq]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x✝ : S
n : ℕ
x : R
⊢ eval₂ C X (↑(monomial n) x) = ↑(monomial n) x
[PROOFSTEP]
rw [eval₂_monomial, ← smul_X_eq_monomial, C_mul']
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x ↑n = ↑n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x ↑Nat.zero = ↑Nat.zero
[PROOFSTEP]
simp only [eval₂_zero, Nat.cast_zero, Nat.zero_eq]
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
ih : eval₂ f x ↑n = ↑n
⊢ eval₂ f x ↑(Nat.succ n) = ↑(Nat.succ n)
[PROOFSTEP]
rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T
p : T[X]
g : ℕ → T → R[X]
x : S
⊢ eval₂ f x (sum p g) = sum p fun n a => eval₂ f x (g n a)
[PROOFSTEP]
let T : R[X] →+ S :=
  { toFun := eval₂ f x
    map_zero' := eval₂_zero _ _
    map_add' := fun p q => eval₂_add _ _ }
[GOAL]
R : Type u
S : Type v
T✝ : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S :=
  { toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
    map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
⊢ eval₂ f x (sum p g) = sum p fun n a => eval₂ f x (g n a)
[PROOFSTEP]
have A : ∀ y, eval₂ f x y = T y := fun y => rfl
[GOAL]
R : Type u
S : Type v
T✝ : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S :=
  { toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
    map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
A : ∀ (y : R[X]), eval₂ f x y = ↑T y
⊢ eval₂ f x (sum p g) = sum p fun n a => eval₂ f x (g n a)
[PROOFSTEP]
simp only [A]
[GOAL]
R : Type u
S : Type v
T✝ : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x✝ : S
inst✝ : Semiring T✝
p : T✝[X]
g : ℕ → T✝ → R[X]
x : S
T : R[X] →+ S :=
  { toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
    map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
A : ∀ (y : R[X]), eval₂ f x y = ↑T y
⊢ ↑{ toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
          map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
      (sum p g) =
    sum p fun n a =>
      ↑{ toZeroHom := { toFun := eval₂ f x, map_zero' := (_ : eval₂ f x 0 = 0) },
            map_add' := (_ : ∀ (p q : R[X]), eval₂ f x (p + q) = eval₂ f x p + eval₂ f x q) }
        (g n a)
[PROOFSTEP]
rw [sum, T.map_sum, sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f✝ : R →+* S
x✝ : S
inst✝ : Semiring T
f : R →+* S
x : S
p : AddMonoidAlgebra R ℕ
⊢ eval₂ f x { toFinsupp := p } = ↑(liftNC ↑f ↑(↑(powersHom S) x)) p
[PROOFSTEP]
simp only [eval₂_eq_sum, sum, toFinsupp_sum, support, coeff]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f✝ : R →+* S
x✝ : S
inst✝ : Semiring T
f : R →+* S
x : S
p : AddMonoidAlgebra R ℕ
⊢ ∑ x_1 in p.support, ↑f (↑p x_1) * x ^ x_1 = ↑(liftNC ↑f ↑(↑(powersHom S) x)) p
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
hf : ∀ (k : ℕ), Commute (↑f (coeff q k)) x
⊢ eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q
[PROOFSTEP]
rcases p with ⟨p⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
hf : ∀ (k : ℕ), Commute (↑f (coeff q k)) x
p : AddMonoidAlgebra R ℕ
⊢ eval₂ f x ({ toFinsupp := p } * q) = eval₂ f x { toFinsupp := p } * eval₂ f x q
[PROOFSTEP]
rcases q with ⟨q⟩
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
p q : AddMonoidAlgebra R ℕ
hf : ∀ (k : ℕ), Commute (↑f (coeff { toFinsupp := q } k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }
[PROOFSTEP]
simp only [coeff] at hf 
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
p q : AddMonoidAlgebra R ℕ
hf : ∀ (k : ℕ), Commute (↑f (↑q k)) x
⊢ eval₂ f x ({ toFinsupp := p } * { toFinsupp := q }) = eval₂ f x { toFinsupp := p } * eval₂ f x { toFinsupp := q }
[PROOFSTEP]
simp only [← ofFinsupp_mul, eval₂_ofFinsupp]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
p q : AddMonoidAlgebra R ℕ
hf : ∀ (k : ℕ), Commute (↑f (↑q k)) x
⊢ ↑(liftNC ↑f ↑(↑(powersHom S) x)) (p * q) = ↑(liftNC ↑f ↑(↑(powersHom S) x)) p * ↑(liftNC ↑f ↑(↑(powersHom S) x)) q
[PROOFSTEP]
exact liftNC_mul _ _ p q fun {k n} _hn => (hf k).pow_right n
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
⊢ eval₂ f x (p * X) = eval₂ f x p * x
[PROOFSTEP]
refine' _root_.trans (eval₂_mul_noncomm _ _ fun k => _) (by rw [eval₂_X])
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
⊢ eval₂ f x p * eval₂ f x X = eval₂ f x p * x
[PROOFSTEP]
rw [eval₂_X]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
k : ℕ
⊢ Commute (↑f (coeff X k)) x
[PROOFSTEP]
rcases em (k = 1) with (rfl | hk)
[GOAL]
case inl
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
⊢ Commute (↑f (coeff X 1)) x
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
k : ℕ
hk : ¬k = 1
⊢ Commute (↑f (coeff X k)) x
[PROOFSTEP]
simp [coeff_X_of_ne_one hk]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
⊢ eval₂ f x (X * p) = eval₂ f x p * x
[PROOFSTEP]
rw [X_mul, eval₂_mul_X]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
h : Commute (↑f a) x
⊢ eval₂ f x (p * ↑C a) = eval₂ f x p * ↑f a
[PROOFSTEP]
rw [eval₂_mul_noncomm, eval₂_C]
[GOAL]
case hf
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
h : Commute (↑f a) x
⊢ ∀ (k : ℕ), Commute (↑f (coeff (↑C a) k)) x
[PROOFSTEP]
intro k
[GOAL]
case hf
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
h : Commute (↑f a) x
k : ℕ
⊢ Commute (↑f (coeff (↑C a) k)) x
[PROOFSTEP]
by_cases hk : k = 0
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
h : Commute (↑f a) x
k : ℕ
hk : k = 0
⊢ Commute (↑f (coeff (↑C a) k)) x
[PROOFSTEP]
simp only [hk, h, coeff_C_zero, coeff_C_ne_zero]
[GOAL]
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
h : Commute (↑f a) x
k : ℕ
hk : ¬k = 0
⊢ Commute (↑f (coeff (↑C a) k)) x
[PROOFSTEP]
simp only [coeff_C_ne_zero hk, RingHom.map_zero, Commute.zero_left]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
ps : List R[X]
hf : ∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
⊢ eval₂ f x (List.prod ps) = List.prod (List.map (eval₂ f x) ps)
[PROOFSTEP]
induction' ps using List.reverseRecOn with ps p ihp
[GOAL]
case H0
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
ps : List R[X]
hf✝ : ∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
hf : ∀ (p : R[X]), p ∈ [] → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
⊢ eval₂ f x (List.prod []) = List.prod (List.map (eval₂ f x) [])
[PROOFSTEP]
simp
[GOAL]
case H1
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
ps✝ : List R[X]
hf✝ : ∀ (p : R[X]), p ∈ ps✝ → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
ps : List R[X]
p : R[X]
ihp :
  (∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x) →
    eval₂ f x (List.prod ps) = List.prod (List.map (eval₂ f x) ps)
hf : ∀ (p_1 : R[X]), p_1 ∈ ps ++ [p] → ∀ (k : ℕ), Commute (↑f (coeff p_1 k)) x
⊢ eval₂ f x (List.prod (ps ++ [p])) = List.prod (List.map (eval₂ f x) (ps ++ [p]))
[PROOFSTEP]
simp only [List.forall_mem_append, List.forall_mem_singleton] at hf 
[GOAL]
case H1
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
x : S
inst✝ : Semiring T
ps✝ : List R[X]
hf✝ : ∀ (p : R[X]), p ∈ ps✝ → ∀ (k : ℕ), Commute (↑f (coeff p k)) x
ps : List R[X]
p : R[X]
ihp :
  (∀ (p : R[X]), p ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff p k)) x) →
    eval₂ f x (List.prod ps) = List.prod (List.map (eval₂ f x) ps)
hf : (∀ (x_1 : R[X]), x_1 ∈ ps → ∀ (k : ℕ), Commute (↑f (coeff x_1 k)) x) ∧ ∀ (k : ℕ), Commute (↑f (coeff p k)) x
⊢ eval₂ f x (List.prod (ps ++ [p])) = List.prod (List.map (eval₂ f x) (ps ++ [p]))
[PROOFSTEP]
simp [eval₂_mul_noncomm _ _ hf.2, ihp hf.1]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ (fun i => eval₂ f x (↑(monomial i) (coeff p i))) = fun i => ↑f (coeff p i) * x ^ i
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ : R →+* S
x✝ : S
f : R →+* S
p : R[X]
n : ℕ
hn : natDegree p < n
x : S
⊢ eval₂ f x p = ∑ i in range n, ↑f (coeff p i) * x ^ i
[PROOFSTEP]
rw [eval₂_eq_sum, p.sum_over_range' _ _ hn]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ : R →+* S
x✝ : S
f : R →+* S
p : R[X]
n : ℕ
hn : natDegree p < n
x : S
⊢ ∀ (n : ℕ), ↑f 0 * x ^ n = 0
[PROOFSTEP]
intro i
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ : R →+* S
x✝ : S
f : R →+* S
p : R[X]
n : ℕ
hn : natDegree p < n
x : S
i : ℕ
⊢ ↑f 0 * x ^ i = 0
[PROOFSTEP]
rw [f.map_zero, zero_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x (p * q) = 0
[PROOFSTEP]
rw [eval₂_mul f x]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q✝ r : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
q : R[X]
hp : eval₂ f x p = 0
⊢ eval₂ f x p * eval₂ f x q = 0
[PROOFSTEP]
exact mul_eq_zero_of_left hp (q.eval₂ f x)
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hq : eval₂ f x q = 0
⊢ eval₂ f x (p * q) = 0
[PROOFSTEP]
rw [eval₂_mul f x]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : CommSemiring S
f : R →+* S
x : S
p : R[X]
hq : eval₂ f x q = 0
⊢ eval₂ f x p * eval₂ f x q = 0
[PROOFSTEP]
exact mul_eq_zero_of_right (p.eval₂ f x) hq
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ eval x p = sum p fun e a => a * x ^ e
[PROOFSTEP]
rw [eval, eval₂_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ (sum p fun e a => ↑(RingHom.id R) a * x ^ e) = sum p fun e a => a * x ^ e
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x✝ : R
p : R[X]
x : R
⊢ eval x p = ∑ i in range (natDegree p + 1), coeff p i * x ^ i
[PROOFSTEP]
rw [eval_eq_sum, sum_over_range]
[GOAL]
case h
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x✝ : R
p : R[X]
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x✝ : R
p : R[X]
n : ℕ
hn : natDegree p < n
x : R
⊢ eval x p = ∑ i in range n, coeff p i * x ^ i
[PROOFSTEP]
rw [eval_eq_sum, p.sum_over_range' _ _ hn]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x✝ : R
p : R[X]
n : ℕ
hn : natDegree p < n
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
x : R
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ eval₂ f (↑f r) p = ↑f (eval r p)
[PROOFSTEP]
rw [eval₂_eq_sum, eval_eq_sum, sum, sum, f.map_sum]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
x : R
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ ∑ n in support p, ↑f (coeff p n) * ↑f r ^ n = ∑ x in support p, ↑f (coeff p x * r ^ x)
[PROOFSTEP]
simp only [f.map_mul, f.map_pow]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
S : Type u_1
inst✝ : Semiring S
f : R →+* S
⊢ eval₂ f 1 p = ↑f (eval 1 p)
[PROOFSTEP]
convert eval₂_at_apply (p := p) f 1
[GOAL]
case h.e'_2.h.e'_6
R : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
S : Type u_1
inst✝ : Semiring S
f : R →+* S
⊢ 1 = ↑f 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
S : Type u_1
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ eval₂ f (↑n) p = ↑f (eval (↑n) p)
[PROOFSTEP]
convert eval₂_at_apply (p := p) f n
[GOAL]
case h.e'_2.h.e'_6
R : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
S : Type u_1
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ↑n = ↑f ↑n
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
n : ℕ
⊢ eval x ↑n = ↑n
[PROOFSTEP]
simp only [← C_eq_nat_cast, eval_C]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝³ : Semiring R
p✝ q r : R[X]
x✝ : R
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p : R[X]
x : R
⊢ eval x (s • p) = s • eval x p
[PROOFSTEP]
rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ eval x (↑C a * p) = a * eval x p
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q ph qh => simp only [mul_add, eval_add, ph, qh]
| h_monomial n b => simp only [mul_assoc, C_mul_monomial, eval_monomial]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ eval x (↑C a * p) = a * eval x p
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q ph qh => simp only [mul_add, eval_add, ph, qh]
| h_monomial n b => simp only [mul_assoc, C_mul_monomial, eval_monomial]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
x : R
p q : R[X]
ph : eval x (↑C a * p) = a * eval x p
qh : eval x (↑C a * q) = a * eval x q
⊢ eval x (↑C a * (p + q)) = a * eval x (p + q)
[PROOFSTEP]

| h_add p q ph qh => simp only [mul_add, eval_add, ph, qh]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
x : R
p q : R[X]
ph : eval x (↑C a * p) = a * eval x p
qh : eval x (↑C a * q) = a * eval x q
⊢ eval x (↑C a * (p + q)) = a * eval x (p + q)
[PROOFSTEP]
simp only [mul_add, eval_add, ph, qh]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
n : ℕ
b : R
⊢ eval x (↑C a * ↑(monomial n) b) = a * eval x (↑(monomial n) b)
[PROOFSTEP]

| h_monomial n b => simp only [mul_assoc, C_mul_monomial, eval_monomial]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
n : ℕ
b : R
⊢ eval x (↑C a * ↑(monomial n) b) = a * eval x (↑(monomial n) b)
[PROOFSTEP]
simp only [mul_assoc, C_mul_monomial, eval_monomial]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
⊢ eval (1 + y) (↑(monomial d) (↑d + 1)) - eval y (↑(monomial d) (↑d + 1)) =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * y ^ (x_1 - 1))
[PROOFSTEP]
have cast_succ : (d + 1 : S) = ((d.succ : ℕ) : S) := by simp only [Nat.cast_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
⊢ ↑d + 1 = ↑(Nat.succ d)
[PROOFSTEP]
simp only [Nat.cast_succ]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
⊢ eval (1 + y) (↑(monomial d) (↑d + 1)) - eval y (↑(monomial d) (↑d + 1)) =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * y ^ (x_1 - 1))
[PROOFSTEP]
rw [cast_succ, eval_monomial, eval_monomial, add_comm, add_pow]
  -- Porting note: `apply_congr` hadn't been ported yet, so `congr` & `ext` is used.
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
⊢ ↑(Nat.succ d) * ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m) - ↑(Nat.succ d) * y ^ d =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * y ^ (x_1 - 1))
[PROOFSTEP]
conv_lhs =>
  congr
  · congr
    ·skip
    · congr
      ·skip
      · ext
        rw [one_pow, mul_one, mul_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d) * ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m) - ↑(Nat.succ d) * y ^ d
[PROOFSTEP]
  congr
  · congr
    ·skip
    · congr
      ·skip
      · ext
        rw [one_pow, mul_one, mul_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d) * ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m) - ↑(Nat.succ d) * y ^ d
[PROOFSTEP]
  congr
  · congr
    ·skip
    · congr
      ·skip
      · ext
        rw [one_pow, mul_one, mul_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d) * ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m) - ↑(Nat.succ d) * y ^ d
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d) * ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
case a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d) * y ^ d
[PROOFSTEP]
· congr
  ·skip
  · congr
    ·skip
    · ext
      rw [one_pow, mul_one, mul_comm]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d) * ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
  congr
  ·skip
  · congr
    ·skip
    · ext
      rw [one_pow, mul_one, mul_comm]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d) * ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
  congr
  ·skip
  · congr
    ·skip
    · ext
      rw [one_pow, mul_one, mul_comm]
[GOAL]
case a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d) * ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
congr
[GOAL]
case a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d)
case a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
·skip
[GOAL]
case a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d)
[PROOFSTEP]
skip
[GOAL]
case a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d)
[PROOFSTEP]
skip
[GOAL]
case a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ↑(Nat.succ d)
[PROOFSTEP]
skip
[GOAL]
case a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
· congr
  ·skip
  · ext
    rw [one_pow, mul_one, mul_comm]
[GOAL]
case a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
  congr
  ·skip
  · ext
    rw [one_pow, mul_one, mul_comm]
[GOAL]
case a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
  congr
  ·skip
  · ext
    rw [one_pow, mul_one, mul_comm]
[GOAL]
case a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| ∑ m in range (d + 1), y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
congr
[GOAL]
case a.a.s
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| range (d + 1)
case a.a.f
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| fun m => y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
·skip
[GOAL]
case a.a.s
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| range (d + 1)
[PROOFSTEP]
skip
[GOAL]
case a.a.s
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| range (d + 1)
[PROOFSTEP]
skip
[GOAL]
case a.a.s
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| range (d + 1)
[PROOFSTEP]
skip
[GOAL]
case a.a.f
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| fun m => y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
· ext
  rw [one_pow, mul_one, mul_comm]
[GOAL]
case a.a.f
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| fun m => y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
  ext
  rw [one_pow, mul_one, mul_comm]
[GOAL]
case a.a.f
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| fun m => y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
  ext
  rw [one_pow, mul_one, mul_comm]
[GOAL]
case a.a.f
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
| fun m => y ^ m * 1 ^ (d - m) * ↑(Nat.choose d m)
[PROOFSTEP]
ext
[GOAL]
case a.a.f.h
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
x✝ : ℕ
| y ^ x✝ * 1 ^ (d - x✝) * ↑(Nat.choose d x✝)
[PROOFSTEP]
rw [one_pow, mul_one, mul_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
⊢ ↑(Nat.succ d) * ∑ x in range (d + 1), ↑(Nat.choose d x) * y ^ x - ↑(Nat.succ d) * y ^ d =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * y ^ (x_1 - 1))
[PROOFSTEP]
rw [sum_range_succ, mul_add, Nat.choose_self, Nat.cast_one, one_mul, add_sub_cancel, mul_sum, sum_range_succ',
  Nat.cast_zero, zero_mul, mul_zero, add_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
⊢ ∑ x in range d, ↑(Nat.succ d) * (↑(Nat.choose d x) * y ^ x) =
    ∑ k in range d, ↑(Nat.choose (d + 1) (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1))
[PROOFSTEP]
refine sum_congr rfl fun y _hy => ?_
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : CommRing S
d : ℕ
y✝ : S
cast_succ : ↑d + 1 = ↑(Nat.succ d)
y : ℕ
_hy : y ∈ range d
⊢ ↑(Nat.succ d) * (↑(Nat.choose d y) * y✝ ^ y) = ↑(Nat.choose (d + 1) (y + 1)) * (↑(y + 1) * y✝ ^ (y + 1 - 1))
[PROOFSTEP]
rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.succ_mul_choose_eq, Nat.cast_mul, Nat.add_sub_cancel]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
n : ℕ
⊢ eval x (↑n * p) = ↑n * eval x p
[PROOFSTEP]
rw [← C_eq_nat_cast, eval_C_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ eval x (p * X) = eval x p * x
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q ph qh => simp only [add_mul, eval_add, ph, qh]
| h_monomial n a =>
  simp only [← monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial, mul_one, pow_succ', mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ eval x (p * X) = eval x p * x
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q ph qh => simp only [add_mul, eval_add, ph, qh]
| h_monomial n a =>
  simp only [← monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial, mul_one, pow_succ', mul_assoc]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
x : R
p q : R[X]
ph : eval x (p * X) = eval x p * x
qh : eval x (q * X) = eval x q * x
⊢ eval x ((p + q) * X) = eval x (p + q) * x
[PROOFSTEP]

| h_add p q ph qh => simp only [add_mul, eval_add, ph, qh]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
x : R
p q : R[X]
ph : eval x (p * X) = eval x p * x
qh : eval x (q * X) = eval x q * x
⊢ eval x ((p + q) * X) = eval x (p + q) * x
[PROOFSTEP]
simp only [add_mul, eval_add, ph, qh]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
n : ℕ
a : R
⊢ eval x (↑(monomial n) a * X) = eval x (↑(monomial n) a) * x
[PROOFSTEP]

| h_monomial n a =>
  simp only [← monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial, mul_one, pow_succ', mul_assoc]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
n : ℕ
a : R
⊢ eval x (↑(monomial n) a * X) = eval x (↑(monomial n) a) * x
[PROOFSTEP]
simp only [← monomial_one_one_eq_X, monomial_mul_monomial, eval_monomial, mul_one, pow_succ', mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k : ℕ
⊢ eval x (p * X ^ k) = eval x p * x ^ k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
⊢ eval x (p * X ^ Nat.zero) = eval x p * x ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k : ℕ
ih : eval x (p * X ^ k) = eval x p * x ^ k
⊢ eval x (p * X ^ Nat.succ k) = eval x p * x ^ Nat.succ k
[PROOFSTEP]
simp [pow_succ', ← mul_assoc, ih]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : DecidableEq R
⊢ Decidable (IsRoot p a)
[PROOFSTEP]
unfold IsRoot
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
x : R
inst✝ : DecidableEq R
⊢ Decidable (eval a p = 0)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x : R
p : R[X]
⊢ coeff p 0 = coeff p 0 * 0 ^ 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x : R
p : R[X]
⊢ coeff p 0 * 0 ^ 0 = eval 0 p
[PROOFSTEP]
symm
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x : R
p : R[X]
⊢ eval 0 p = coeff p 0 * 0 ^ 0
[PROOFSTEP]
rw [eval_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x : R
p : R[X]
⊢ (sum p fun e a => a * 0 ^ e) = coeff p 0 * 0 ^ 0
[PROOFSTEP]
exact Finset.sum_eq_single _ (fun b _ hb => by simp [zero_pow (Nat.pos_of_ne_zero hb)]) (by simp)
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x : R
p : R[X]
b : ℕ
x✝ : b ∈ support p
hb : b ≠ 0
⊢ (fun e a => a * 0 ^ e) b (coeff p b) = 0
[PROOFSTEP]
simp [zero_pow (Nat.pos_of_ne_zero hb)]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x : R
p : R[X]
⊢ ¬0 ∈ support p → (fun e a => a * 0 ^ e) 0 (coeff p 0) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
x : R
p : R[X]
hp : coeff p 0 = 0
⊢ IsRoot p 0
[PROOFSTEP]
rwa [coeff_zero_eq_eval_zero] at hp 
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p✝ q✝ r : R✝[X]
x✝ : R✝
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
x : R
h : IsRoot p x
hpq : p ∣ q
⊢ IsRoot q x
[PROOFSTEP]
rwa [IsRoot, eval, eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hpq]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
x r a : R
hr : r ≠ 0
⊢ ¬IsRoot (↑C r) a
[PROOFSTEP]
simpa using hr
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp p q = sum p fun e a => ↑C a * q ^ e
[PROOFSTEP]
rw [comp, eval₂_eq_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp p X = p
[PROOFSTEP]
simp only [comp, eval₂_def, C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ (sum p fun e a => ↑(monomial e) a) = p
[PROOFSTEP]
exact sum_monomial_eq _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp p (↑C a) = ↑C (eval a p)
[PROOFSTEP]
simp [comp, (C : R →+* _).map_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ comp (↑n) p = ↑n
[PROOFSTEP]
rw [← C_eq_nat_cast, C_comp]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp p 0 = ↑C (eval 0 p)
[PROOFSTEP]
rw [← C_0, comp_C]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp 0 p = 0
[PROOFSTEP]
rw [← C_0, C_comp]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp p 1 = ↑C (eval 1 p)
[PROOFSTEP]
rw [← C_1, comp_C]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp 1 p = 1
[PROOFSTEP]
rw [← C_1, C_comp]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp (p * X) r = comp p r * r
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp only [hp, hq, add_mul, add_comp]
| h_monomial n b => simp only [pow_succ', mul_assoc, monomial_mul_X, monomial_comp]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp (p * X) r = comp p r * r
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp only [hp, hq, add_mul, add_comp]
| h_monomial n b => simp only [pow_succ', mul_assoc, monomial_mul_X, monomial_comp]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : comp (p * X) r = comp p r * r
hq : comp (q * X) r = comp q r * r
⊢ comp ((p + q) * X) r = comp (p + q) r * r
[PROOFSTEP]

| h_add p q hp hq => simp only [hp, hq, add_mul, add_comp]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : comp (p * X) r = comp p r * r
hq : comp (q * X) r = comp q r * r
⊢ comp ((p + q) * X) r = comp (p + q) r * r
[PROOFSTEP]
simp only [hp, hq, add_mul, add_comp]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
b : R
⊢ comp (↑(monomial n) b * X) r = comp (↑(monomial n) b) r * r
[PROOFSTEP]

| h_monomial n b => simp only [pow_succ', mul_assoc, monomial_mul_X, monomial_comp]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
b : R
⊢ comp (↑(monomial n) b * X) r = comp (↑(monomial n) b) r * r
[PROOFSTEP]
simp only [pow_succ', mul_assoc, monomial_mul_X, monomial_comp]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
k : ℕ
⊢ comp (X ^ k) p = p ^ k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp (X ^ Nat.zero) p = p ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
k : ℕ
ih : comp (X ^ k) p = p ^ k
⊢ comp (X ^ Nat.succ k) p = p ^ Nat.succ k
[PROOFSTEP]
simp [pow_succ', mul_X_comp, ih]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
k : ℕ
⊢ comp (p * X ^ k) r = comp p r * r ^ k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp (p * X ^ Nat.zero) r = comp p r * r ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
k : ℕ
ih : comp (p * X ^ k) r = comp p r * r ^ k
⊢ comp (p * X ^ Nat.succ k) r = comp p r * r ^ Nat.succ k
[PROOFSTEP]
simp [ih, pow_succ', ← mul_assoc, mul_X_comp]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp (↑C a * p) r = ↑C a * comp p r
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp [hp, hq, mul_add]
| h_monomial n b => simp [mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp (↑C a * p) r = ↑C a * comp p r
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp [hp, hq, mul_add]
| h_monomial n b => simp [mul_assoc]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : comp (↑C a * p) r = ↑C a * comp p r
hq : comp (↑C a * q) r = ↑C a * comp q r
⊢ comp (↑C a * (p + q)) r = ↑C a * comp (p + q) r
[PROOFSTEP]

| h_add p q hp hq => simp [hp, hq, mul_add]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : comp (↑C a * p) r = ↑C a * comp p r
hq : comp (↑C a * q) r = ↑C a * comp q r
⊢ comp (↑C a * (p + q)) r = ↑C a * comp (p + q) r
[PROOFSTEP]
simp [hp, hq, mul_add]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
b : R
⊢ comp (↑C a * ↑(monomial n) b) r = ↑C a * comp (↑(monomial n) b) r
[PROOFSTEP]

| h_monomial n b => simp [mul_assoc]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
b : R
⊢ comp (↑C a * ↑(monomial n) b) r = ↑C a * comp (↑(monomial n) b) r
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ comp (↑n * p) r = ↑n * comp p r
[PROOFSTEP]
rw [← C_eq_nat_cast, C_mul_comp, C_eq_nat_cast]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp (bit0 p) q = bit0 (comp p q)
[PROOFSTEP]
simp only [bit0, add_comp]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp (bit1 p) q = bit1 (comp p q)
[PROOFSTEP]
simp only [bit1, add_comp, bit0_comp, one_comp]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝³ : Semiring R
p✝ q✝ r : R[X]
inst✝² : Monoid S
inst✝¹ : DistribMulAction S R
inst✝ : IsScalarTower S R R
s : S
p q : R[X]
⊢ comp (s • p) q = s • comp p q
[PROOFSTEP]
rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ comp (comp φ ψ) χ = comp φ (comp ψ χ)
[PROOFSTEP]
refine Polynomial.induction_on φ ?_ ?_ ?_
[GOAL]
case refine_1
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (a : R), comp (comp (↑C a) ψ) χ = comp (↑C a) (comp ψ χ)
[PROOFSTEP]
intros
[GOAL]
case refine_1
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
a✝ : R
⊢ comp (comp (↑C a✝) ψ) χ = comp (↑C a✝) (comp ψ χ)
[PROOFSTEP]
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ', ← mul_assoc]
[GOAL]
case refine_2
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (p q : R[X]),
    comp (comp p ψ) χ = comp p (comp ψ χ) →
      comp (comp q ψ) χ = comp q (comp ψ χ) → comp (comp (p + q) ψ) χ = comp (p + q) (comp ψ χ)
[PROOFSTEP]
intros
[GOAL]
case refine_2
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ p✝ q✝ : R[X]
a✝¹ : comp (comp p✝ ψ) χ = comp p✝ (comp ψ χ)
a✝ : comp (comp q✝ ψ) χ = comp q✝ (comp ψ χ)
⊢ comp (comp (p✝ + q✝) ψ) χ = comp (p✝ + q✝) (comp ψ χ)
[PROOFSTEP]
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ', ← mul_assoc]
[GOAL]
case refine_3
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
⊢ ∀ (n : ℕ) (a : R),
    comp (comp (↑C a * X ^ n) ψ) χ = comp (↑C a * X ^ n) (comp ψ χ) →
      comp (comp (↑C a * X ^ (n + 1)) ψ) χ = comp (↑C a * X ^ (n + 1)) (comp ψ χ)
[PROOFSTEP]
intros
[GOAL]
case refine_3
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
n✝ : ℕ
a✝¹ : R
a✝ : comp (comp (↑C a✝¹ * X ^ n✝) ψ) χ = comp (↑C a✝¹ * X ^ n✝) (comp ψ χ)
⊢ comp (comp (↑C a✝¹ * X ^ (n✝ + 1)) ψ) χ = comp (↑C a✝¹ * X ^ (n✝ + 1)) (comp ψ χ)
[PROOFSTEP]
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ', ← mul_assoc]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ coeff (comp p q) (natDegree p * natDegree q) = leadingCoeff p * leadingCoeff q ^ natDegree p
[PROOFSTEP]
rw [comp, eval₂_def, coeff_sum]
  -- Porting note: `convert` → `refine`
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ (sum p fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) = leadingCoeff p * leadingCoeff q ^ natDegree p
[PROOFSTEP]
refine Eq.trans (Finset.sum_eq_single p.natDegree ?h₀ ?h₁) ?h₂
[GOAL]
case h₀
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ∀ (b : ℕ),
    b ∈ support p → b ≠ natDegree p → (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0
case h₂
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) =
    leadingCoeff p * leadingCoeff q ^ natDegree p
[PROOFSTEP]
case h₂ => simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) =
    leadingCoeff p * leadingCoeff q ^ natDegree p
[PROOFSTEP]
case h₂ => simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) =
    leadingCoeff p * leadingCoeff q ^ natDegree p
[PROOFSTEP]
simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]
[GOAL]
case h₀
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ∀ (b : ℕ),
    b ∈ support p → b ≠ natDegree p → (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0
[PROOFSTEP]
case h₀ =>
  intro b hbs hbp
  refine' coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt _)
  rw [natDegree_C, zero_add]
  refine' natDegree_pow_le.trans_lt ((mul_lt_mul_right (pos_iff_ne_zero.mpr hqd0)).mpr _)
  exact lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ∀ (b : ℕ),
    b ∈ support p → b ≠ natDegree p → (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0
[PROOFSTEP]
case h₀ =>
  intro b hbs hbp
  refine' coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt _)
  rw [natDegree_C, zero_add]
  refine' natDegree_pow_le.trans_lt ((mul_lt_mul_right (pos_iff_ne_zero.mpr hqd0)).mpr _)
  exact lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ∀ (b : ℕ),
    b ∈ support p → b ≠ natDegree p → (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0
[PROOFSTEP]
intro b hbs hbp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) b (coeff p b) = 0
[PROOFSTEP]
refine' coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt _)
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ natDegree (↑C (coeff p b)) + natDegree (q ^ b) < natDegree p * natDegree q
[PROOFSTEP]
rw [natDegree_C, zero_add]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ natDegree (q ^ b) < natDegree p * natDegree q
[PROOFSTEP]
refine' natDegree_pow_le.trans_lt ((mul_lt_mul_right (pos_iff_ne_zero.mpr hqd0)).mpr _)
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
b : ℕ
hbs : b ∈ support p
hbp : b ≠ natDegree p
⊢ b < natDegree p
[PROOFSTEP]
exact lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp
[GOAL]
case h₁
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0
[PROOFSTEP]
case h₁ => simp (config := { contextual := true })
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0
[PROOFSTEP]
case h₁ => simp (config := { contextual := true })
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
hqd0 : natDegree q ≠ 0
⊢ ¬natDegree p ∈ support p →
    (fun a b => coeff (↑C b * q ^ a) (natDegree p * natDegree q)) (natDegree p) (coeff p (natDegree p)) = 0
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ map f (↑(monomial n) a) = ↑(monomial n) (↑f a)
[PROOFSTEP]
dsimp only [map]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ eval₂ (RingHom.comp C f) X (↑(monomial n) a) = ↑(monomial n) (↑f a)
[PROOFSTEP]
rw [eval₂_monomial, ← C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
a : R
⊢ ↑(RingHom.comp C f) a * X ^ n = ↑C (↑f a) * X ^ n
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
⊢ map f (p * q) = map f p * map f q
[PROOFSTEP]
rw [map, eval₂_mul_noncomm]
[GOAL]
case hf
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
⊢ ∀ (k : ℕ), Commute (↑(RingHom.comp C f) (coeff q k)) X
[PROOFSTEP]
exact fun k => (commute_X _).symm
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : Semiring S
f : R →+* S
r : R
⊢ map f (r • p) = ↑f r • map f p
[PROOFSTEP]
rw [map, eval₂_smul, RingHom.comp_apply, C_mul']
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
n : ℕ
inst✝ : Nat.AtLeastTwo n
⊢ map f ↑n = ↑n
[PROOFSTEP]
rw [Polynomial.map_nat_cast]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ coeff (map f p) n = ↑f (coeff p n)
[PROOFSTEP]
rw [map, eval₂_def, coeff_sum, sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ∑ n_1 in support p, coeff (↑(RingHom.comp C f) (coeff p n_1) * X ^ n_1) n = ↑f (coeff p n)
[PROOFSTEP]
conv_rhs => rw [← sum_C_mul_X_pow_eq p, coeff_sum, sum, map_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
| ↑f (coeff p n)
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq p, coeff_sum, sum, map_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
| ↑f (coeff p n)
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq p, coeff_sum, sum, map_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
| ↑f (coeff p n)
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq p, coeff_sum, sum, map_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ ∑ n_1 in support p, coeff (↑(RingHom.comp C f) (coeff p n_1) * X ^ n_1) n =
    ∑ x in support p, ↑f (coeff (↑C (coeff p x) * X ^ x) n)
[PROOFSTEP]
refine'
  Finset.sum_congr rfl fun x _hx =>
    _
      -- Porting note: Was `simp [Function.comp, coeff_C_mul_X_pow, f.map_mul]`.
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n x : ℕ
_hx : x ∈ support p
⊢ coeff (↑(RingHom.comp C f) (coeff p x) * X ^ x) n = ↑f (coeff (↑C (coeff p x) * X ^ x) n)
[PROOFSTEP]
simp [Function.comp, coeff_C_mul_X_pow, -map_mul, -coeff_C_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n x : ℕ
_hx : x ∈ support p
⊢ (if n = x then ↑f (coeff p x) else 0) = ↑f (if n = x then coeff p x else 0)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n x : ℕ
_hx : x ∈ support p
h✝ : n = x
⊢ ↑f (coeff p x) = ↑f (coeff p x)
[PROOFSTEP]
simp [f.map_zero]
[GOAL]
case neg
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
n x : ℕ
_hx : x ∈ support p
h✝ : ¬n = x
⊢ 0 = ↑f 0
[PROOFSTEP]
simp [f.map_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
e : R ≃+* S
⊢ RingHom.comp ↑(mapRingHom ↑(RingEquiv.symm e)) ↑(mapRingHom ↑e) = RingHom.id R[X]
[PROOFSTEP]
ext
[GOAL]
case h₁.a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
e : R ≃+* S
x✝ : R
n✝ : ℕ
⊢ coeff (↑(RingHom.comp (RingHom.comp ↑(mapRingHom ↑(RingEquiv.symm e)) ↑(mapRingHom ↑e)) C) x✝) n✝ =
    coeff (↑(RingHom.comp (RingHom.id R[X]) C) x✝) n✝
[PROOFSTEP]
simp
[GOAL]
case h₂.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
e : R ≃+* S
n✝ : ℕ
⊢ coeff (↑(RingHom.comp ↑(mapRingHom ↑(RingEquiv.symm e)) ↑(mapRingHom ↑e)) X) n✝ = coeff (↑(RingHom.id R[X]) X) n✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
e : R ≃+* S
⊢ RingHom.comp ↑(mapRingHom ↑e) ↑(mapRingHom ↑(RingEquiv.symm e)) = RingHom.id S[X]
[PROOFSTEP]
ext
[GOAL]
case h₁.a.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
e : R ≃+* S
x✝ : S
n✝ : ℕ
⊢ coeff (↑(RingHom.comp (RingHom.comp ↑(mapRingHom ↑e) ↑(mapRingHom ↑(RingEquiv.symm e))) C) x✝) n✝ =
    coeff (↑(RingHom.comp (RingHom.id S[X]) C) x✝) n✝
[PROOFSTEP]
simp
[GOAL]
case h₂.a
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
e : R ≃+* S
n✝ : ℕ
⊢ coeff (↑(RingHom.comp ↑(mapRingHom ↑e) ↑(mapRingHom ↑(RingEquiv.symm e))) X) n✝ = coeff (↑(RingHom.id S[X]) X) n✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p✝ q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
p : R[X]
⊢ ∀ (n : ℕ), coeff (map g (map f p)) n = coeff (map (RingHom.comp g f) p) n
[PROOFSTEP]
simp [coeff_map]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
⊢ map (RingHom.id R) p = p
[PROOFSTEP]
simp [Polynomial.ext_iff, coeff_map]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p = eval x (map f p)
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp [hp, hq]
| h_monomial n r => simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x p = eval x (map f p)
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp [hp, hq]
| h_monomial n r => simp
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[X]
hp : eval₂ f x p = eval x (map f p)
hq : eval₂ f x q = eval x (map f q)
⊢ eval₂ f x (p + q) = eval x (map f (p + q))
[PROOFSTEP]

| h_add p q hp hq => simp [hp, hq]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
p q : R[X]
hp : eval₂ f x p = eval x (map f p)
hq : eval₂ f x q = eval x (map f q)
⊢ eval₂ f x (p + q) = eval x (map f (p + q))
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
r : R
⊢ eval₂ f x (↑(monomial n) r) = eval x (map f (↑(monomial n) r))
[PROOFSTEP]

| h_monomial n r => simp
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
r : R
⊢ eval₂ f x (↑(monomial n) r) = eval x (map f (↑(monomial n) r))
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m✝ n : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Injective ↑f
p q : R[X]
h : map f p = map f q
m : ℕ
⊢ ↑f (coeff p m) = ↑f (coeff q m)
[PROOFSTEP]
rw [← coeff_map f, ← coeff_map f, h]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝¹ q✝ r : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ↑f
p✝ p q : S[X]
hp : ∃ a, map f a = p
hq : ∃ a, map f a = q
p' : R[X]
hp' : map f p' = p
q' : R[X]
hq' : map f q' = q
⊢ map f (p' + q') = p + q
[PROOFSTEP]
rw [Polynomial.map_add f, hp', hq']
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r✝ : R[X]
inst✝ : Semiring S
f : R →+* S
hf : Function.Surjective ↑f
p : S[X]
n : ℕ
s : S
r : R
hr : ↑f r = s
⊢ map f (↑(monomial n) r) = ↑(monomial n) s
[PROOFSTEP]
rw [map_monomial f, hr]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ degree (map f p) ≤ degree p
[PROOFSTEP]
refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m✝ n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : degree p < ↑m
⊢ coeff (map f p) m = 0
[PROOFSTEP]
rw [degree_lt_iff_coeff_zero] at hm 
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m✝ n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff p m_1 = 0
⊢ coeff (map f p) m = 0
[PROOFSTEP]
simp [hm m le_rfl]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
hfp : map f p = 0
x : R
⊢ ↑f x = ↑f x * ↑f (leadingCoeff p)
[PROOFSTEP]
simp only [mul_one, hp.leadingCoeff, f.map_one]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
hfp : map f p = 0
x : R
⊢ ↑f x * coeff (map f p) (natDegree p) = 0
[PROOFSTEP]
simp only [hfp, mul_zero, coeff_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
hp : Monic p
h : ∀ (x : R), ↑f x = 0
n : ℕ
⊢ coeff (map f p) n = coeff 0 n
[PROOFSTEP]
simp only [h, coeff_map, coeff_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
⊢ degree p ≤ degree (map f p)
[PROOFSTEP]
have hp0 : p ≠ 0 := leadingCoeff_ne_zero.mp fun hp0 => hf (_root_.trans (congr_arg _ hp0) f.map_zero)
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ degree p ≤ degree (map f p)
[PROOFSTEP]
rw [degree_eq_natDegree hp0]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ ↑(natDegree p) ≤ degree (map f p)
[PROOFSTEP]
refine' le_degree_of_ne_zero _
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ coeff (map f p) (natDegree p) ≠ 0
[PROOFSTEP]
rw [coeff_map]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
hp0 : p ≠ 0
⊢ ↑f (coeff p (natDegree p)) ≠ 0
[PROOFSTEP]
exact hf
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
⊢ leadingCoeff (map f p) = ↑f (leadingCoeff p)
[PROOFSTEP]
unfold leadingCoeff
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
hf : ↑f (leadingCoeff p) ≠ 0
⊢ coeff (map f p) (natDegree (map f p)) = ↑f (coeff p (natDegree p))
[PROOFSTEP]
rw [coeff_map, natDegree_map_of_leadingCoeff_ne_zero f hf]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ RingHom.rangeS (mapRingHom f) ↔ ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ RingHom.rangeS (mapRingHom f) → ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
[PROOFSTEP]
rintro ⟨p, rfl⟩ n
[GOAL]
case mp.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ coeff (↑(mapRingHom f) p) n ∈ RingHom.rangeS f
[PROOFSTEP]
rw [coe_mapRingHom, coeff_map]
[GOAL]
case mp.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ ↑f (coeff p n) ∈ RingHom.rangeS f
[PROOFSTEP]
exact Set.mem_range_self _
[GOAL]
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
⊢ (∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f) → p ∈ RingHom.rangeS (mapRingHom f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ p ∈ RingHom.rangeS (mapRingHom f)
[PROOFSTEP]
rw [p.as_sum_range_C_mul_X_pow]
[GOAL]
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ ∑ i in range (natDegree p + 1), ↑C (coeff p i) * X ^ i ∈ RingHom.rangeS (mapRingHom f)
[PROOFSTEP]
refine' (mapRingHom f).rangeS.sum_mem _
[GOAL]
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
⊢ ∀ (c : ℕ), c ∈ range (natDegree p + 1) → ↑C (coeff p c) * X ^ c ∈ RingHom.rangeS (mapRingHom f)
[PROOFSTEP]
intro i _hi
[GOAL]
case mpr
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
i : ℕ
_hi : i ∈ range (natDegree p + 1)
⊢ ↑C (coeff p i) * X ^ i ∈ RingHom.rangeS (mapRingHom f)
[PROOFSTEP]
rcases h i with ⟨c, hc⟩
[GOAL]
case mpr.intro
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
i : ℕ
_hi : i ∈ range (natDegree p + 1)
c : R
hc : ↑f c = coeff p i
⊢ ↑C (coeff p i) * X ^ i ∈ RingHom.rangeS (mapRingHom f)
[PROOFSTEP]
use C c * X ^ i
[GOAL]
case h
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), coeff p n ∈ RingHom.rangeS f
i : ℕ
_hi : i ∈ range (natDegree p + 1)
c : R
hc : ↑f c = coeff p i
⊢ ↑(mapRingHom f) (↑C c * X ^ i) = ↑C (coeff p i) * X ^ i
[PROOFSTEP]
rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
x : T
⊢ eval₂ g x (map f p) = eval₂ (RingHom.comp g f) x p
[PROOFSTEP]
rw [eval₂_eq_eval_map, eval₂_eq_eval_map, map_map]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (a : R), map f (comp (↑C a) q) = comp (map f (↑C a)) (map f q)
[PROOFSTEP]
simp only [map_C, forall_const, C_comp, eq_self_iff_true]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (p q_1 : R[X]),
    map f (comp p q) = comp (map f p) (map f q) →
      map f (comp q_1 q) = comp (map f q_1) (map f q) → map f (comp (p + q_1) q) = comp (map f (p + q_1)) (map f q)
[PROOFSTEP]
simp (config := { contextual := true }) only [Polynomial.map_add, add_comp, forall_const, imp_true_iff,
  eq_self_iff_true]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (n : ℕ) (a : R),
    map f (comp (↑C a * X ^ n) q) = comp (map f (↑C a * X ^ n)) (map f q) →
      map f (comp (↑C a * X ^ (n + 1)) q) = comp (map f (↑C a * X ^ (n + 1))) (map f q)
[PROOFSTEP]
simp (config := { contextual := true }) only [pow_succ', ← mul_assoc, comp, forall_const, eval₂_mul_X, imp_true_iff,
  eq_self_iff_true, map_X, Polynomial.map_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
p : R[X]
⊢ eval 0 (map f p) = ↑f (eval 0 p)
[PROOFSTEP]
simp [← coeff_zero_eq_eval_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
p : R[X]
⊢ eval 1 (map f p) = ↑f (eval 1 p)
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| h_monomial n r => simp only [one_pow, mul_one, eval_monomial, map_monomial]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
p : R[X]
⊢ eval 1 (map f p) = ↑f (eval 1 p)
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| h_monomial n r => simp only [one_pow, mul_one, eval_monomial, map_monomial]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
p q : R[X]
hp : eval 1 (map f p) = ↑f (eval 1 p)
hq : eval 1 (map f q) = ↑f (eval 1 q)
⊢ eval 1 (map f (p + q)) = ↑f (eval 1 (p + q))
[PROOFSTEP]

| h_add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
p q : R[X]
hp : eval 1 (map f p) = ↑f (eval 1 p)
hq : eval 1 (map f q) = ↑f (eval 1 q)
⊢ eval 1 (map f (p + q)) = ↑f (eval 1 (p + q))
[PROOFSTEP]
simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
n : ℕ
r : R
⊢ eval 1 (map f (↑(monomial n) r)) = ↑f (eval 1 (↑(monomial n) r))
[PROOFSTEP]

| h_monomial n r => simp only [one_pow, mul_one, eval_monomial, map_monomial]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
n : ℕ
r : R
⊢ eval 1 (map f (↑(monomial n) r)) = ↑f (eval 1 (↑(monomial n) r))
[PROOFSTEP]
simp only [one_pow, mul_one, eval_monomial, map_monomial]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
p : R[X]
n : ℕ
⊢ eval (↑n) (map f p) = ↑f (eval (↑n) p)
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| h_monomial n r => simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
p : R[X]
n : ℕ
⊢ eval (↑n) (map f p) = ↑f (eval (↑n) p)
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| h_monomial n r => simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
n : ℕ
p q : R[X]
hp : eval (↑n) (map f p) = ↑f (eval (↑n) p)
hq : eval (↑n) (map f q) = ↑f (eval (↑n) q)
⊢ eval (↑n) (map f (p + q)) = ↑f (eval (↑n) (p + q))
[PROOFSTEP]

| h_add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q✝ r : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
n : ℕ
p q : R[X]
hp : eval (↑n) (map f p) = ↑f (eval (↑n) p)
hq : eval (↑n) (map f q) = ↑f (eval (↑n) q)
⊢ eval (↑n) (map f (p + q)) = ↑f (eval (↑n) (p + q))
[PROOFSTEP]
simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝¹ : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
n✝ n : ℕ
r : R
⊢ eval (↑n✝) (map f (↑(monomial n) r)) = ↑f (eval (↑n✝) (↑(monomial n) r))
[PROOFSTEP]

| h_monomial n r => simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝¹ : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : Semiring S
f✝ f : R →+* S
n✝ n : ℕ
r : R
⊢ eval (↑n✝) (map f (↑(monomial n) r)) = ↑f (eval (↑n✝) (↑(monomial n) r))
[PROOFSTEP]
simp only [map_natCast f, eval_monomial, map_monomial, f.map_pow, f.map_mul]
[GOAL]
R✝ : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p✝ q r : R✝[X]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
p : R[X]
i : ℤ
⊢ eval (↑i) (map f p) = ↑f (eval (↑i) p)
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| h_monomial n r => simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]
[GOAL]
R✝ : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p✝ q r : R✝[X]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
p : R[X]
i : ℤ
⊢ eval (↑i) (map f p) = ↑f (eval (↑i) p)
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
| h_monomial n r => simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]
[GOAL]
case h_add
R✝ : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p✝ q✝ r : R✝[X]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
i : ℤ
p q : R[X]
hp : eval (↑i) (map f p) = ↑f (eval (↑i) p)
hq : eval (↑i) (map f q) = ↑f (eval (↑i) q)
⊢ eval (↑i) (map f (p + q)) = ↑f (eval (↑i) (p + q))
[PROOFSTEP]

| h_add p q hp hq => simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
[GOAL]
case h_add
R✝ : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝³ : Semiring R✝
p✝ q✝ r : R✝[X]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
i : ℤ
p q : R[X]
hp : eval (↑i) (map f p) = ↑f (eval (↑i) p)
hq : eval (↑i) (map f q) = ↑f (eval (↑i) q)
⊢ eval (↑i) (map f (p + q)) = ↑f (eval (↑i) (p + q))
[PROOFSTEP]
simp only [hp, hq, Polynomial.map_add, RingHom.map_add, eval_add]
[GOAL]
case h_monomial
R✝ : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R✝
m n✝ : ℕ
inst✝³ : Semiring R✝
p q r✝ : R✝[X]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
i : ℤ
n : ℕ
r : R
⊢ eval (↑i) (map f (↑(monomial n) r)) = ↑f (eval (↑i) (↑(monomial n) r))
[PROOFSTEP]

| h_monomial n r => simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]
[GOAL]
case h_monomial
R✝ : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R✝
m n✝ : ℕ
inst✝³ : Semiring R✝
p q r✝ : R✝[X]
inst✝² : Semiring S✝
f✝ : R✝ →+* S✝
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
i : ℤ
n : ℕ
r : R
⊢ eval (↑i) (map f (↑(monomial n) r)) = ↑f (eval (↑i) (↑(monomial n) r))
[PROOFSTEP]
simp only [map_intCast, eval_monomial, map_monomial, map_pow, map_mul]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝² : Semiring R
p q r : R[X]
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
x : S
⊢ ↑g (eval₂ f x p) = eval₂ (RingHom.comp g f) (↑g x) p
[PROOFSTEP]
rw [← eval₂_map, eval₂_at_apply, eval_map]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
x✝ : R
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (comp p q) = eval₂ f (eval₂ f x q) p
[PROOFSTEP]
rw [comp, p.as_sum_range]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
x✝ : R
inst✝ : CommSemiring S
f : R →+* S
x : S
⊢ eval₂ f x (eval₂ C q (∑ i in range (natDegree p + 1), ↑(monomial i) (coeff p i))) =
    eval₂ f (eval₂ f x q) (∑ i in range (natDegree p + 1), ↑(monomial i) (coeff p i))
[PROOFSTEP]
simp [eval₂_finset_sum, eval₂_pow]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
k : ℕ
t : S
⊢ eval₂ f t ((comp p)^[k] q) = (fun x => eval₂ f x p)^[k] (eval₂ f t q)
[PROOFSTEP]
induction' k with k IH
[GOAL]
case zero
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
t : S
⊢ eval₂ f t ((comp p)^[Nat.zero] q) = (fun x => eval₂ f x p)^[Nat.zero] (eval₂ f t q)
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t ((comp p)^[k] q) = (fun x => eval₂ f x p)^[k] (eval₂ f t q)
⊢ eval₂ f t ((comp p)^[Nat.succ k] q) = (fun x => eval₂ f x p)^[Nat.succ k] (eval₂ f t q)
[PROOFSTEP]
rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : CommSemiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
⊢ eval x (comp p q) = eval (eval x q) p
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add r s hr hs => simp [add_comp, hr, hs]
| h_monomial n a => simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : CommSemiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
⊢ eval x (comp p q) = eval (eval x q) p
[PROOFSTEP]
induction p using Polynomial.induction_on' with
| h_add r s hr hs => simp [add_comp, hr, hs]
| h_monomial n a => simp
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : CommSemiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
r s : R[X]
hr : eval x (comp r q) = eval (eval x q) r
hs : eval x (comp s q) = eval (eval x q) s
⊢ eval x (comp (r + s) q) = eval (eval x q) (r + s)
[PROOFSTEP]

| h_add r s hr hs => simp [add_comp, hr, hs]
[GOAL]
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : CommSemiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
r s : R[X]
hr : eval x (comp r q) = eval (eval x q) r
hs : eval x (comp s q) = eval (eval x q) s
⊢ eval x (comp (r + s) q) = eval (eval x q) (r + s)
[PROOFSTEP]
simp [add_comp, hr, hs]
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a✝ b : R
m n✝ : ℕ
inst✝¹ : CommSemiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
n : ℕ
a : R
⊢ eval x (comp (↑(monomial n) a) q) = eval (eval x q) (↑(monomial n) a)
[PROOFSTEP]

| h_monomial n a => simp
[GOAL]
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a✝ b : R
m n✝ : ℕ
inst✝¹ : CommSemiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
n : ℕ
a : R
⊢ eval x (comp (↑(monomial n) a) q) = eval (eval x q) (↑(monomial n) a)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
p q : R[X]
H : IsRoot q a
⊢ IsRoot (p * q) a
[PROOFSTEP]
rw [IsRoot, eval_mul, IsRoot.def.1 H, mul_zero]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : CommSemiring R
p✝ q✝ : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
p q : R[X]
H : IsRoot p a
⊢ IsRoot (p * q) a
[PROOFSTEP]
rw [IsRoot, eval_mul, IsRoot.def.1 H, zero_mul]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n : ℕ
inst✝³ : CommSemiring R✝
p✝ q : R✝[X]
x✝ : R✝
inst✝² : CommSemiring S
f : R✝ →+* S
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
ι : Type u_1
s : Finset ι
p : ι → R[X]
x : R
⊢ IsRoot (∏ j in s, p j) x ↔ ∃ i, i ∈ s ∧ IsRoot (p i) x
[PROOFSTEP]
simp only [IsRoot, eval_prod, Finset.prod_eq_zero_iff]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n✝ : ℕ
inst✝² : CommSemiring R✝
p q : R✝[X]
x✝ : R✝
inst✝¹ : CommSemiring S
f : R✝ →+* S
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ eval x (∑ i in range n, X ^ i) = ∑ i in range n, x ^ i
[PROOFSTEP]
simp [eval_finset_sum]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ support (map f p) ⊆ support p
[PROOFSTEP]
intro x
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ x ∈ support (map f p) → x ∈ support p
[PROOFSTEP]
contrapose!
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
x : ℕ
⊢ ¬x ∈ support p → ¬x ∈ support (map f p)
[PROOFSTEP]
simp (config := { contextual := true })
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : Function.Injective ↑f
⊢ support (map f p) = support p
[PROOFSTEP]
simp_rw [Finset.ext_iff, mem_support_iff, coeff_map, ← map_zero f, hf.ne_iff, forall_const]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ f : R →+* S
x : R
p : R[X]
h : IsRoot p x
⊢ IsRoot (Polynomial.map f p) (↑f x)
[PROOFSTEP]
rw [IsRoot, eval_map, eval₂_hom, h.eq_zero, f.map_zero]
[GOAL]
R✝ : Type u
S : Type v
T : Type w
ι : Type y
a b : R✝
m n : ℕ
inst✝² : CommSemiring R✝
inst✝¹ : CommSemiring S
f✝ : R✝ →+* S
R : Type u_1
inst✝ : CommRing R
f : R →+* S
x : R
p : R[X]
h : IsRoot (Polynomial.map f p) (↑f x)
hf : Function.Injective ↑f
⊢ IsRoot p x
[PROOFSTEP]
rwa [IsRoot, ← (injective_iff_map_eq_zero' f).mp hf, ← eval₂_hom, ← eval_map]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝ : Ring R
p q r : R[X]
n : ℤ
x : R
⊢ eval x ↑n = ↑n
[PROOFSTEP]
simp only [← C_eq_int_cast, eval_C]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Ring R
p q r : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
x : S
⊢ eval₂ f x (-p) = -eval₂ f x p
[PROOFSTEP]
rw [eq_neg_iff_add_eq_zero, ← eval₂_add, add_left_neg, eval₂_zero]
[GOAL]
R : Type u
S✝ : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Ring R
p q r : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
x : S
⊢ eval₂ f x (p - q) = eval₂ f x p - eval₂ f x q
[PROOFSTEP]
rw [sub_eq_add_neg, eval₂_add, eval₂_neg, sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Ring R
p q r : R[X]
⊢ IsRoot (X - ↑C a) b ↔ a = b
[PROOFSTEP]
rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]
[GOAL]
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Ring R
p q r : R[X]
i : ℤ
⊢ comp (↑i) p = ↑i
[PROOFSTEP]
cases i
[GOAL]
case ofNat
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Ring R
p q r : R[X]
a✝ : ℕ
⊢ comp (↑(Int.ofNat a✝)) p = ↑(Int.ofNat a✝)
[PROOFSTEP]
simp
[GOAL]
case negSucc
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Ring R
p q r : R[X]
a✝ : ℕ
⊢ comp (↑(Int.negSucc a✝)) p = ↑(Int.negSucc a✝)
[PROOFSTEP]
simp
