-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_add_eq_left_of_totalDegree_lt {p q : MvPolynomial σ R}
    (h : q.totalDegree < p.totalDegree) : (p + q).totalDegree = p.totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
⊢ b ∉ q.support

Tactic:
contrapose! h

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
h : b ∈ q.support
⊢ p.totalDegree ≤ q.totalDegree

Proof state:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
obtain ⟨b, hb₁, hb₂⟩ :=
  p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
    Multiset.card (toMultiset m)

Result:
case neg.intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
⊢ p.totalDegree ≤ (p + q).totalDegree

Proof state:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
⊢ b ∈ p.support \ q.support

Tactic:
rw [Finset.mem_sdiff]

Result:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
⊢ b ∈ p.support ∧ b ∉ q.support

Proof state:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
simp [hp]

Result:
no goals

Proof state:
case neg.intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
have hb : ¬b ∈ q.support := by
  contrapose! h
  rw [totalDegree_eq p, hb₂, totalDegree_eq]
  apply Finset.le_sup h

Result:
case neg.intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
⊢ p.totalDegree ≤ (p + q).totalDegree

Proof state:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree

case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
⊢ b ∈ (p + q).support

Tactic:
apply support_sdiff_support_subset_support_add

Result:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
⊢ b ∈ p.support \ q.support

Proof state:
case neg.intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ (toMultiset b).card ≤ (p + q).support.sup fun m => (toMultiset m).card

Tactic:
exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb

Result:
no goals

Proof state:
case neg.intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
have hbb : b ∈ (p + q).support := by
  apply support_sdiff_support_subset_support_add
  rw [Finset.mem_sdiff]
  exact ⟨hb₁, hb⟩

Result:
case neg.intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ p.totalDegree ≤ (p + q).totalDegree

Proof state:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ p.totalDegree

Tactic:
rw [← max_eq_left_of_lt h]

Result:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ p.totalDegree ⊔ q.totalDegree

Proof state:
case neg.intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
rw [totalDegree_eq, hb₂, totalDegree_eq]

Result:
case neg.intro.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ (toMultiset b).card ≤ (p + q).support.sup fun m => (toMultiset m).card

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree = p.totalDegree

Tactic:
apply le_antisymm

Result:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ p.totalDegree

case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ p.totalDegree ≤ (p + q).totalDegree

Proof state:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
⊢ (p + q).totalDegree ≤ p.totalDegree ⊔ q.totalDegree

Tactic:
exact totalDegree_add p q

Result:
no goals

Proof state:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m => (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
⊢ b ∈ p.support ∧ b ∉ q.support

Tactic:
exact ⟨hb₁, hb⟩

Result:
no goals