-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_add_le {f g : MvPolynomial σ R} :
    m.toSyn (m.degree (f + g)) ≤ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Proof state:
case pos.h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f)

Tactic:
exact m.le_degree hf

Result:
no goals

Proof state:
case neg.h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree g)

Tactic:
apply m.le_degree

Result:
case neg.h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ b ∈ g.support

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)

Tactic:
by_cases hf : b ∈ f.support

Result:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f + g)) ≤ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Tactic:
conv_rhs => rw [← m.toSyn.apply_symm_apply (_ ⊔ _)]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f + g)) ≤ m.toSyn (m.toSyn.symm (m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)))

Proof state:
case neg.h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ b ∈ g.support

Tactic:
simp only [not_mem_support_iff] at hf

Result:
case neg.h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : coeff b f = 0
⊢ b ∈ g.support

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f + g)) ≤ m.toSyn (m.toSyn.symm (m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)))

Tactic:
rw [degree_le_iff]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f + g).support, m.toSyn c ≤ m.toSyn (m.toSyn.symm (m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)))

Proof state:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)

Tactic:
left

Result:
case pos.h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f)

Proof state:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)

Tactic:
right

Result:
case neg.h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree g)

Proof state:
case neg.h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : coeff b f = 0
⊢ b ∈ g.support

Tactic:
simpa only [mem_support_iff, coeff_add, hf, zero_add] using hb

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f + g).support, m.toSyn c ≤ m.toSyn (m.toSyn.symm (m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)))

Tactic:
simp only [AddEquiv.apply_symm_apply, le_sup_iff]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f + g).support, m.toSyn c ≤ m.toSyn (m.degree f) ∨ m.toSyn c ≤ m.toSyn (m.degree g)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
⊢ ∀ c ∈ (f + g).support, m.toSyn c ≤ m.toSyn (m.degree f) ∨ m.toSyn c ≤ m.toSyn (m.degree g)

Tactic:
intro b hb

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)