-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem isLocalization : IsLocalization (Submonoid.powers (X : R[X])) R[T;T⁻¹] :=
  { map_units' := fun ⟨t, ht⟩ => by
      obtain ⟨n, rfl⟩ := ht
      rw [algebraMap_eq_toLaurent, toLaurent_X_pow]
      exact isUnit_T ↑n
    surj' := fun f => by
      induction' f using LaurentPolynomial.induction_on_mul_T with f n
      have : X ^ n ∈ Submonoid.powers (X : R[X]) := ⟨n, rfl⟩
      refine ⟨(f, ⟨_, this⟩), ?_⟩
      simp only [algebraMap_eq_toLaurent, toLaurent_X_pow, mul_T_assoc, neg_add_cancel, T_zero,
        mul_one]
    exists_of_eq := fun {f g} => by
      rw [algebraMap_eq_toLaurent, algebraMap_eq_toLaurent, Polynomial.toLaurent_inj]
      rintro rfl
      exact ⟨1, rfl⟩ }

Proof state:
R : Type u_1
inst✝ : CommSemiring R
x✝ : ↥(Submonoid.powers X)
t : R[X]
ht : t ∈ Submonoid.powers X
⊢ IsUnit ((algebraMap R[X] R[T;T⁻¹]) ↑⟨t, ht⟩)

Tactic:
obtain ⟨n, rfl⟩ := ht

Result:
case intro
R : Type u_1
inst✝ : CommSemiring R
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit ((algebraMap R[X] R[T;T⁻¹]) ↑⟨(fun x => X ^ x) n, ⋯⟩)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ (algebraMap R[X] R[T;T⁻¹]) f = (algebraMap R[X] R[T;T⁻¹]) g → ∃ c, ↑c * f = ↑c * g

Tactic:
rw [algebraMap_eq_toLaurent, algebraMap_eq_toLaurent, Polynomial.toLaurent_inj]

Result:
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ f = g → ∃ c, ↑c * f = ↑c * g

Proof state:
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
⊢ ∃ x, toLaurent f * T (-↑n) * (algebraMap R[X] R[T;T⁻¹]) ↑x.2 = (algebraMap R[X] R[T;T⁻¹]) x.1

Tactic:
have : X ^ n ∈ Submonoid.powers (X : R[X]) := ⟨n, rfl⟩

Result:
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
this : X ^ n ∈ Submonoid.powers X
⊢ ∃ x, toLaurent f * T (-↑n) * (algebraMap R[X] R[T;T⁻¹]) ↑x.2 = (algebraMap R[X] R[T;T⁻¹]) x.1

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : R[T;T⁻¹]
⊢ ∃ x, f * (algebraMap R[X] R[T;T⁻¹]) ↑x.2 = (algebraMap R[X] R[T;T⁻¹]) x.1

Tactic:
induction' f using LaurentPolynomial.induction_on_mul_T with f n

Result:
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
⊢ ∃ x, toLaurent f * T (-↑n) * (algebraMap R[X] R[T;T⁻¹]) ↑x.2 = (algebraMap R[X] R[T;T⁻¹]) x.1

Proof state:
case intro
R : Type u_1
inst✝ : CommSemiring R
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit ((algebraMap R[X] R[T;T⁻¹]) ↑⟨(fun x => X ^ x) n, ⋯⟩)

Tactic:
rw [algebraMap_eq_toLaurent, toLaurent_X_pow]

Result:
case intro
R : Type u_1
inst✝ : CommSemiring R
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit (T ↑n)

Proof state:
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
this : X ^ n ∈ Submonoid.powers X
⊢ toLaurent f * T (-↑n) * (algebraMap R[X] R[T;T⁻¹]) ↑(f, ⟨X ^ n, this⟩).2 =
    (algebraMap R[X] R[T;T⁻¹]) (f, ⟨X ^ n, this⟩).1

Tactic:
simp only [algebraMap_eq_toLaurent, toLaurent_X_pow, mul_T_assoc, neg_add_cancel, T_zero,
  mul_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ f = g → ∃ c, ↑c * f = ↑c * g

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ ∃ c, ↑c * f = ↑c * f

Proof state:
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
this : X ^ n ∈ Submonoid.powers X
⊢ ∃ x, toLaurent f * T (-↑n) * (algebraMap R[X] R[T;T⁻¹]) ↑x.2 = (algebraMap R[X] R[T;T⁻¹]) x.1

Tactic:
refine ⟨(f, ⟨_, this⟩), ?_⟩

Result:
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
this : X ^ n ∈ Submonoid.powers X
⊢ toLaurent f * T (-↑n) * (algebraMap R[X] R[T;T⁻¹]) ↑(f, ⟨X ^ n, this⟩).2 =
    (algebraMap R[X] R[T;T⁻¹]) (f, ⟨X ^ n, this⟩).1

Proof state:
case intro
R : Type u_1
inst✝ : CommSemiring R
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit (T ↑n)

Tactic:
exact isUnit_T ↑n

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ ∃ c, ↑c * f = ↑c * f

Tactic:
exact ⟨1, rfl⟩

Result:
no goals