-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma supDegree_add_eq_left (h : q.supDegree D < p.supDegree D) :
    (p + q).supDegree D = p.supDegree D

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
⊢ supDegree D (p + q) = supDegree D p

Tactic:
apply (supDegree_add_le.trans <| sup_le le_rfl h.le).antisymm

Result:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
⊢ supDegree D p ≤ supDegree D (p + q)

Proof state:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
⊢ supDegree D p ≤ supDegree D (p + q)

Tactic:
obtain ⟨a, ha, he⟩ := exists_supDegree_mem_support D (ne_zero_of_not_supDegree_le h.not_le)

Result:
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
ha : a ∈ p.support
he : supDegree D p = D a
⊢ supDegree D p ≤ supDegree D (p + q)

Proof state:
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
h : supDegree D q < supDegree D p
a : A
ha : a ∈ p.support
he : supDegree D p = D a
⊢ supDegree D p ≤ supDegree D (p + q)

Tactic:
rw [he] at h ⊢

Result:
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
⊢ D a ≤ supDegree D (p + q)

Proof state:
case intro.intro.hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
⊢ p a ≠ 0

Tactic:
exact mem_support_iff.mp ha

Result:
no goals

Proof state:
case intro.intro.hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
⊢ a ∈ (p + q).support

Tactic:
rw [mem_support_iff, add_apply, apply_eq_zero_of_not_le_supDegree h.not_le, add_zero]

Result:
case intro.intro.hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
⊢ p a ≠ 0

Proof state:
case intro.intro
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
⊢ D a ≤ supDegree D (p + q)

Tactic:
apply Finset.le_sup

Result:
case intro.intro.hb
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.support
he : supDegree D p = D a
⊢ a ∈ (p + q).support