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

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

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

State before:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ homogenization i ((monomial s) r) = (monomial s) r
Tactic:
erw [homogenization, Finsupp.mapDomain_single, single_eq_monomial, totalDegree_monomial _ hr,
  tsub_self]
State after:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ (monomial (s + Finsupp.single i 0)) r = (monomial s) r

State before:
case neg
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
hr : ¬r = 0
⊢ (monomial (s + Finsupp.single i 0)) r = (monomial s) r
Tactic:
simp
State after:
no goals

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