[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
⊢ coeff (p + q) n = coeff p n + coeff q n
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q✝ r q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝ } + q) n = coeff { toFinsupp := toFinsupp✝ } n + coeff q n
[PROOFSTEP]
rcases q with ⟨⟩
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }) n =
    coeff { toFinsupp := toFinsupp✝¹ } n + coeff { toFinsupp := toFinsupp✝ } n
[PROOFSTEP]
simp_rw [← ofFinsupp_add, coeff]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(toFinsupp✝¹ + toFinsupp✝) n = ↑toFinsupp✝¹ n + ↑toFinsupp✝ n
[PROOFSTEP]
exact Finsupp.add_apply _ _ _
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
⊢ coeff (bit0 p) n = bit0 (coeff p n)
[PROOFSTEP]
simp [bit0]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p✝ q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
p : R[X]
n : ℕ
⊢ coeff (r • p) n = r • coeff p n
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (r • { toFinsupp := toFinsupp✝ }) n = r • coeff { toFinsupp := toFinsupp✝ } n
[PROOFSTEP]
simp_rw [← ofFinsupp_smul, coeff]
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r✝ : R[X]
inst✝ : SMulZeroClass S R
r : S
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(r • toFinsupp✝) n = r • ↑toFinsupp✝ n
[PROOFSTEP]
exact Finsupp.smul_apply _ _ _
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
⊢ support (r • p) ⊆ support p
[PROOFSTEP]
intro i hi
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : i ∈ support (r • p)
⊢ i ∈ support p
[PROOFSTEP]
simp [mem_support_iff] at hi ⊢
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : ¬r • coeff p i = 0
⊢ ¬coeff p i = 0
[PROOFSTEP]
contrapose! hi
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝² : Semiring R
p✝ q r✝ : R[X]
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
r : S
p : R[X]
i : ℕ
hi : coeff p i = 0
⊢ r • coeff p i = 0
[PROOFSTEP]
simp [hi]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝⁵ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : AddCommMonoid M
inst✝¹ : Module R A
inst✝ : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ AddHom.toFun
      { toFun := fun p => sum p fun x x_1 => ↑(f x) x_1,
        map_add' :=
          (_ :
            ∀ (p q : A[X]),
              (sum (p + q) fun x x_1 => ↑(f x) x_1) = (sum p fun x x_1 => ↑(f x) x_1) + sum q fun x x_1 => ↑(f x) x_1) }
      (c • p) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        { toFun := fun p => sum p fun x x_1 => ↑(f x) x_1,
          map_add' :=
            (_ :
              ∀ (p q : A[X]),
                (sum (p + q) fun x x_1 => ↑(f x) x_1) =
                  (sum p fun x x_1 => ↑(f x) x_1) + sum q fun x x_1 => ↑(f x) x_1) }
        p
[PROOFSTEP]
dsimp only []
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝⁵ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : AddCommMonoid M
inst✝¹ : Module R A
inst✝ : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ (sum (c • p) fun x x_1 => ↑(f x) x_1) = ↑(RingHom.id R) c • sum p fun x x_1 => ↑(f x) x_1
[PROOFSTEP]
rw [sum_eq_of_subset (f · ·) (fun n => (f n).map_zero) (support_smul c p)]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝⁵ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : AddCommMonoid M
inst✝¹ : Module R A
inst✝ : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ ∑ n in support p, ↑(f n) (coeff (c • p) n) = ↑(RingHom.id R) c • sum p fun x x_1 => ↑(f x) x_1
[PROOFSTEP]
simp only [sum_def, Finset.smul_sum, coeff_smul, LinearMap.map_smul, RingHom.id_apply]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
⊢ coeff (sum p f) n = sum p fun a b => coeff (f a b) n
[PROOFSTEP]
rcases p with
  ⟨⟩
    -- Porting note: Was `simp [Polynomial.sum, support, coeff]`.
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝¹ : Semiring R
q r : R[X]
inst✝ : Semiring S
n : ℕ
f : ℕ → R → S[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (sum { toFinsupp := toFinsupp✝ } f) n = sum { toFinsupp := toFinsupp✝ } fun a b => coeff (f a b) n
[PROOFSTEP]
simp [Polynomial.sum, support_ofFinsupp, coeff_ofFinsupp]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
n : ℕ
⊢ coeff (p * q) n = ∑ x in Nat.antidiagonal n, coeff p x.fst * coeff q x.snd
[PROOFSTEP]
rcases p with ⟨p⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r q : R[X]
n : ℕ
p : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * q) n = ∑ x in Nat.antidiagonal n, coeff { toFinsupp := p } x.fst * coeff q x.snd
[PROOFSTEP]
rcases q with ⟨q⟩
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * { toFinsupp := q }) n =
    ∑ x in Nat.antidiagonal n, coeff { toFinsupp := p } x.fst * coeff { toFinsupp := q } x.snd
