[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q f : R[X]
⊢ { toFinsupp := f.toFinsupp } = f
[PROOFSTEP]
cases f
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := { toFinsupp := toFinsupp✝ }.toFinsupp } = { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a b : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a + b } = Polynomial.add { toFinsupp := a } { toFinsupp := b }
[PROOFSTEP]
rw [add_def]
[GOAL]
R✝ : Type u
a✝ b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := -a } = Polynomial.neg { toFinsupp := a }
[PROOFSTEP]
rw [neg_def]
[GOAL]
R✝ : Type u
a✝ b✝ : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a b : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }
[PROOFSTEP]
rw [sub_eq_add_neg, ofFinsupp_add, ofFinsupp_neg]
[GOAL]
R✝ : Type u
a✝ b✝ : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a b : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a } + -{ toFinsupp := b } = { toFinsupp := a } - { toFinsupp := b }
[PROOFSTEP]
rfl
[GOAL]
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a b : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a * b } = Polynomial.mul { toFinsupp := a } { toFinsupp := b }
[PROOFSTEP]
rw [mul_def]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := a ^ n } = { toFinsupp := a } ^ n
[PROOFSTEP]
change _ = npowRec n _
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
[PROOFSTEP]
induction n with
| zero => simp [npowRec]
| succ n n_ih => simp [npowRec, n_ih, pow_succ]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
[PROOFSTEP]
induction n with
| zero => simp [npowRec]
| succ n n_ih => simp [npowRec, n_ih, pow_succ]
[GOAL]
case zero
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a ^ Nat.zero } = npowRec Nat.zero { toFinsupp := a }
[PROOFSTEP]

| zero => simp [npowRec]
[GOAL]
case zero
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a ^ Nat.zero } = npowRec Nat.zero { toFinsupp := a }
[PROOFSTEP]
simp [npowRec]
[GOAL]
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := a ^ Nat.succ n } = npowRec (Nat.succ n) { toFinsupp := a }
[PROOFSTEP]

