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

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

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

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

case h
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Tactic:
apply IsHomogeneous.mul <;> simp [isHomogeneous_leadingTerms]
State after:
case h
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0

State before:
case h
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
Tactic:
apply mul_ne_zero (leadingTerms_ne_zero hp) (leadingTerms_ne_zero hq)
State after:
no goals