[PROOFSTEP]
simp_rw [← ofFinsupp_mul, coeff]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q✝ r : R[X]
n : ℕ
p q : AddMonoidAlgebra R ℕ
⊢ ↑(p * q) n = ∑ x in Nat.antidiagonal n, ↑p x.fst * ↑q x.snd
[PROOFSTEP]
exact AddMonoidAlgebra.mul_apply_antidiagonal p q n _ Nat.mem_antidiagonal
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
⊢ coeff (p * q) 0 = coeff p 0 * coeff q 0
[PROOFSTEP]
simp [coeff_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ coeff (p * X) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ coeff (X * p) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k n : ℕ
⊢ coeff (↑C x * X ^ k) n = if n = k then x else 0
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, coeff_monomial]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k n : ℕ
⊢ (if k = n then x else 0) = if n = k then x else 0
[PROOFSTEP]
congr 1
[GOAL]
case e_c
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
k n : ℕ
⊢ (k = n) = (n = k)
[PROOFSTEP]
simp [eq_comm]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
x : R
n : ℕ
⊢ coeff (↑C x * X) n = if n = 1 then x else 0
[PROOFSTEP]
rw [← pow_one X, coeff_C_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
⊢ coeff (↑C a * p) n = a * coeff p n
[PROOFSTEP]
rcases p with ⟨p⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
p : AddMonoidAlgebra R ℕ
⊢ coeff (↑C a * { toFinsupp := p }) n = a * coeff { toFinsupp := p } n
[PROOFSTEP]
simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
p : AddMonoidAlgebra R ℕ
⊢ ↑(Finsupp.single 0 a * p) n = a * ↑p n
[PROOFSTEP]
exact AddMonoidAlgebra.single_zero_mul_apply p a n
[GOAL]
R : Type u
S : Type v
a✝ b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
f : R[X]
⊢ ↑C a * f = a • f
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
S : Type v
a✝ b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
f : R[X]
n✝ : ℕ
⊢ coeff (↑C a * f) n✝ = coeff (a • f) n✝
[PROOFSTEP]
rw [coeff_C_mul, coeff_smul, smul_eq_mul]
[GOAL]
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
a : R
⊢ coeff (p * ↑C a) n = coeff p n * a
[PROOFSTEP]
rcases p with ⟨p⟩
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
n : ℕ
a : R
p : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := p } * ↑C a) n = coeff { toFinsupp := p } n * a
[PROOFSTEP]
simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
[GOAL]
case ofFinsupp
R : Type u
S : Type v
a✝ b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r : R[X]
n : ℕ
a : R
p : AddMonoidAlgebra R ℕ
⊢ ↑(p * Finsupp.single 0 a) n = ↑p n * a
[PROOFSTEP]
exact AddMonoidAlgebra.mul_single_zero_apply p a n
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
k n : ℕ
⊢ coeff (X ^ k) n = if n = k then 1 else 0
[PROOFSTEP]
simp only [one_mul, RingHom.map_one, ← coeff_C_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ coeff (X ^ n) n = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
a b : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ support (↑C x * X ^ k + ↑C y * X ^ m) = {k, m}
[PROOFSTEP]
apply subset_antisymm (support_binomial' k m x y)
[GOAL]
R : Type u
S : Type v
a b : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ {k, m} ⊆ support (↑C x * X ^ k + ↑C y * X ^ m)
[PROOFSTEP]
simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one,
  coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add, add_zero, Ne.def, hx, hy]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) = {k, m, n}