| succ n n_ih => simp [npowRec, n_ih, pow_succ]
[GOAL]
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := a ^ Nat.succ n } = npowRec (Nat.succ n) { toFinsupp := a }
[PROOFSTEP]
simp [npowRec, n_ih, pow_succ]
[GOAL]
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
p q a b : R[X]
⊢ (a + b).toFinsupp = a.toFinsupp + b.toFinsupp
[PROOFSTEP]
cases a
[GOAL]
case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q b : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } + b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp + b.toFinsupp
[PROOFSTEP]
cases b
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp + { toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
rw [← ofFinsupp_add]
[GOAL]
R✝ : Type u
a✝ b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a : R[X]
⊢ (-a).toFinsupp = -a.toFinsupp
[PROOFSTEP]
cases a
[GOAL]
case ofFinsupp
R✝ : Type u
a b : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (-{ toFinsupp := toFinsupp✝ }).toFinsupp = -{ toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
rw [← ofFinsupp_neg]
[GOAL]
R✝ : Type u
a✝ b✝ : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp - b.toFinsupp
[PROOFSTEP]
rw [sub_eq_add_neg, ← toFinsupp_neg, ← toFinsupp_add]
[GOAL]
R✝ : Type u
a✝ b✝ : R✝
m n : ℕ
inst✝¹ : Semiring R✝
p q : R✝[X]
R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = (a + -b).toFinsupp
[PROOFSTEP]
rfl
[GOAL]
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝ : Semiring R
p q a b : R[X]
⊢ (a * b).toFinsupp = a.toFinsupp * b.toFinsupp
[PROOFSTEP]
cases a
[GOAL]
case ofFinsupp
R : Type u
a b✝ : R
m n : ℕ
inst✝ : Semiring R
p q b : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } * b).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp * b.toFinsupp
[PROOFSTEP]
cases b
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝¹ }.toFinsupp * { toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
rw [← ofFinsupp_mul]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q a : R[X]
n : ℕ
⊢ (a ^ n).toFinsupp = a.toFinsupp ^ n
[PROOFSTEP]
cases a
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } ^ n).toFinsupp = { toFinsupp := toFinsupp✝ }.toFinsupp ^ n
[PROOFSTEP]
rw [← ofFinsupp_pow]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q a : R[X]
⊢ a.toFinsupp = 0 ↔ a = 0
[PROOFSTEP]
rw [← toFinsupp_zero, toFinsupp_inj]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q a : R[X]
⊢ a.toFinsupp = 1 ↔ a = 1
[PROOFSTEP]
rw [← toFinsupp_one, toFinsupp_inj]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a } = 0 ↔ a = 0
[PROOFSTEP]
rw [← ofFinsupp_zero, ofFinsupp_inj]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := a } = 1 ↔ a = 1
[PROOFSTEP]
rw [← ofFinsupp_one, ofFinsupp_inj]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S₁ : Type ?u.114071
S₂ : Type ?u.114238
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : SMulCommClass S₁ S₂ R
⊢ ∀ (m : S₁) (n : S₂) (a : R[X]), m • n • a = n • m • a
[PROOFSTEP]
rintro m n ⟨f⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝³ : Semiring R
p q : R[X]
S₁ : Type ?u.114071
S₂ : Type ?u.114238
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : SMulCommClass S₁ S₂ R
m : S₁
n : S₂
f : AddMonoidAlgebra R ℕ
⊢ m • n • { toFinsupp := f } = n • m • { toFinsupp := f }
[PROOFSTEP]
simp_rw [← ofFinsupp_smul, smul_comm m n f]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝⁴ : Semiring R
p q : R[X]
S₁ : Type ?u.117123
S₂ : Type ?u.117122
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : IsScalarTower S₁ S₂ R
⊢ ∀ (x : S₁) (y : S₂) (z : R[X]), (x • y) • z = x • y • z
[PROOFSTEP]
rintro _ _ ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝⁴ : Semiring R
p q : R[X]
S₁ : Type ?u.117123
S₂ : Type ?u.117122
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : IsScalarTower S₁ S₂ R
x✝ : S₁
y✝ : S₂
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (x✝ • y✝) • { toFinsupp := toFinsupp✝ } = x✝ • y✝ • { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
simp_rw [← ofFinsupp_smul, smul_assoc]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst✝² : Semiring K
inst✝¹ : DistribSMul α K
inst✝ : IsScalarTower α K K
⊢ ∀ (x : α) (y z : K[X]), (x • y) • z = x • y • z
[PROOFSTEP]
rintro _ ⟨⟩ ⟨⟩
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst✝² : Semiring K
inst✝¹ : DistribSMul α K
inst✝ : IsScalarTower α K K
x✝ : α
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra K ℕ
⊢ (x✝ • { toFinsupp := toFinsupp✝¹ }) • { toFinsupp := toFinsupp✝ } =
    x✝ • { toFinsupp := toFinsupp✝¹ } • { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type ?u.129006
inst✝² : SMulZeroClass S R
inst✝¹ : SMulZeroClass Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
⊢ ∀ (m : S) (a : R[X]), MulOpposite.op m • a = m • a
[PROOFSTEP]
rintro _ ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type ?u.129006
inst✝² : SMulZeroClass S R
inst✝¹ : SMulZeroClass Sᵐᵒᵖ R
inst✝ : IsCentralScalar S R
m✝ : S
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ MulOpposite.op m✝ • { toFinsupp := toFinsupp✝ } = m✝ • { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
simp_rw [← ofFinsupp_smul, op_smul_eq_smul]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Subsingleton R
src✝ : Inhabited R[X] := inhabited
⊢ ∀ (a : R[X]), a = default
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Subsingleton R
src✝ : Inhabited R[X] := inhabited
x : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := x } = default
[PROOFSTEP]
refine' congr_arg ofFinsupp _
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Subsingleton R
src✝ : Inhabited R[X] := inhabited
x : AddMonoidAlgebra R ℕ
⊢ x = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
p : AddMonoidAlgebra R ℕ
⊢ support { toFinsupp := p } = p.support
[PROOFSTEP]
rw [support]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
⊢ p.toFinsupp.support = support p
[PROOFSTEP]
rw [support]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ support p = ∅ ↔ p = 0
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support { toFinsupp := toFinsupp✝ } = ∅ ↔ { toFinsupp := toFinsupp✝ } = 0
[PROOFSTEP]
simp [support]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ Finset.card (support p) = 0 ↔ p = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
x y : R
⊢ (fun t => { toFinsupp := Finsupp.single n t }) (x + y) =
    (fun t => { toFinsupp := Finsupp.single n t }) x + (fun t => { toFinsupp := Finsupp.single n t }) y
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
x y : R
⊢ { toFinsupp := Finsupp.single n x + Finsupp.single n y } =
    { toFinsupp := Finsupp.single n x } + { toFinsupp := Finsupp.single n y }
[PROOFSTEP]
rw [ofFinsupp_add]
  -- Porting note: Was `simp [← ofFinsupp_smul]`.
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r x : R
⊢ AddHom.toFun
      { toFun := fun t => { toFinsupp := Finsupp.single n t },
        map_add' :=
          (_ :
            ∀ (x y : R),
              (fun t => { toFinsupp := Finsupp.single n t }) (x + y) =
                (fun t => { toFinsupp := Finsupp.single n t }) x + (fun t => { toFinsupp := Finsupp.single n t }) y) }
      (r • x) =
    ↑(RingHom.id R) r •
      AddHom.toFun
        { toFun := fun t => { toFinsupp := Finsupp.single n t },
          map_add' :=
            (_ :
              ∀ (x y : R),
                (fun t => { toFinsupp := Finsupp.single n t }) (x + y) =
                  (fun t => { toFinsupp := Finsupp.single n t }) x + (fun t => { toFinsupp := Finsupp.single n t }) y) }
        x
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r x : R
⊢ { toFinsupp := Finsupp.single n (r * x) } = r • { toFinsupp := Finsupp.single n x }
[PROOFSTEP]
rw [← ofFinsupp_smul, smul_single']
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ (↑(monomial n) r).toFinsupp = Finsupp.single n r
[PROOFSTEP]
simp [monomial]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ { toFinsupp := Finsupp.single n r } = ↑(monomial n) r
[PROOFSTEP]
simp [monomial]
[GOAL]
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n m : ℕ
r s : R
⊢ (↑(monomial n) r * ↑(monomial m) s).toFinsupp = (↑(monomial (n + m)) (r * s)).toFinsupp
[PROOFSTEP]
simp only [toFinsupp_monomial, toFinsupp_mul, AddMonoidAlgebra.single_mul_single]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
⊢ ↑(monomial n) r ^ k = ↑(monomial (n * k)) (r ^ k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ ↑(monomial n) r ^ Nat.zero = ↑(monomial (n * Nat.zero)) (r ^ Nat.zero)
[PROOFSTEP]
simp [pow_zero, monomial_zero_one]
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
ih : ↑(monomial n) r ^ k = ↑(monomial (n * k)) (r ^ k)
⊢ ↑(monomial n) r ^ Nat.succ k = ↑(monomial (n * Nat.succ k)) (r ^ Nat.succ k)
[PROOFSTEP]
simp [pow_succ, ih, monomial_mul_monomial, Nat.succ_eq_add_one, mul_add, add_comm]
[GOAL]
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : SMulZeroClass S R
a : S
n : ℕ
b : R
⊢ (a • ↑(monomial n) b).toFinsupp = (↑(monomial n) (a • b)).toFinsupp
[PROOFSTEP]
simp
[GOAL]
R : Type u
a✝ b✝ : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : SMulZeroClass S R
a : S
n : ℕ
b : R
⊢ a • Finsupp.single n b = Finsupp.single n (a • b)
[PROOFSTEP]
rw [smul_single]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ support (p + q) ⊆ support p ∪ support q
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support ({ toFinsupp := toFinsupp✝ } + q) ⊆ support { toFinsupp := toFinsupp✝ } ∪ support q
[PROOFSTEP]
rcases q with ⟨⟩
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support ({ toFinsupp := toFinsupp✝¹ } + { toFinsupp := toFinsupp✝ }) ⊆
    support { toFinsupp := toFinsupp✝¹ } ∪ support { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
simp only [← ofFinsupp_add, support]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (toFinsupp✝¹ + toFinsupp✝).support ⊆ toFinsupp✝¹.support ∪ toFinsupp✝.support
[PROOFSTEP]
exact support_add
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
src✝ : R →ₗ[R] R[X] := monomial 0
⊢ AddHom.toFun src✝.toAddHom 1 = 1
[PROOFSTEP]
simp [monomial_zero_one]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
src✝ : R →ₗ[R] R[X] := monomial 0
⊢ ∀ (x y : R),
    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : 1 = 1) } (x * y) =
      OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : 1 = 1) } x *
        OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : 1 = 1) } y
