-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem exists_T_pow (f : R[T;T⁻¹]) : ∃ (n : ℕ) (f' : R[X]), toLaurent f' = f * T n

Proof state:
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

Tactic:
rcases n with n | n

Result:
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

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ ∃ n f', toLaurent f' = f * T ↑n

Tactic:
refine f.induction_on' ?_ fun n a => ?_ <;> clear f

Result:
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

Proof state:
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)

Tactic:
simp only [hf, hg, add_mul, add_comm (n : ℤ), map_add, map_mul, Polynomial.toLaurent_X_pow,
  mul_T_assoc, Int.ofNat_add]

Result:
no goals

Proof state:
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)

Tactic:
simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.ofNat_succ, mul_T_assoc,
  neg_add_cancel, T_zero, mul_one]

Result:
no goals

Proof state:
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

Tactic:
rintro f g ⟨m, fn, hf⟩ ⟨n, gn, hg⟩

Result:
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

Proof state:
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

Tactic:
refine ⟨n + 1, Polynomial.C a, ?_⟩

Result:
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)

Proof state:
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

Tactic:
refine ⟨m + n, fn * X ^ n + gn * X ^ m, ?_⟩

Result:
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)

Proof state:
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

Tactic:
exact ⟨0, Polynomial.C a * X ^ n, by simp⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ toLaurent (Polynomial.C a * X ^ n) = C a * T (Int.ofNat n) * T ↑0

Tactic:
simp

Result:
no goals