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

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ homogenization i (C c) = C c
Tactic:
simp only [homogenization, totalDegree_C, zero_tsub]
State after:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i 0) (C c) = C c

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i 0) (C c) = C c
Tactic:
convert Finsupp.mapDomain_single (M := R) using 1
State after:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = Finsupp.single (0 + Finsupp.single i 0) c

State before:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = Finsupp.single (0 + Finsupp.single i 0) c
Tactic:
rw [single_eq_monomial]
State after:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = (monomial (0 + Finsupp.single i 0)) c

State before:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = (monomial (0 + Finsupp.single i 0)) c
Tactic:
have : (0 : ι →₀ ℕ) i = 0 := by simp only [Finsupp.coe_zero, Pi.zero_apply]
State after:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
this : 0 i = 0
⊢ C c = (monomial (0 + Finsupp.single i 0)) c

State before:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
this : 0 i = 0
⊢ C c = (monomial (0 + Finsupp.single i 0)) c
Tactic:
rw [← this]
State after:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
this : 0 i = 0
⊢ C c = (monomial (0 + Finsupp.single i (0 i))) c

State before:
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
this : 0 i = 0
⊢ C c = (monomial (0 + Finsupp.single i (0 i))) c
Tactic:
simp
State after:
no goals

State before:
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ 0 i = 0
Tactic:
simp only [Finsupp.coe_zero, Pi.zero_apply]
State after:
no goals