[PROOFSTEP]
simp [monomial_mul_monomial]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
src✝ : R →ₗ[R] R[X] := monomial 0
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : 1 = 1) },
          map_mul' := (_ : ∀ (a a_1 : R), ↑(monomial 0) (a * a_1) = ↑(monomial 0) a * ↑(monomial 0) a_1) })
      0 =
    0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑C 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑C (bit1 a) = bit1 (↑C a)
[PROOFSTEP]
simp [bit1, C_bit0]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑C a * ↑(monomial n) b = ↑(monomial n) (a * b)
[PROOFSTEP]
simp only [← monomial_zero_left, monomial_mul_monomial, zero_add]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑(monomial n) a * ↑C b = ↑(monomial n) (a * b)
[PROOFSTEP]
simp only [← monomial_zero_left, monomial_mul_monomial, add_zero]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ ↑(monomial n) 1 = X ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑(monomial Nat.zero) 1 = X ^ Nat.zero
[PROOFSTEP]
simp [monomial_zero_one]
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : ↑(monomial n) 1 = X ^ n
⊢ ↑(monomial (Nat.succ n)) 1 = X ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, add_comm, one_mul]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ X * p = p * X
[PROOFSTEP]
rcases p with
  ⟨⟩
    -- Porting note: `ofFinsupp.injEq` is required.
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ X * { toFinsupp := toFinsupp✝ } = { toFinsupp := toFinsupp✝ } * X
[PROOFSTEP]
simp only [X, ← ofFinsupp_single, ← ofFinsupp_mul, LinearMap.coe_mk, ofFinsupp.injEq]
  -- Porting note: Was `ext`.
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ Finsupp.single 1 1 * toFinsupp✝ = toFinsupp✝ * Finsupp.single 1 1
[PROOFSTEP]
refine Finsupp.ext fun _ => ?_
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
x✝ : ℕ
⊢ ↑(Finsupp.single 1 1 * toFinsupp✝) x✝ = ↑(toFinsupp✝ * Finsupp.single 1 1) x✝
[PROOFSTEP]
simp [AddMonoidAlgebra.mul_apply, AddMonoidAlgebra.sum_single_index, add_comm]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ X ^ n * p = p * X ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ X ^ Nat.zero * p = p * X ^ Nat.zero
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ Nat.succ n * p = p * X ^ Nat.succ n
[PROOFSTEP]
conv_lhs => rw [pow_succ']
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
| X ^ Nat.succ n * p
[PROOFSTEP]
rw [pow_succ']
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
| X ^ Nat.succ n * p
[PROOFSTEP]
rw [pow_succ']
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
| X ^ Nat.succ n * p
[PROOFSTEP]
rw [pow_succ']
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * X * p = p * X ^ Nat.succ n
[PROOFSTEP]
rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ']
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ p * X ^ n * q = p * q * X ^ n
[PROOFSTEP]
rw [mul_assoc, X_pow_mul, ← mul_assoc]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ ↑(monomial n) r * X = ↑(monomial (n + 1)) r
[PROOFSTEP]
erw [monomial_mul_monomial, mul_one]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
⊢ ↑(monomial n) r * X ^ k = ↑(monomial (n + k)) r
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ ↑(monomial n) r * X ^ Nat.zero = ↑(monomial (n + Nat.zero)) r
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
k : ℕ
ih : ↑(monomial n) r * X ^ k = ↑(monomial (n + k)) r
⊢ ↑(monomial n) r * X ^ Nat.succ k = ↑(monomial (n + Nat.succ k)) r
[PROOFSTEP]
simp [ih, pow_succ', ← mul_assoc, add_assoc]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
r : R
⊢ X * ↑(monomial n) r = ↑(monomial (n + 1)) r
[PROOFSTEP]
rw [X_mul, monomial_mul_X]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
k n : ℕ
r : R
⊢ X ^ k * ↑(monomial n) r = ↑(monomial (n + k)) r
[PROOFSTEP]
rw [X_pow_mul, monomial_mul_X_pow]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
p : AddMonoidAlgebra R ℕ
⊢ coeff { toFinsupp := p } = ↑p
[PROOFSTEP]
rw [coeff]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ Injective coeff
[PROOFSTEP]
rintro ⟨p⟩
  ⟨q⟩
      -- Porting note: `ofFinsupp.injEq` is required.
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ : R[X]
p q : AddMonoidAlgebra R ℕ
⊢ coeff { toFinsupp := p } = coeff { toFinsupp := q } → { toFinsupp := p } = { toFinsupp := q }
[PROOFSTEP]
simp only [coeff, FunLike.coe_fn_eq, imp_self, ofFinsupp.injEq]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q f : R[X]
i : ℕ
⊢ ↑f.toFinsupp i = coeff f i
[PROOFSTEP]
cases f
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑{ toFinsupp := toFinsupp✝ }.toFinsupp i = coeff { toFinsupp := toFinsupp✝ } i
[PROOFSTEP]
rfl
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (↑(monomial n) a) m = if n = m then a else 0
[PROOFSTEP]
rw [← ofFinsupp_single]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff { toFinsupp := Finsupp.single n a } m = if n = m then a else 0
[PROOFSTEP]
simp only [coeff, LinearMap.coe_mk]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑(Finsupp.single n a) m = if n = m then a else 0
[PROOFSTEP]
rw [Finsupp.single_apply]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff 1 0 = 1
[PROOFSTEP]
rw [← monomial_zero_one, coeff_monomial]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (if 0 = 0 then 1 else 0) = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (↑(monomial (n + 1)) a) 0 = 0
[PROOFSTEP]
simp [coeff_monomial]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : n ≠ 1
⊢ coeff X n = 0
[PROOFSTEP]
rw [coeff_X, if_neg hn.symm]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ n ∈ support p ↔ coeff p n ≠ 0
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ n ∈ support { toFinsupp := toFinsupp✝ } ↔ coeff { toFinsupp := toFinsupp✝ } n ≠ 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ¬n ∈ support p ↔ coeff p n = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (↑C a) n = if n = 0 then a else 0
[PROOFSTEP]
convert coeff_monomial (a := a) (m := n) (n := 0) using 2
[GOAL]
case h.e'_3.h₁.a
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ n = 0 ↔ 0 = n
[PROOFSTEP]
simp [eq_comm]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
h : n ≠ 0
⊢ coeff (↑C a) n = 0
[PROOFSTEP]
rw [coeff_C, if_neg h]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
r : R
n : ℕ
⊢ coeff (↑C r) (n + 1) = 0
[PROOFSTEP]
simp [coeff_C]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (↑m) n = ↑(if n = 0 then m else 0)
[PROOFSTEP]
simp only [← C_eq_nat_cast, coeff_C, Nat.cast_ite, Nat.cast_zero]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ ↑C a * X ^ (n + 1) = ↑(monomial (n + 1)) a
[PROOFSTEP]
rw [pow_succ', ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
a : R
n : ℕ
⊢ (↑C a * X ^ n).toFinsupp = Finsupp.single n a
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, toFinsupp_monomial]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ↑C a * X = ↑(monomial 1) a
[PROOFSTEP]
rw [← C_mul_X_pow_eq_monomial, pow_one]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : R
⊢ (↑C a * X).toFinsupp = Finsupp.single 1 a
[PROOFSTEP]
rw [C_mul_X_eq_monomial, toFinsupp_monomial]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ Subsingleton R → Subsingleton R[X]
[PROOFSTEP]
intro
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a✝ : Subsingleton R
⊢ Subsingleton R[X]
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (∀ (f g : R[X]), f = g) ↔ ∀ (a b : R), a = b
[PROOFSTEP]
simpa only [← subsingleton_iff] using subsingleton_iff_subsingleton
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ p q : R[X]
⊢ p = q ↔ ∀ (n : ℕ), coeff p n = coeff q n
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q✝ q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝ } = q ↔ ∀ (n : ℕ), coeff { toFinsupp := toFinsupp✝ } n = coeff q n
[PROOFSTEP]
rcases q with
  ⟨⟩
    -- Porting note: Was `simp [coeff, FunLike.ext_iff]`
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp✝¹ } = { toFinsupp := toFinsupp✝ } ↔
    ∀ (n : ℕ), coeff { toFinsupp := toFinsupp✝¹ } n = coeff { toFinsupp := toFinsupp✝ } n
[PROOFSTEP]
simp [coeff]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ toFinsupp✝¹ = toFinsupp✝ ↔ ∀ (n : ℕ), ↑toFinsupp✝¹ n = ↑toFinsupp✝ n
[PROOFSTEP]
exact FunLike.ext_iff (F := ℕ →₀ R)
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a} = ⊤
[PROOFSTEP]
apply top_unique
[GOAL]
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ ⊤ ≤ AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a}
[PROOFSTEP]
rw [← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv, ← Finsupp.add_closure_setOf_eq_single,
  AddMonoidHom.map_mclosure]
[GOAL]
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ AddSubmonoid.closure
      (↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ''
        {f | ∃ a b, f = Finsupp.single a b}) ≤
    AddSubmonoid.closure {p | ∃ n a, p = ↑(monomial n) a}
[PROOFSTEP]
refine' AddSubmonoid.closure_mono (Set.image_subset_iff.2 _)
[GOAL]
case h
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ {f | ∃ a b, f = Finsupp.single a b} ⊆
    ↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ⁻¹'
      {p | ∃ n a, p = ↑(monomial n) a}
[PROOFSTEP]
rintro _ ⟨n, a, rfl⟩
[GOAL]
case h.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ Finsupp.single n a ∈
    ↑(AddEquiv.toAddMonoidHom (RingEquiv.toAddEquiv (RingEquiv.symm (toFinsuppIso R)))) ⁻¹'
      {p | ∃ n a, p = ↑(monomial n) a}
[PROOFSTEP]
exact ⟨n, a, Polynomial.ofFinsupp_single _ _⟩
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
M : Type u_1
inst✝ : AddMonoid M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
⊢ Set.EqOn ↑f ↑g {p | ∃ n a, p = ↑(monomial n) a}
[PROOFSTEP]
rintro p ⟨n, a, rfl⟩
[GOAL]
case intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
M : Type u_1
inst✝ : AddMonoid M
f g : R[X] →+ M
h : ∀ (n : ℕ) (a : R), ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
n : ℕ
a : R
⊢ ↑f (↑(monomial n) a) = ↑g (↑(monomial n) a)
[PROOFSTEP]
exact h n a
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q : R[X]
h : 0 = 1
p : R[X]
⊢ p = 0
[PROOFSTEP]
rw [← one_smul R p, ← h, zero_smul]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
H : a ≠ 0
⊢ support (↑(monomial n) a) = {n}
[PROOFSTEP]
rw [← ofFinsupp_single, support]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
H : a ≠ 0
⊢ (match { toFinsupp := Finsupp.single n a } with
    | { toFinsupp := p } => p.support) =
    {n}
[PROOFSTEP]
exact Finsupp.support_single_ne_zero _ H
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ support (↑(monomial n) a) ⊆ {n}
[PROOFSTEP]
rw [← ofFinsupp_single, support]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ (match { toFinsupp := Finsupp.single n a } with
    | { toFinsupp := p } => p.support) ⊆
    {n}
[PROOFSTEP]
exact Finsupp.support_single_subset
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
c : R
h : c ≠ 0
⊢ support (↑C c * X) = {1}
[PROOFSTEP]
rw [C_mul_X_eq_monomial, support_monomial 1 h]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
c : R
⊢ support (↑C c * X) ⊆ {1}
[PROOFSTEP]
simpa only [C_mul_X_eq_monomial] using support_monomial' 1 c
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
c : R
h : c ≠ 0
⊢ support (↑C c * X ^ n) = {n}
[PROOFSTEP]
rw [C_mul_X_pow_eq_monomial, support_monomial n h]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
c : R
⊢ support (↑C c * X ^ n) ⊆ {n}
[PROOFSTEP]
simpa only [C_mul_X_pow_eq_monomial] using support_monomial' n c
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ X ^ n = ↑(monomial n) 1
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ X ^ Nat.zero = ↑(monomial Nat.zero) 1
[PROOFSTEP]
rw [pow_zero, monomial_zero_one]
[GOAL]
case succ
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
hn : X ^ n = ↑(monomial n) 1
⊢ X ^ Nat.succ n = ↑(monomial (Nat.succ n)) 1
[PROOFSTEP]
rw [pow_succ', hn, X, monomial_mul_monomial, one_mul]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (X ^ n).toFinsupp = Finsupp.single n 1
[PROOFSTEP]
rw [X_pow_eq_monomial, toFinsupp_monomial]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ a • X ^ n = ↑(monomial n) a
[PROOFSTEP]
rw [X_pow_eq_monomial, smul_monomial, smul_eq_mul, mul_one]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
H : ¬1 = 0
n : ℕ
⊢ support (X ^ n) = {n}
[PROOFSTEP]
convert support_monomial n H
[GOAL]
case h.e'_2.h.e'_3
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
H : ¬1 = 0
n : ℕ
⊢ X ^ n = ↑(monomial n) 1
[PROOFSTEP]
exact X_pow_eq_monomial n
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
H : 1 = 0
⊢ support X = ∅
[PROOFSTEP]
rw [X, H, monomial_zero_right, support_zero]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
H : ¬1 = 0
⊢ support X = {1}
[PROOFSTEP]
rw [← pow_one X, support_X_pow H 1]
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
a : R
ha : a ≠ 0
i j : ℕ
⊢ ↑(monomial i) a = ↑(monomial j) a ↔ i = j
[PROOFSTEP]
rw [← ofFinsupp_single, ← ofFinsupp_single, ofFinsupp.injEq, Finsupp.single_left_inj ha]
[GOAL]
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ ↑C u * X ^ k + ↑C v * X ^ l = ↑C u * X ^ m + ↑C v * X ^ n ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
[PROOFSTEP]
simp_rw [C_mul_X_pow_eq_monomial, ← toFinsupp_inj, toFinsupp_add, toFinsupp_monomial]
[GOAL]
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
k l m n : ℕ
u v : R
hu : u ≠ 0
hv : v ≠ 0
⊢ Finsupp.single k u + Finsupp.single l v = Finsupp.single m u + Finsupp.single n v ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n
[PROOFSTEP]
exact Finsupp.single_add_single_eq_single_add_single hu hv
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ p * q = ∑ i in support p, sum q fun j a => ↑(monomial (i + j)) (coeff p i * a)
[PROOFSTEP]
apply toFinsupp_injective
[GOAL]
case a
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).toFinsupp = (∑ i in support p, sum q fun j a => ↑(monomial (i + j)) (coeff p i * a)).toFinsupp
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case a.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
q : R[X]
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝ } * q).toFinsupp =
    (∑ i in support { toFinsupp := toFinsupp✝ },
        sum q fun j a => ↑(monomial (i + j)) (coeff { toFinsupp := toFinsupp✝ } i * a)).toFinsupp
