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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).leadingTerms = C r
Tactic:
rw [leadingTerms_eq_self_iff_isHomogeneous]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).IsHomogeneous (C r).totalDegree

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).IsHomogeneous (C r).totalDegree
Tactic:
convert isHomogeneous_C (R := R) _ _
State after:
case h.e'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).totalDegree = 0

State before:
case h.e'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
r : R
⊢ (C r).totalDegree = 0
Tactic:
simp
State after:
no goals