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
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
rw [degreeOf_lt_iff h]
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
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
intro m hm
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
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
by_contra' hc
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
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
have h := support_sub σ f g hm
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
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
simp only [mem_support_iff, Ne.def, coeff_sub, sub_eq_zero] at hm
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

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
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
cases' Finset.mem_union.1 h with cf cg
no goals
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
exact hm (hf m cf hc)
no goals
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
exact hm (hg m cg hc)