[PROOFSTEP]
rcases q with ⟨⟩
[GOAL]
case a.ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ({ toFinsupp := toFinsupp✝¹ } * { toFinsupp := toFinsupp✝ }).toFinsupp =
    (∑ i in support { toFinsupp := toFinsupp✝¹ },
        sum { toFinsupp := toFinsupp✝ } fun j a =>
          ↑(monomial (i + j)) (coeff { toFinsupp := toFinsupp✝¹ } i * a)).toFinsupp
[PROOFSTEP]
simp [support, sum, coeff, toFinsupp_sum]
[GOAL]
case a.ofFinsupp.ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ toFinsupp✝¹ * toFinsupp✝ =
    ∑ x in toFinsupp✝¹.support, ∑ x_1 in toFinsupp✝.support, Finsupp.single (x + x_1) (↑toFinsupp✝¹ x * ↑toFinsupp✝ x_1)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
f : ℕ → R → S
⊢ sum 0 f = 0
[PROOFSTEP]
simp [sum]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ sum (p + q) f = sum p f + sum q f
[PROOFSTEP]
rw [show p + q = ⟨p.toFinsupp + q.toFinsupp⟩ from add_def p q]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q✝ : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p q : R[X]
f : ℕ → R → S
hf : ∀ (i : ℕ), f i 0 = 0
h_add : ∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂
⊢ sum { toFinsupp := p.toFinsupp + q.toFinsupp } f = sum p f + sum q f
[PROOFSTEP]
exact Finsupp.sum_add_index (fun i _ ↦ hf i) (fun a _ b₁ b₂ ↦ h_add a b₁ b₂)
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p✝ q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
p : R[X]
f g : ℕ → R → S
⊢ sum p (f + g) = sum p f + sum p g
[PROOFSTEP]
simp [sum_def, Finset.sum_add_distrib]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
⊢ (sum p fun n a => ↑C a * X ^ n) = p
[PROOFSTEP]
simp_rw [C_mul_X_pow_eq_monomial, sum_monomial_eq]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ (erase n p).toFinsupp = Finsupp.erase n p.toFinsupp
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (erase n { toFinsupp := toFinsupp✝ }).toFinsupp = Finsupp.erase n { toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
simp only [erase_def]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q : R[X]
p : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := Finsupp.erase n p } = erase n { toFinsupp := p }
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case mk
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
support✝ : Finset ℕ
toFun✝ : ℕ → R
mem_support_toFun✝ : ∀ (a : ℕ), a ∈ support✝ ↔ toFun✝ a ≠ 0
⊢ { toFinsupp := Finsupp.erase n { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } } =
    erase n { toFinsupp := { support := support✝, toFun := toFun✝, mem_support_toFun := mem_support_toFun✝ } }