[PROOFSTEP]
apply subset_antisymm (support_trinomial' k m n x y z)
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ {k, m, n} ⊆ support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
[PROOFSTEP]
simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one,
  coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne, if_neg hmn.ne', if_neg (hkm.trans hmn).ne,
  if_neg (hkm.trans hmn).ne', mul_zero, add_zero, zero_add, Ne.def, hx, hy, hz]
[GOAL]
R : Type u
S : Type v
a b : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m)) = 2
[PROOFSTEP]
rw [support_binomial h hx hy, card_insert_of_not_mem (mt mem_singleton.mp h), card_singleton]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)) = 3
[PROOFSTEP]
rw [support_trinomial hkm hmn hx hy hz,
  card_insert_of_not_mem (mt mem_insert.mp (not_or_of_not hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
  card_insert_of_not_mem (mt mem_singleton.mp hmn.ne), card_singleton]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ coeff (p * X ^ n) (d + n) = coeff p d
[PROOFSTEP]
rw [coeff_mul, sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
[GOAL]
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ ∀ (b : ℕ × ℕ), b ∈ Nat.antidiagonal (d + n) → b ≠ (d, n) → coeff p b.fst * coeff (X ^ n) b.snd = 0
[PROOFSTEP]
rintro ⟨i, j⟩ h1 h2
[GOAL]
case h₀.mk
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ coeff p (i, j).fst * coeff (X ^ n) (i, j).snd = 0
[PROOFSTEP]
rw [coeff_X_pow, if_neg, mul_zero]
[GOAL]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + n)
h2 : (i, j) ≠ (d, n)
⊢ ¬(i, j).snd = n
[PROOFSTEP]
rintro rfl
[GOAL]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + (i, j).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ False
[PROOFSTEP]
apply h2
[GOAL]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
d i j : ℕ
h1 : (i, j) ∈ Nat.antidiagonal (d + (i, j).snd)
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ (i, j) = (d, (i, j).snd)
[PROOFSTEP]
rw [Nat.mem_antidiagonal, add_right_cancel_iff] at h1 
[GOAL]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
d i j : ℕ
h1 : (i, j).fst = d
h2 : (i, j) ≠ (d, (i, j).snd)
⊢ (i, j) = (d, (i, j).snd)
[PROOFSTEP]
subst h1
[GOAL]
case h₀.mk.hnc
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
i j : ℕ
h2 : (i, j) ≠ ((i, j).fst, (i, j).snd)
⊢ (i, j) = ((i, j).fst, (i, j).snd)
[PROOFSTEP]
rfl
[GOAL]
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ ¬(d, n) ∈ Nat.antidiagonal (d + n) → coeff p (d, n).fst * coeff (X ^ n) (d, n).snd = 0
[PROOFSTEP]
exact fun h1 => (h1 (Nat.mem_antidiagonal.2 rfl)).elim
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ coeff (X ^ n * p) (d + n) = coeff p d
[PROOFSTEP]
rw [(commute_X_pow p n).eq, coeff_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ coeff (p * X ^ n) d = if n ≤ d then coeff p (d - n) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : n ≤ d
⊢ coeff (p * X ^ n) d = coeff p (d - n)
[PROOFSTEP]
rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
⊢ coeff (p * X ^ n) d = 0
[PROOFSTEP]
refine' (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => _)
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Nat.antidiagonal d
⊢ coeff p x.fst * coeff (X ^ n) x.snd = 0
[PROOFSTEP]
rw [coeff_X_pow, if_neg, mul_zero]
[GOAL]
case neg.hnc
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ Nat.antidiagonal d
⊢ ¬x.snd = n
[PROOFSTEP]
exact ((le_of_add_le_right (Finset.Nat.mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n d : ℕ
⊢ coeff (X ^ n * p) d = if n ≤ d then coeff p (d - n) else 0
[PROOFSTEP]
rw [(commute_X_pow p n).eq, coeff_mul_X_pow']
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
⊢ coeff (p * X) (n + 1) = coeff p n
[PROOFSTEP]
simpa only [pow_one] using coeff_mul_X_pow p 1 n
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
⊢ coeff (X * p) (n + 1) = coeff p n
[PROOFSTEP]
rw [(commute_X p).eq, coeff_mul_X]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r✝ p : R[X]
n d : ℕ
r : R
⊢ coeff (p * ↑(monomial n) r) (d + n) = coeff p d * r
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r✝ p : R[X]
n d : ℕ
r : R
⊢ coeff (↑(monomial n) r * p) (d + n) = r * coeff p d
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ IsRegular X
[PROOFSTEP]
suffices : IsLeftRegular (X : R[X])
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
this : IsLeftRegular X
⊢ IsRegular X
[PROOFSTEP]
exact ⟨this, this.right_of_commute commute_X⟩
[GOAL]
case this
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ IsLeftRegular X
[PROOFSTEP]
intro P Q (hPQ : X * P = X * Q)
[GOAL]
case this
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r P Q : R[X]
hPQ : X * P = X * Q
⊢ P = Q
[PROOFSTEP]
ext i
[GOAL]
case this.a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r P Q : R[X]
hPQ : X * P = X * Q
i : ℕ
⊢ coeff P i = coeff Q i
[PROOFSTEP]
rw [← coeff_X_mul P i, hPQ, coeff_X_mul Q i]
  -- TODO Unify this with `Polynomial.Monic.isRegular`
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ coeff ((X + ↑C r) ^ n) k = r ^ (n - k) * ↑(Nat.choose n k)
[PROOFSTEP]
rw [(commute_X (C r : R[X])).add_pow, ← lcoeff_apply, LinearMap.map_sum]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∑ i in range (n + 1), ↑(lcoeff R k) (X ^ i * ↑C r ^ (n - i) * ↑(Nat.choose n i)) = r ^ (n - k) * ↑(Nat.choose n k)
[PROOFSTEP]
simp only [one_pow, mul_one, lcoeff_apply, ← C_eq_nat_cast, ← C_pow, coeff_mul_C, Nat.cast_id]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∑ x in range (n + 1), coeff (X ^ x) k * r ^ (n - x) * ↑(Nat.choose n x) = r ^ (n - k) * ↑(Nat.choose n k)
[PROOFSTEP]
rw [Finset.sum_eq_single k, coeff_X_pow_self, one_mul]
[GOAL]
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ∀ (b : ℕ), b ∈ range (n + 1) → b ≠ k → coeff (X ^ b) k * r ^ (n - b) * ↑(Nat.choose n b) = 0
[PROOFSTEP]
intro _ _ h
[GOAL]
case h₀
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k b✝ : ℕ
a✝ : b✝ ∈ range (n + 1)
h : b✝ ≠ k
⊢ coeff (X ^ b✝) k * r ^ (n - b✝) * ↑(Nat.choose n b✝) = 0
[PROOFSTEP]
simp [coeff_X_pow, h.symm]
[GOAL]
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ ¬k ∈ range (n + 1) → coeff (X ^ k) k * r ^ (n - k) * ↑(Nat.choose n k) = 0
[PROOFSTEP]
simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]
[GOAL]
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
⊢ n + 1 ≤ k → r ^ (n - k) * ↑(Nat.choose n k) = 0
[PROOFSTEP]
intro h
[GOAL]
case h₁
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
n k : ℕ
h : n + 1 ≤ k
⊢ r ^ (n - k) * ↑(Nat.choose n k) = 0
[PROOFSTEP]
rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ coeff ((X + 1) ^ n) k = ↑(Nat.choose n k)
[PROOFSTEP]
rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ coeff ((1 + X) ^ n) k = ↑(Nat.choose n k)
[PROOFSTEP]
rw [add_comm _ X, coeff_X_add_one_pow]
[GOAL]
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ ↑C r ∣ φ ↔ ∀ (i : ℕ), r ∣ coeff φ i
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ ↑C r ∣ φ → ∀ (i : ℕ), r ∣ coeff φ i
[PROOFSTEP]
rintro ⟨φ, rfl⟩ c
[GOAL]
case mp.intro
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ
⊢ r ∣ coeff (↑C r * φ) c
[PROOFSTEP]
rw [coeff_C_mul]
[GOAL]
case mp.intro
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ
⊢ r ∣ r * coeff φ c
[PROOFSTEP]
apply dvd_mul_right
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
⊢ (∀ (i : ℕ), r ∣ coeff φ i) → ↑C r ∣ φ
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
h : ∀ (i : ℕ), r ∣ coeff φ i
⊢ ↑C r ∣ φ
[PROOFSTEP]
choose c hc using h
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
⊢ ↑C r ∣ φ
[PROOFSTEP]
classical
let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
let ψ : R[X] := ∑ i in φ.support, monomial i (c' i)
use ψ
ext i
simp only [coeff_C_mul, mem_support_iff, coeff_monomial, finset_sum_coeff, Finset.sum_ite_eq']
split_ifs with hi
· rw [hc]
· rw [Classical.not_not] at hi 
  rwa [mul_zero]
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
⊢ ↑C r ∣ φ
[PROOFSTEP]
let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
⊢ ↑C r ∣ φ
[PROOFSTEP]
let ψ : R[X] := ∑ i in φ.support, monomial i (c' i)
[GOAL]
case mpr
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
⊢ ↑C r ∣ φ
[PROOFSTEP]
use ψ
[GOAL]
case h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
⊢ φ = ↑C r * ψ
[PROOFSTEP]
ext i
[GOAL]
case h.a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
⊢ coeff φ i = coeff (↑C r * ψ) i
[PROOFSTEP]
simp only [coeff_C_mul, mem_support_iff, coeff_monomial, finset_sum_coeff, Finset.sum_ite_eq']
[GOAL]
case h.a
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
⊢ coeff φ i = r * if coeff φ i ≠ 0 then if coeff φ i ≠ 0 then c i else 0 else 0
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : coeff φ i ≠ 0
⊢ coeff φ i = r * c i
[PROOFSTEP]
rw [hc]
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : ¬coeff φ i ≠ 0
⊢ coeff φ i = r * 0
[PROOFSTEP]
rw [Classical.not_not] at hi 
[GOAL]
case neg
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r✝ : R[X]
r : R
φ : R[X]
c : ℕ → R
hc : ∀ (i : ℕ), coeff φ i = r * c i
c' : ℕ → R := fun i => if i ∈ support φ then c i else 0
ψ : R[X] := ∑ i in support φ, ↑(monomial i) (c' i)
i : ℕ
hi : coeff φ i = 0
⊢ coeff φ i = r * 0
[PROOFSTEP]
rwa [mul_zero]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r P Q : R[X]
n : ℕ
⊢ coeff (bit0 P * Q) n = 2 * coeff (P * Q) n
[PROOFSTEP]
simp [bit0, add_mul, two_mul]
[GOAL]
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r P Q : R[X]
n : ℕ
⊢ coeff (bit1 P * Q) n = 2 * coeff (P * Q) n + coeff Q n
[PROOFSTEP]
simp [bit1, add_mul, coeff_bit0_mul]
[GOAL]
R : Type u
S : Type v
a✝ b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
a : R
⊢ a • p = ↑C a * p
[PROOFSTEP]
simp [ext_iff]
[GOAL]
R✝ : Type u
S : Type v
a✝ b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
⊢ update p n a = p + ↑C (a - coeff p n) * X ^ n
[PROOFSTEP]
ext
[GOAL]
case a
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ coeff (update p n a) n✝ = coeff (p + ↑C (a - coeff p n) * X ^ n) n✝
[PROOFSTEP]
rw [coeff_update_apply, coeff_add, coeff_C_mul_X_pow]
[GOAL]
case a
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (if n✝ = n then a else coeff p n✝) = coeff p n✝ + if n✝ = n then a - coeff p n else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
h : n✝ = n
⊢ a = coeff p n✝ + (a - coeff p n)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
h : ¬n✝ = n
⊢ coeff p n✝ = coeff p n✝ + 0
[PROOFSTEP]
simp [h]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
n : ℕ
R : Type u_1
inst✝ : Semiring R
⊢ coeff (↑n) 0 = ↑n
[PROOFSTEP]
simp only [coeff_nat_cast_ite, ite_true]
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n
[PROOFSTEP]
constructor
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n
[PROOFSTEP]
intro h
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
apply_fun fun p => p.coeff 0 at h 
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : coeff (↑m) 0 = coeff (↑n) 0
⊢ m = n
[PROOFSTEP]
simpa using h
[GOAL]
case mpr
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R✝ : Type u
S : Type v
a b : R✝
n m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
⊢ ↑m = ↑m
[PROOFSTEP]
rfl
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
i : ℤ
R : Type u_1
inst✝ : Ring R
⊢ coeff (↑i) 0 = ↑i
[PROOFSTEP]
cases i
[GOAL]
case ofNat
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Ring R
a✝ : ℕ
⊢ coeff (↑(Int.ofNat a✝)) 0 = ↑(Int.ofNat a✝)
[PROOFSTEP]
simp
[GOAL]
case negSucc
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Ring R
a✝ : ℕ
⊢ coeff (↑(Int.negSucc a✝)) 0 = ↑(Int.negSucc a✝)
[PROOFSTEP]
simp
[GOAL]
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n ↔ m = n
[PROOFSTEP]
constructor
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑n → m = n
[PROOFSTEP]
intro h
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : ↑m = ↑n
⊢ m = n
[PROOFSTEP]
apply_fun fun p => p.coeff 0 at h 
[GOAL]
case mp
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : coeff (↑m) 0 = coeff (↑n) 0
⊢ m = n
[PROOFSTEP]
simpa using h
[GOAL]
case mpr
R✝ : Type u
S : Type v
a b : R✝
n✝ m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ m = n → ↑m = ↑n
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R✝ : Type u
S : Type v
a b : R✝
n m✝ : ℕ
inst✝² : Semiring R✝
p q r : R✝[X]
m : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
⊢ ↑m = ↑m
[PROOFSTEP]
rfl
