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

State before:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
Tactic:
by_cases hr : r = 0
State after:
case pos
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : r = 0
⊢ (C r * p).leadingTerms = C r * p.leadingTerms

case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (C r * p).leadingTerms = C r * p.leadingTerms

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
Tactic:
have : support (C r * p) = p.support := by
  rw [C_mul']
  exact Finsupp.support_smul_eq hr
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
this : (C r * p).support = p.support
⊢ (C r * p).leadingTerms = C r * p.leadingTerms

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
this : (C r * p).support = p.support
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
Tactic:
rw [leadingTerms, leadingTerms, totalDegree, this, homogeneousComponent_C_mul]
State after:
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
this : (C r * p).support = p.support
⊢ C r * (homogeneousComponent (p.support.sup fun s => s.sum fun x e => e)) p =
    C r * (homogeneousComponent p.totalDegree) p

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
this : (C r * p).support = p.support
⊢ C r * (homogeneousComponent (p.support.sup fun s => s.sum fun x e => e)) p =
    C r * (homogeneousComponent p.totalDegree) p
Tactic:
rfl
State after:
no goals

State before:
case pos
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : r = 0
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
Tactic:
simp [hr]
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (C r * p).support = p.support
Tactic:
rw [C_mul']
State after:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (r • p).support = p.support

State before:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (r • p).support = p.support
Tactic:
exact Finsupp.support_smul_eq hr
State after:
no goals