case h.e'_3
R : Type u_1
inst✝ : Semiring R
r : R
⊢ ↑C r = ↑C r * T ↑0
R : Type u_1
inst✝ : Semiring R
r : R
⊢ ↑toLaurent (↑Polynomial.C r) = ↑C r
convert Polynomial.toLaurent_C_mul_T 0 r
no goals
case h.e'_3
R : Type u_1
inst✝ : Semiring R
r : R
⊢ ↑C r = ↑C r * T ↑0
simp only [Int.ofNat_zero, T_zero, mul_one]