Theorem: MvPolynomial.leadingTerms_mul (FltRegular/ReadyForMathlib/Homogenization.lean)

State before:
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
by_cases hp : p.totalDegree = 0
State after:
case pos
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms

case neg
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms

State before:
case neg
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
by_cases hq : q.totalDegree = 0
State after:
case pos
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : q.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms

case neg
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms

State before:
case neg
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
rcases eq_leadingTerms_add p hp with ⟨wp, hp, tp⟩
State after:
case neg.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms

State before:
case neg.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
rcases eq_leadingTerms_add q hq with ⟨wq, hq, tq⟩
State after:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms

State before:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
rw [hp, hq]
State after:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ ((p.leadingTerms + wp) * (q.leadingTerms + wq)).leadingTerms =
    (p.leadingTerms + wp).leadingTerms * (q.leadingTerms + wq).leadingTerms

State before:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ ((p.leadingTerms + wp) * (q.leadingTerms + wq)).leadingTerms =
    (p.leadingTerms + wp).leadingTerms * (q.leadingTerms + wq).leadingTerms
Tactic:
simp only [add_mul, mul_add]
State after:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms + wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).leadingTerms =
    (p.leadingTerms + wp).leadingTerms * (q.leadingTerms + wq).leadingTerms

State before:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms + wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).leadingTerms =
    (p.leadingTerms + wp).leadingTerms * (q.leadingTerms + wq).leadingTerms
Tactic:
rw [add_assoc, leadingTerms_add_of_totalDegree_lt, leadingTerms_add_of_totalDegree_lt,
  leadingTerms_add_of_totalDegree_lt, leadingTerms_idempotent, leadingTerms_idempotent,
  leadingTerms_eq_self_iff_isHomogeneous]
State after:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.leadingTerms * q.leadingTerms).totalDegree

case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ wq.totalDegree < q.leadingTerms.totalDegree

case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ wp.totalDegree < p.leadingTerms.totalDegree

case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).totalDegree < (p.leadingTerms * q.leadingTerms).totalDegree

State before:
case pos
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
rw [eq_C_of_totalDegree_zero hp, leadingTerms_C_mul, leadingTerms_C]
State after:
no goals

State before:
case pos
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : q.totalDegree = 0
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
Tactic:
rw [eq_C_of_totalDegree_zero hq, mul_comm, leadingTerms_C_mul, leadingTerms_C, mul_comm]
State after:
no goals

State before:
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
Tactic:
rw [IsHomogeneous.totalDegree]
State after:
case hφ
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.totalDegree + q.totalDegree)

case h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0

State before:
case hφ
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.totalDegree + q.totalDegree)

case h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Tactic:
apply IsHomogeneous.mul (isHomogeneous_leadingTerms p) (isHomogeneous_leadingTerms q)
State after:
case h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0

State before:
case h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Tactic:
apply mul_ne_zero
State after:
case h.ha
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms ≠ 0

case h.hb
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ q.leadingTerms ≠ 0

State before:
case h.ha
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p.leadingTerms ≠ 0
Tactic:
apply leadingTerms_ne_zero
State after:
case h.ha.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p ≠ 0

State before:
case h.ha.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ p ≠ 0
Tactic:
rintro rfl
State after:
case h.ha.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
q : MvPolynomial ι S
hq : ¬q.totalDegree = 0
hp : ¬totalDegree 0 = 0
⊢ False

State before:
case h.ha.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
q : MvPolynomial ι S
hq : ¬q.totalDegree = 0
hp : ¬totalDegree 0 = 0
⊢ False
Tactic:
exact hp totalDegree_zero
State after:
no goals

State before:
case h.hb
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ q.leadingTerms ≠ 0
Tactic:
apply leadingTerms_ne_zero
State after:
case h.hb.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ q ≠ 0

State before:
case h.hb.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬q.totalDegree = 0
⊢ q ≠ 0
Tactic:
rintro rfl
State after:
case h.hb.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬totalDegree 0 = 0
⊢ False

State before:
case h.hb.hp
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p : MvPolynomial ι S
hp : ¬p.totalDegree = 0
hq : ¬totalDegree 0 = 0
⊢ False
Tactic:
exact hq totalDegree_zero
State after:
no goals

State before:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.leadingTerms * q.leadingTerms).totalDegree
Tactic:
rw [this]
State after:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.totalDegree + q.totalDegree)

State before:
case neg.intro.intro.intro.intro
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.totalDegree + q.totalDegree)
Tactic:
exact IsHomogeneous.mul (isHomogeneous_leadingTerms p) (isHomogeneous_leadingTerms q)
State after:
no goals

State before:
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ wq.totalDegree < q.leadingTerms.totalDegree
Tactic:
rwa [totalDegree_leadingTerms]
State after:
no goals

State before:
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ wp.totalDegree < p.leadingTerms.totalDegree
Tactic:
rwa [totalDegree_leadingTerms]
State after:
no goals

State before:
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).totalDegree < (p.leadingTerms * q.leadingTerms).totalDegree
Tactic:
rw [this]
State after:
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).totalDegree < p.totalDegree + q.totalDegree

State before:
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).totalDegree < p.totalDegree + q.totalDegree
Tactic:
calc
  _ ≤ max (wp * (leadingTerms q)).totalDegree ((leadingTerms p) * wq + wp * wq).totalDegree :=
    totalDegree_add _ _
  _ ≤
      max (wp * (leadingTerms q)).totalDegree
        (max ((leadingTerms p) * wq).totalDegree (wp * wq).totalDegree) :=
    (max_le_max (le_refl _) (totalDegree_add _ _))
  _ ≤
      max (wp.totalDegree + (leadingTerms q).totalDegree)
        (max ((leadingTerms p) * wq).totalDegree (wp * wq).totalDegree) :=
    (max_le_max (totalDegree_mul _ _) (le_refl _))
  _ ≤
      max (wp.totalDegree + (leadingTerms q).totalDegree)
        (max ((leadingTerms p).totalDegree + wq.totalDegree)
          (wp.totalDegree + wq.totalDegree)) :=
    (max_le_max (le_refl _) (max_le_max (totalDegree_mul _ _) (totalDegree_mul _ _)))
  _ < p.totalDegree + q.totalDegree := ?_
State after:
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ max (wp.totalDegree + q.leadingTerms.totalDegree)
      (max (p.leadingTerms.totalDegree + wq.totalDegree) (wp.totalDegree + wq.totalDegree)) <
    p.totalDegree + q.totalDegree

State before:
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ max (wp.totalDegree + q.leadingTerms.totalDegree)
      (max (p.leadingTerms.totalDegree + wq.totalDegree) (wp.totalDegree + wq.totalDegree)) <
    p.totalDegree + q.totalDegree
Tactic:
simp only [totalDegree_leadingTerms, max_lt_iff, add_lt_add_iff_right, add_lt_add_iff_left]
State after:
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ wp.totalDegree < p.totalDegree ∧
    wq.totalDegree < q.totalDegree ∧ wp.totalDegree + wq.totalDegree < p.totalDegree + q.totalDegree

State before:
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ wp.totalDegree < p.totalDegree ∧
    wq.totalDegree < q.totalDegree ∧ wp.totalDegree + wq.totalDegree < p.totalDegree + q.totalDegree
Tactic:
exact ⟨tp, tq, add_lt_add tp tq⟩
State after:
no goals