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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
⊢ (X s).leadingTerms = X s
Tactic:
nontriviality R
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).leadingTerms = X s

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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).IsHomogeneous (X s).totalDegree
Tactic:
convert isHomogeneous_X _ _
State after:
case h.e'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).totalDegree = 1

State before:
case h.e'_1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
s : ι
a✝ : Nontrivial R
⊢ (X s).totalDegree = 1
Tactic:
exact totalDegree_X _
State after:
no goals