[PROOFSTEP]
simp only [erase_def]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ support (erase n p) = Finset.erase (support p) n
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (erase n { toFinsupp := toFinsupp✝ }) = Finset.erase (support { toFinsupp := toFinsupp✝ }) n
[PROOFSTEP]
simp only [support, erase_def, Finsupp.support_erase]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ (↑(monomial n) (coeff p n) + erase n p).toFinsupp = p.toFinsupp
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (↑(monomial n) (coeff { toFinsupp := toFinsupp✝ } n) + erase n { toFinsupp := toFinsupp✝ }).toFinsupp =
    { toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
rw [toFinsupp_add, toFinsupp_monomial, toFinsupp_erase, coeff]
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ Finsupp.single n
        ((match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝ } with
          | { toFinsupp := p } => ↑p)
          n) +
      Finsupp.erase n { toFinsupp := toFinsupp✝ }.toFinsupp =
    { toFinsupp := toFinsupp✝ }.toFinsupp
[PROOFSTEP]
exact Finsupp.single_add_erase _ _
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n i : ℕ
⊢ coeff (erase n p) i = if i = n then 0 else coeff p i
[PROOFSTEP]
rcases p with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (erase n { toFinsupp := toFinsupp✝ }) i = if i = n then 0 else coeff { toFinsupp := toFinsupp✝ } i
[PROOFSTEP]
simp only [erase_def, coeff]
  -- Porting note: Was `convert rfl`.
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n i : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ ↑(Finsupp.erase n toFinsupp✝) i = if i = n then 0 else ↑toFinsupp✝ i
[PROOFSTEP]
exact ite_congr rfl (fun _ => rfl) (fun _ => rfl)
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
⊢ (erase n 0).toFinsupp = 0.toFinsupp
[PROOFSTEP]
simp
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
⊢ (erase n (↑(monomial n) a)).toFinsupp = 0.toFinsupp
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ coeff (erase n p) n = 0
[PROOFSTEP]
simp [coeff_erase]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n i : ℕ
h : i ≠ n
⊢ coeff (erase n p) i = coeff p i
[PROOFSTEP]
simp [coeff_erase, h]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
⊢ coeff (update p n a) = Function.update (coeff p) n a
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
x✝ : ℕ
⊢ coeff (update p n a) x✝ = Function.update (coeff p) n a x✝
[PROOFSTEP]
cases p
[GOAL]
case h.ofFinsupp
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n : ℕ
a : R
x✝ : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (update { toFinsupp := toFinsupp✝ } n a) x✝ = Function.update (coeff { toFinsupp := toFinsupp✝ }) n a x✝
[PROOFSTEP]
simp only [coeff, update, Function.update_apply, coe_update]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
i : ℕ
⊢ coeff (update p n a) i = if i = n then a else coeff p i
[PROOFSTEP]
rw [coeff_update, Function.update_apply]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
⊢ coeff (update p n a) n = a
[PROOFSTEP]
rw [p.coeff_update_apply, if_pos rfl]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
i : ℕ
h : i ≠ n
⊢ coeff (update p n a) i = coeff p i
[PROOFSTEP]
rw [p.coeff_update_apply, if_neg h]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ update p n 0 = erase n p
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
a b : R
m n✝¹ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n n✝ : ℕ
⊢ coeff (update p n 0) n✝ = coeff (erase n p) n✝
[PROOFSTEP]
rw [coeff_update_apply, coeff_erase]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ support (update p n a) = if a = 0 then Finset.erase (support p) n else insert n (support p)
[PROOFSTEP]
classical
cases p
simp only [support, update, Finsupp.support_update]
congr
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
⊢ support (update p n a) = if a = 0 then Finset.erase (support p) n else insert n (support p)
[PROOFSTEP]
cases p
[GOAL]
case ofFinsupp
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (update { toFinsupp := toFinsupp✝ } n a) =
    if a = 0 then Finset.erase (support { toFinsupp := toFinsupp✝ }) n
    else insert n (support { toFinsupp := toFinsupp✝ })
