-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem degreeOf_sub_lt {x : σ} {f g : MvPolynomial σ R} {k : ℕ} (h : 0 < k)
    (hf : ∀ m : σ →₀ ℕ, m ∈ f.support → k ≤ m x → coeff m f = coeff m g)
    (hg : ∀ m : σ →₀ ℕ, m ∈ g.support → k ≤ m x → coeff m f = coeff m g) :
    degreeOf x (f - g) < k

Proof state:
case inr
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hc : k ≤ m x
h : m ∈ f.support ∪ g.support
hm : ¬coeff m f = coeff m g
cg : m ∈ g.support
⊢ False

Tactic:
exact hm (hg m cg hc)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hc : k ≤ m x
h : m ∈ f.support ∪ g.support
hm : ¬coeff m f = coeff m g
⊢ False

Tactic:
rcases Finset.mem_union.1 h with cf | cg

Result:
case inl
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hc : k ≤ m x
h : m ∈ f.support ∪ g.support
hm : ¬coeff m f = coeff m g
cf : m ∈ f.support
⊢ False

case inr
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hc : k ≤ m x
h : m ∈ f.support ∪ g.support
hm : ¬coeff m f = coeff m g
cg : m ∈ g.support
⊢ False

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hm : m ∈ (f - g).support
hc : k ≤ m x
h : m ∈ f.support ∪ g.support
⊢ False

Tactic:
simp only [mem_support_iff, Ne, coeff_sub, sub_eq_zero] at hm

Result:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hc : k ≤ m x
h : m ∈ f.support ∪ g.support
hm : ¬coeff m f = coeff m g
⊢ False

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hm : m ∈ (f - g).support
⊢ m x < k

Tactic:
by_contra! hc

Result:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hm : m ∈ (f - g).support
hc : k ≤ m x
⊢ False

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
⊢ degreeOf x (f - g) < k

Tactic:
rw [degreeOf_lt_iff h]

Result:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
⊢ ∀ m ∈ (f - g).support, m x < k

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hm : m ∈ (f - g).support
hc : k ≤ m x
⊢ False

Tactic:
have h := support_sub σ f g hm

Result:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hm : m ∈ (f - g).support
hc : k ≤ m x
h : m ∈ f.support ∪ g.support
⊢ False

Proof state:
case inl
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h✝ : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hc : k ≤ m x
h : m ∈ f.support ∪ g.support
hm : ¬coeff m f = coeff m g
cf : m ∈ f.support
⊢ False

Tactic:
exact hm (hf m cf hc)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
⊢ ∀ m ∈ (f - g).support, m x < k

Tactic:
intro m hm

Result:
R : Type u
σ : Type u_1
inst✝ : CommRing R
x : σ
f g : MvPolynomial σ R
k : ℕ
h : 0 < k
hf : ∀ m ∈ f.support, k ≤ m x → coeff m f = coeff m g
hg : ∀ m ∈ g.support, k ≤ m x → coeff m f = coeff m g
m : σ →₀ ℕ
hm : m ∈ (f - g).support
⊢ m x < k