case refine_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (p q : R[T;T⁻¹]),
    (∃ n f', ↑toLaurent f' = p * T ↑n) → (∃ n f', ↑toLaurent f' = q * T ↑n) → ∃ n f', ↑toLaurent f' = (p + q) * T ↑n

case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T n * T ↑n_1
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ ∃ n f', ↑toLaurent f' = f * T ↑n
refine f.induction_on' ?_ fun n a => ?_ <;> clear f
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : ↑toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : ↑toLaurent gn = g * T ↑n
⊢ ∃ n f', ↑toLaurent f' = (f + g) * T ↑n
case refine_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (p q : R[T;T⁻¹]),
    (∃ n f', ↑toLaurent f' = p * T ↑n) → (∃ n f', ↑toLaurent f' = q * T ↑n) → ∃ n f', ↑toLaurent f' = (p + q) * T ↑n
rintro f g ⟨m, fn, hf⟩ ⟨n, gn, hg⟩
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : ↑toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : ↑toLaurent gn = g * T ↑n
⊢ ↑toLaurent (fn * X ^ n + gn * X ^ m) = (f + g) * T ↑(m + n)
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : ↑toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : ↑toLaurent gn = g * T ↑n
⊢ ∃ n f', ↑toLaurent f' = (f + g) * T ↑n
refine' ⟨m + n, fn * X ^ n + gn * X ^ m, _⟩
no goals
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : ↑toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : ↑toLaurent gn = g * T ↑n
⊢ ↑toLaurent (fn * X ^ n + gn * X ^ m) = (f + g) * T ↑(m + n)
simp only [hf, hg, add_mul, add_comm (n : ℤ), map_add, map_mul, Polynomial.toLaurent_X_pow,
  mul_T_assoc, Int.ofNat_add]
case refine_2.ofNat
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T (Int.ofNat n) * T ↑n_1

case refine_2.negSucc
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T (Int.negSucc n) * T ↑n_1
case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T n * T ↑n_1
cases' n with n n
no goals
case refine_2.ofNat
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T (Int.ofNat n) * T ↑n_1
exact ⟨0, Polynomial.C a * X ^ n, by simp⟩
no goals
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ↑toLaurent (↑Polynomial.C a * X ^ n) = ↑C a * T (Int.ofNat n) * T ↑0
simp
case refine_2.negSucc
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ↑toLaurent (↑Polynomial.C a) = ↑C a * T (Int.negSucc n) * T ↑(n + 1)
case refine_2.negSucc
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T (Int.negSucc n) * T ↑n_1
refine' ⟨n + 1, Polynomial.C a, _⟩
no goals
case refine_2.negSucc
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ↑toLaurent (↑Polynomial.C a) = ↑C a * T (Int.negSucc n) * T ↑(n + 1)
simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.ofNat_succ, mul_T_assoc, add_left_neg,
  T_zero, mul_one]