-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
lemma supDegree_sub_lt_of_leadingCoeff_eq (hD : D.Injective) {R} [CommRing R] {p q : R[A]}
    (hd : p.supDegree D = q.supDegree D) (hc : p.leadingCoeff D = q.leadingCoeff D) :
    (p - q).supDegree D < p.supDegree D ∨ p = q

Proof state:
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
⊢ ¬p = q → supDegree D (p - q) < supDegree D p

Tactic:
refine fun he => (supDegree_sub_le.trans ?_).lt_of_ne ?_

Result:
case refine_1
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ supDegree D p ⊔ supDegree D q ≤ supDegree D p

case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ supDegree D (p - q) ≠ supDegree D p

Proof state:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q) (Function.invFun D (supDegree D (p - q))) = 0
⊢ supDegree D (p - q) ≠ supDegree D p

Tactic:
refine fun h => he ?_

Result:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q) (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ (p - q) (Function.invFun D (supDegree D (p - q))) = 0

Proof state:
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
⊢ supDegree D (p - q) < supDegree D p ∨ p = q

Tactic:
rw [or_iff_not_imp_right]

Result:
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
⊢ ¬p = q → supDegree D (p - q) < supDegree D p

Proof state:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ supDegree D (p - q) ≠ supDegree D p

Tactic:
rw [← sub_eq_zero, ← leadingCoeff_eq_zero hD, leadingCoeff] at he

Result:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q) (Function.invFun D (supDegree D (p - q))) = 0
⊢ supDegree D (p - q) ≠ supDegree D p

Proof state:
case refine_2
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬(p - q) (Function.invFun D (supDegree D (p - q))) = 0
h : supDegree D (p - q) = supDegree D p
⊢ (p - q) (Function.invFun D (supDegree D (p - q))) = 0

Tactic:
rwa [h, Finsupp.sub_apply, ← leadingCoeff, hd, ← leadingCoeff, sub_eq_zero]

Result:
no goals

Proof state:
case refine_1
A : Type u_3
B : Type u_5
inst✝³ : LinearOrder B
inst✝² : OrderBot B
D : A → B
inst✝¹ : AddZeroClass A
hD : Function.Injective D
R : Type u_8
inst✝ : CommRing R
p q : R[A]
hd : supDegree D p = supDegree D q
hc : leadingCoeff D p = leadingCoeff D q
he : ¬p = q
⊢ supDegree D p ⊔ supDegree D q ≤ supDegree D p

Tactic:
rw [hd, sup_idem]

Result:
no goals