[PROOFSTEP]
simp only [support, update, Finsupp.support_update]
[GOAL]
case ofFinsupp
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
n : ℕ
a : R
inst✝ : Decidable (a = 0)
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (if a = 0 then Finset.erase toFinsupp✝.support n else insert n toFinsupp✝.support) =
    if a = 0 then Finset.erase toFinsupp✝.support n else insert n toFinsupp✝.support
[PROOFSTEP]
congr
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
⊢ support (update p n 0) = Finset.erase (support p) n
[PROOFSTEP]
rw [update_zero_eq_erase, support_erase]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ support (update p n a) = insert n (support p)
[PROOFSTEP]
classical rw [support_update, if_neg ha]
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ support (update p n a) = insert n (support p)
[PROOFSTEP]
rw [support_update, if_neg ha]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ coeff (-p) n = -coeff p n
[PROOFSTEP]
rcases p with
  ⟨⟩
    -- Porting note: The last rule should be `apply`ed.
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff (-{ toFinsupp := toFinsupp✝ }) n = -coeff { toFinsupp := toFinsupp✝ } n
[PROOFSTEP]
rw [← ofFinsupp_neg, coeff, coeff]
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (match (motive := R[X] → ℕ → R) { toFinsupp := -toFinsupp✝ } with
      | { toFinsupp := p } => ↑p)
      n =
    -(match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝ } with
        | { toFinsupp := p } => ↑p)
        n
