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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
⊢ (homogenization i p).totalDegree = p.totalDegree
Tactic:
by_cases hp : p = 0
State after:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : p = 0
⊢ (homogenization i p).totalDegree = p.totalDegree

case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ (homogenization i p).totalDegree = p.totalDegree

State before:
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ (homogenization i p).totalDegree = p.totalDegree
Tactic:
apply IsHomogeneous.totalDegree
State after:
case neg.hφ
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ (homogenization i p).IsHomogeneous p.totalDegree

case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ homogenization i p ≠ 0

State before:
case neg.hφ
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ (homogenization i p).IsHomogeneous p.totalDegree

case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ homogenization i p ≠ 0
Tactic:
refine' isHomogeneous_homogenization _ _
State after:
case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ homogenization i p ≠ 0

State before:
case neg.h
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : ¬p = 0
⊢ homogenization i p ≠ 0
Tactic:
exact homogenization_ne_zero_of_ne_zero _ hp h
State after:
no goals

State before:
case pos
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
hp : p = 0
⊢ (homogenization i p).totalDegree = p.totalDegree
Tactic:
simp [hp]
State after:
no goals