[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p✝ q p : MvPolynomial σ R
⊢ degrees (-p) = degrees p
[PROOFSTEP]
rw [degrees, support_neg]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p✝ q p : MvPolynomial σ R
⊢ (Finset.sup (support p) fun s => ↑toMultiset s) = degrees p
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ degrees (p - q) ≤ degrees p ⊔ degrees q
[PROOFSTEP]
simpa only [sub_eq_add_neg] using le_trans (degrees_add p (-q)) (by rw [degrees_neg])
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
⊢ degrees p ⊔ degrees (-q) ≤ degrees p ⊔ degrees q
[PROOFSTEP]
rw [degrees_neg]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q : MvPolynomial σ R
⊢ vars (-p) = vars p
[PROOFSTEP]
simp [vars, degrees_neg]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars (p - q) ⊆ vars p ∪ vars q
[PROOFSTEP]
convert vars_add_subset p (-q) using 2
[GOAL]
case h.e'_3.h.e'_4
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ p - q = p + -q
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
case h.e'_4.h.e'_4
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars q = vars (-q)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint (vars p) (vars q)
⊢ vars (p - q) = vars p ∪ vars q
[PROOFSTEP]
rw [← vars_neg q] at hpq
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint (vars p) (vars (-q))
⊢ vars (p - q) = vars p ∪ vars q
[PROOFSTEP]
convert vars_add_of_disjoint hpq using 2
[GOAL]
case h.e'_2.h.e'_4
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint (vars p) (vars (-q))
⊢ p - q = p + -q
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
case h.e'_3.h.e'_4
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
hpq : Disjoint (vars p) (vars (-q))
⊢ vars q = vars (-q)
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
R✝ : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
⊢ eval₂ c (↑f ∘ X) x = ↑f x
[PROOFSTEP]
apply
  MvPolynomial.induction_on x
    (fun n => by
      rw [hom_C f, eval₂_C]
      exact eq_intCast c n)
    (fun p q hp hq => by
      rw [eval₂_add, hp, hq]
      exact (f.map_add _ _).symm)
    (fun p n hp => by
      rw [eval₂_mul, eval₂_X, hp]
      exact (f.map_mul _ _).symm)
[GOAL]
R✝ : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ eval₂ c (↑f ∘ X) (↑C n) = ↑f (↑C n)
[PROOFSTEP]
rw [hom_C f, eval₂_C]
[GOAL]
R✝ : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x : MvPolynomial R ℤ
n : ℤ
⊢ ↑c n = ↑n
[PROOFSTEP]
exact eq_intCast c n
[GOAL]
R✝ : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p✝ q✝ : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (↑f ∘ X) p = ↑f p
hq : eval₂ c (↑f ∘ X) q = ↑f q
⊢ eval₂ c (↑f ∘ X) (p + q) = ↑f (p + q)
[PROOFSTEP]
rw [eval₂_add, hp, hq]
[GOAL]
R✝ : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p✝ q✝ : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p q : MvPolynomial R ℤ
hp : eval₂ c (↑f ∘ X) p = ↑f p
hq : eval₂ c (↑f ∘ X) q = ↑f q
⊢ ↑f p + ↑f q = ↑f (p + q)
[PROOFSTEP]
exact (f.map_add _ _).symm
[GOAL]
R✝ : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p✝ q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (↑f ∘ X) p = ↑f p
⊢ eval₂ c (↑f ∘ X) (p * X n) = ↑f (p * X n)
[PROOFSTEP]
rw [eval₂_mul, eval₂_X, hp]
[GOAL]
R✝ : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R✝
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R✝
p✝ q : MvPolynomial σ R✝
inst✝ : CommRing S
f✝ : R✝ →+* S
g : σ → S
R : Type u
c : ℤ →+* S
f : MvPolynomial R ℤ →+* S
x p : MvPolynomial R ℤ
n : R
hp : eval₂ c (↑f ∘ X) p = ↑f p
⊢ ↑f p * (↑f ∘ X) n = ↑f (p * X n)
[PROOFSTEP]
exact (f.map_mul _ _).symm
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : CommRing S
f✝ : R →+* S
g f : σ → S
x : σ
⊢ (fun f => ↑f ∘ X) ((fun f => eval₂Hom (Int.castRingHom S) f) f) x = f x
[PROOFSTEP]
simp only [coe_eval₂Hom, Function.comp_apply, eval₂_X]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q : MvPolynomial σ R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ (m : σ →₀ ℕ), m ∈ support f → k ≤ ↑m x → coeff m f = coeff m g
hg : ∀ (m : σ →₀ ℕ), m ∈ support g → k ≤ ↑m x → coeff m f = coeff m g
⊢ degreeOf x (f - g) < k
[PROOFSTEP]
classical
rw [degreeOf_lt_iff h]
intro m hm
by_contra' hc
have h := support_sub σ f g hm
simp only [mem_support_iff, Ne.def, coeff_sub, sub_eq_zero] at hm
cases' Finset.mem_union.1 h with cf cg
· exact hm (hf m cf hc)
· exact hm (hg m cg hc)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q : MvPolynomial σ R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ (m : σ →₀ ℕ), m ∈ support f → k ≤ ↑m x → coeff m f = coeff m g
hg : ∀ (m : σ →₀ ℕ), m ∈ support g → k ≤ ↑m x → coeff m f = coeff m g
⊢ degreeOf x (f - g) < k
[PROOFSTEP]
rw [degreeOf_lt_iff h]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q : MvPolynomial σ R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ (m : σ →₀ ℕ), m ∈ support f → k ≤ ↑m x → coeff m f = coeff m g
hg : ∀ (m : σ →₀ ℕ), m ∈ support g → k ≤ ↑m x → coeff m f = coeff m g
⊢ ∀ (m : σ →₀ ℕ), m ∈ support (f - g) → ↑m x < k
[PROOFSTEP]
intro m hm
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q : MvPolynomial σ R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ (m : σ →₀ ℕ), m ∈ support f → k ≤ ↑m x → coeff m f = coeff m g
hg : ∀ (m : σ →₀ ℕ), m ∈ support g → k ≤ ↑m x → coeff m f = coeff m g
m : σ →₀ ℕ
hm : m ∈ support (f - g)
⊢ ↑m x < k
[PROOFSTEP]
by_contra' hc
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q : MvPolynomial σ R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ (m : σ →₀ ℕ), m ∈ support f → k ≤ ↑m x → coeff m f = coeff m g
hg : ∀ (m : σ →₀ ℕ), m ∈ support g → k ≤ ↑m x → coeff m f = coeff m g
m : σ →₀ ℕ
hm : m ∈ support (f - g)
hc : k ≤ ↑m x
⊢ False
[PROOFSTEP]
have h := support_sub σ f g hm
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q : MvPolynomial σ R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ (m : σ →₀ ℕ), m ∈ support f → k ≤ ↑m x → coeff m f = coeff m g
hg : ∀ (m : σ →₀ ℕ), m ∈ support g → k ≤ ↑m x → coeff m f = coeff m g
m : σ →₀ ℕ
hm : m ∈ support (f - g)
hc : k ≤ ↑m x
h : m ∈ support f ∪ support g
⊢ False
[PROOFSTEP]
simp only [mem_support_iff, Ne.def, coeff_sub, sub_eq_zero] at hm
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q : MvPolynomial σ R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ (m : σ →₀ ℕ), m ∈ support f → k ≤ ↑m x → coeff m f = coeff m g
hg : ∀ (m : σ →₀ ℕ), m ∈ support g → k ≤ ↑m x → coeff m f = coeff m g
m : σ →₀ ℕ
hc : k ≤ ↑m x
h : m ∈ support f ∪ support g
hm : ¬coeff m f = coeff m g
⊢ False
[PROOFSTEP]
cases' Finset.mem_union.1 h with cf cg
[GOAL]
case inl
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q : MvPolynomial σ R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ (m : σ →₀ ℕ), m ∈ support f → k ≤ ↑m x → coeff m f = coeff m g
hg : ∀ (m : σ →₀ ℕ), m ∈ support g → k ≤ ↑m x → coeff m f = coeff m g
m : σ →₀ ℕ
hc : k ≤ ↑m x
h : m ∈ support f ∪ support g
hm : ¬coeff m f = coeff m g
cf : m ∈ support f
⊢ False
[PROOFSTEP]
exact hm (hf m cf hc)
[GOAL]
case inr
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q : MvPolynomial σ R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ (m : σ →₀ ℕ), m ∈ support f → k ≤ ↑m x → coeff m f = coeff m g
hg : ∀ (m : σ →₀ ℕ), m ∈ support g → k ≤ ↑m x → coeff m f = coeff m g
m : σ →₀ ℕ
hc : k ≤ ↑m x
h : m ∈ support f ∪ support g
hm : ¬coeff m f = coeff m g
cg : m ∈ support g
⊢ False
[PROOFSTEP]
exact hm (hg m cg hc)
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q a : MvPolynomial σ R
⊢ totalDegree (-a) = totalDegree a
[PROOFSTEP]
simp only [totalDegree, support_neg]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q a b : MvPolynomial σ R
⊢ totalDegree (a - b) = totalDegree (a + -b)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
R : Type u
S : Type v
σ : Type u_1
a✝ a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommRing R
p q a b : MvPolynomial σ R
⊢ max (totalDegree a) (totalDegree (-b)) = max (totalDegree a) (totalDegree b)
[PROOFSTEP]
rw [totalDegree_neg]


[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : MvPolynomial σ R
⊢ ↑(expand 1) f = f
[PROOFSTEP]
simp only [expand, pow_one, eval₂Hom_eq_bind₂, bind₂_C_left, RingHom.toMonoidHom_eq_coe, RingHom.coe_monoidHom_id,
  AlgHom.coe_mk, RingHom.coe_mk, MonoidHom.id_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ expand 1 = AlgHom.id R (MvPolynomial σ R)
[PROOFSTEP]
ext1 f
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ
⊢ ↑(expand 1) (X f) = ↑(AlgHom.id R (MvPolynomial σ R)) (X f)
[PROOFSTEP]
rw [expand_one_apply, AlgHom.id_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
⊢ AlgHom.comp (expand p) (bind₁ f) = bind₁ fun i => ↑(expand p) (f i)
[PROOFSTEP]
apply algHom_ext
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
⊢ ∀ (i : σ), ↑(AlgHom.comp (expand p) (bind₁ f)) (X i) = ↑(bind₁ fun i => ↑(expand p) (f i)) (X i)
[PROOFSTEP]
intro i
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
i : σ
⊢ ↑(AlgHom.comp (expand p) (bind₁ f)) (X i) = ↑(bind₁ fun i => ↑(expand p) (f i)) (X i)
[PROOFSTEP]
simp only [AlgHom.comp_apply, bind₁_X_right]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : σ → MvPolynomial τ R
φ : MvPolynomial σ R
⊢ ↑(expand p) (↑(bind₁ f) φ) = ↑(bind₁ fun i => ↑(expand p) (f i)) φ
[PROOFSTEP]
rw [← AlgHom.comp_apply, expand_comp_bind₁]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
p : ℕ
φ : MvPolynomial σ R
⊢ ↑(map f) (↑(expand p) φ) = ↑(expand p) (↑(map f) φ)
[PROOFSTEP]
simp [expand, map_bind₁]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : ℕ
φ : MvPolynomial σ R
⊢ ↑(rename f) (↑(expand p) φ) = ↑(expand p) (↑(rename f) φ)
[PROOFSTEP]
simp [expand, bind₁_rename, rename_bind₁, Function.comp]
[GOAL]
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : ℕ
⊢ AlgHom.comp (rename f) (expand p) = AlgHom.comp (expand p) (rename f)
[PROOFSTEP]
ext1 φ
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : ℕ
φ : σ
⊢ ↑(AlgHom.comp (rename f) (expand p)) (X φ) = ↑(AlgHom.comp (expand p) (rename f)) (X φ)
[PROOFSTEP]
simp only [rename_expand, AlgHom.comp_apply]