[PROOFSTEP]
apply Finsupp.neg_apply
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring 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
a b : R
m n✝ : ℕ
inst✝ : Ring R
q : R[X]
n : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝ } - q) n = coeff { toFinsupp := toFinsupp✝ } n - coeff q n
[PROOFSTEP]
rcases q with
  ⟨⟩
    -- Porting note: The last rule should be `apply`ed.
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ coeff ({ toFinsupp := toFinsupp✝¹ } - { toFinsupp := toFinsupp✝ }) n =
    coeff { toFinsupp := toFinsupp✝¹ } n - coeff { toFinsupp := toFinsupp✝ } n
[PROOFSTEP]
rw [← ofFinsupp_sub, coeff, coeff, coeff]
[GOAL]
case ofFinsupp.ofFinsupp
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝¹ - toFinsupp✝ } with
      | { toFinsupp := p } => ↑p)
      n =
    (match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝¹ } with
        | { toFinsupp := p } => ↑p)
        n -
      (match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝ } with
        | { toFinsupp := p } => ↑p)
        n
[PROOFSTEP]
apply Finsupp.sub_apply
[GOAL]
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℕ
a : R
⊢ ↑(monomial n) (-a) = -↑(monomial n) a
[PROOFSTEP]
rw [eq_neg_iff_add_eq_zero, ← monomial_add, neg_add_self, monomial_zero_right]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
p : R[X]
⊢ support (-p) = support p
[PROOFSTEP]
rcases p with
  ⟨⟩
    -- Porting note: The last rule should be `apply`ed.
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (-{ toFinsupp := toFinsupp✝ }) = support { toFinsupp := toFinsupp✝ }
[PROOFSTEP]
rw [← ofFinsupp_neg, support, support]
[GOAL]
case ofFinsupp
R : Type u
a b : R
m n : ℕ
inst✝ : Ring R
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ (match { toFinsupp := -toFinsupp✝ } with
    | { toFinsupp := p } => p.support) =
    match { toFinsupp := toFinsupp✝ } with
    | { toFinsupp := p } => p.support
