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

State before:
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
⊢ ((monomial s) r).leadingTerms = (monomial s) r
Tactic:
by_cases hr : r = 0
State after:
case pos
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : r = 0
⊢ ((monomial s) r).leadingTerms = (monomial s) r

case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ ((monomial s) r).leadingTerms = (monomial s) r

State before:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ ((monomial s) r).leadingTerms = (monomial s) r
Tactic:
rw [leadingTerms_eq_self_iff_isHomogeneous]
State after:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ ((monomial s) r).IsHomogeneous ((monomial s) r).totalDegree

State before:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ ((monomial s) r).IsHomogeneous ((monomial s) r).totalDegree
Tactic:
convert isHomogeneous_monomial (R := R) _ _
State after:
case neg.convert_5
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ degree s = ((monomial s) r).totalDegree

State before:
case neg.convert_5
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ degree s = ((monomial s) r).totalDegree
Tactic:
simp [totalDegree_monomial _ hr]
State after:
case neg.convert_5
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ degree s = s.sum fun x e => e

State before:
case neg.convert_5
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ degree s = s.sum fun x e => e
Tactic:
rfl
State after:
no goals

State before:
case pos
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
s : ι →₀ ℕ
r : R
hr : r = 0
⊢ ((monomial s) r).leadingTerms = (monomial s) r
Tactic:
simp [hr]
State after:
no goals