by_cases hr : r = 0
R : Type u_2
ι : Type u_1
inst✝ : CommSemiring R
i : ι
s : ι →₀ ℕ
r : R
⊢ homogenization i ((monomial s) r) = (monomial s) r
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