[PROOFSTEP]
apply Finsupp.support_neg
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Ring R
n : ℤ
⊢ ↑C ↑n = ↑n
[PROOFSTEP]
simp
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ Nontrivial R[X]
[PROOFSTEP]
have h : Nontrivial (AddMonoidAlgebra R ℕ) := by infer_instance
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ Nontrivial (AddMonoidAlgebra R ℕ)
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
h : Nontrivial (AddMonoidAlgebra R ℕ)
⊢ Nontrivial R[X]
[PROOFSTEP]
rcases h.exists_pair_ne with ⟨x, y, hxy⟩
[GOAL]
case intro.intro
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
h : Nontrivial (AddMonoidAlgebra R ℕ)
x y : AddMonoidAlgebra R ℕ
hxy : x ≠ y
⊢ Nontrivial R[X]
[PROOFSTEP]
refine' ⟨⟨⟨x⟩, ⟨y⟩, _⟩⟩
[GOAL]
case intro.intro
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
h : Nontrivial (AddMonoidAlgebra R ℕ)
x y : AddMonoidAlgebra R ℕ
hxy : x ≠ y
⊢ { toFinsupp := x } ≠ { toFinsupp := y }
[PROOFSTEP]
simp [hxy]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ ¬coeff X 1 = coeff 0 1
[PROOFSTEP]
simp
[GOAL]
R : Type u
a✝ b : R
m n : ℕ
inst✝ : DivisionRing R
a : ℚ
f : R[X]
⊢ a • f = ↑C ↑a * f
[PROOFSTEP]
rw [← Rat.smul_one_eq_coe, ← Polynomial.smul_C, C_1, smul_one_mul]
