awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
h₁ : ∀ (n : ℤ), Eq (α := R) ((f : (a : ℤ) → R) n : R) ((0 : (a : ℤ) → R) n : R)
⊢ f = 0

Tactic:
ext n
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
n : ℤ
h₁ : Eq (α := R) ((f : (a : ℤ) → R) n : R) (0 : R)
⊢ Eq (α := R) ((f : (a : ℤ) → R) n : R) ((0 : (a : ℤ) → R) n : R)

Tactic:
simp only [coe_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, Finsupp.coe_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
n : ℤ
⊢ ∀ (s : ℤ), Eq (α := R) ((f : (a : ℤ) → R) s : R) (0 : R)

Tactic:
simp_rw [degree, Finset.max_eq_sup_withBot, Finset.sup_eq_bot_iff, Finsupp.mem_support_iff, Ne,
    WithBot.coe_ne_bot, imp_false, not_not] at h

Premises used: Finsupp.mem_support_iff, Classical.not_not, imp_false, Ne, Finset.max_eq_sup_withBot, LaurentPolynomial.degree, Finset.sup_eq_bot_iff, WithBot.coe_ne_bot
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
n : ℤ
h : ∀ (s : ℤ), Eq (α := R) ((f : (a : ℤ) → R) s : R) (0 : R)
⊢ Eq (α := R) ((f : (a : ℤ) → R) n : R) (0 : R)

Tactic:
h n
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
n : ℤ
h : ∀ (s : ℤ), Eq (α := R) ((f : (a : ℤ) → R) s : R) (0 : R)
⊢ Eq (α := R) ((f : (a : ℤ) → R) n : R) (0 : R)

Tactic:
exact h n
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
rw : Finset.max {n} = (↑n : WithBot ℤ)
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree = (↑n : WithBot ℤ)

Tactic:
rw [degree, support_C_mul_T_of_ne_zero a0 n]

Premises used: LaurentPolynomial.support_C_mul_T_of_ne_zero, LaurentPolynomial.degree
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ Finset.max {n} = (↑n : WithBot ℤ)

Tactic:
Finset.max_singleton

Premises used: Finset.max_singleton
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ Finset.max {n} = (↑n : WithBot ℤ)

Tactic:
exact Finset.max_singleton

Premises used: Finset.max_singleton
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℤ
a : R
pos :
  ∀ (h : a = 0), (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree = ⊥
neg :
  ∀ (h : ¬a = 0),
    (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree = (↑n : WithBot ℤ)
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree =
    if a = 0 then ⊥ else (↑n : WithBot ℤ)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℤ
a : R
h : a = 0
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree = ⊥

Tactic:
simp only [h, map_zero, zero_mul, degree_zero, degree_C_mul_T, Ne,
      not_false_iff]

Premises used: MulZeroClass.zero_mul, LaurentPolynomial.degree_C_mul_T, map_zero, Ne, not_false_iff, LaurentPolynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
n : ℤ
a : R
h : ¬a = 0
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree = (↑n : WithBot ℤ)

Tactic:
simp only [h, map_zero, zero_mul, degree_zero, degree_C_mul_T, Ne,
      not_false_iff]

Premises used: MulZeroClass.zero_mul, LaurentPolynomial.degree_C_mul_T, map_zero, Ne, not_false_iff, LaurentPolynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℤ
rw : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) 1) (T n)).degree = (↑n : WithBot ℤ)
⊢ degree.{u_1} (R := R) (T n) = (↑n : WithBot ℤ)

Tactic:
rw [← one_mul (T n), ← map_one C]

Premises used: LaurentPolynomial.T, map_one, LaurentPolynomial.C, one_mul
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℤ
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) 1) (T n)).degree = (↑n : WithBot ℤ)

Tactic:
degree_C_mul_T n 1 (one_ne_zero : (1 : R) ≠ 0)

Premises used: LaurentPolynomial.degree_C_mul_T, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℤ
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) 1) (T n)).degree = (↑n : WithBot ℤ)

Tactic:
exact degree_C_mul_T n 1 (one_ne_zero : (1 : R) ≠ 0)

Premises used: LaurentPolynomial.degree_C_mul_T, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
a0 : a ≠ 0
rw : (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0)).degree = 0
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = 0

Tactic:
rw [← mul_one (C a), ← T_zero]

Premises used: LaurentPolynomial.T_zero, mul_one, DFunLike.coe, LaurentPolynomial.C
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
a0 : a ≠ 0
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0)).degree = 0

Tactic:
degree_C_mul_T 0 a a0

Premises used: LaurentPolynomial.degree_C_mul_T, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
a0 : a ≠ 0
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0)).degree = 0

Tactic:
exact degree_C_mul_T 0 a a0

Premises used: LaurentPolynomial.degree_C_mul_T, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
a : R
pos : ∀ (h : a = 0), degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = ⊥
neg : ∀ (h : ¬a = 0), degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = 0
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = if a = 0 then ⊥ else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
a : R
h : a = 0
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = ⊥

Tactic:
simp only [h, map_zero, degree_zero, degree_C, Ne, not_false_iff]

Premises used: LaurentPolynomial.degree_C, map_zero, Ne, not_false_iff, LaurentPolynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
a : R
h : ¬a = 0
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = 0

Tactic:
simp only [h, map_zero, degree_zero, degree_C, Ne, not_false_iff]

Premises used: LaurentPolynomial.degree_C, map_zero, Ne, not_false_iff, LaurentPolynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
pos :
  ∀ (a0 : a = 0),
    (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree ≤ (↑n : WithBot ℤ)
neg :
  ∀ (a0 : ¬a = 0),
    (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree ≤ (↑n : WithBot ℤ)
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree ≤ (↑n : WithBot ℤ)

Tactic:
by_cases a0 : a = 0
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
a0 : a = 0
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree ≤ (↑n : WithBot ℤ)

Tactic:
simp only [a0, map_zero, zero_mul, degree_zero, bot_le]

Premises used: MulZeroClass.zero_mul, map_zero, bot_le, LaurentPolynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
a0 : ¬a = 0
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree ≤ (↑n : WithBot ℤ)

Tactic:
(degree_C_mul_T n a a0).le

Premises used: LaurentPolynomial.degree_C_mul_T, Eq.le
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
a0 : ¬a = 0
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree ≤ (↑n : WithBot ℤ)

Tactic:
exact (degree_C_mul_T n a a0).le

Premises used: LaurentPolynomial.degree_C_mul_T, Eq.le
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
rw : degree.{u_1} (R := R) (T n) = (HMul.hMul (α := R[T;T⁻¹]) 1 (T n)).degree
rw₁ rw₂ : degree.{u_1} (R := R) (T n) = degree.{u_1} (R := R) (T n)
⊢ degree.{u_1} (R := R) (T n) = (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) 1) (T n)).degree

Tactic:
rw [map_one, one_mul]

Premises used: map_one, one_mul
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
rw :
  degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) =
    (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (1 : R[T;T⁻¹])).degree
rw₁ rw₂ : degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a)
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) =
    (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0)).degree

Tactic:
rw [T_zero, mul_one]

Premises used: LaurentPolynomial.T_zero, mul_one
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R_1 : Type u_1
S : Type u_2
inst : Semiring R_1
R : Type u_3
inst_1 : Semiring R
x y : R[X]
z : R[T;T⁻¹]
rw : (x * y) • z = x • y • z
rw₁ rw₂ : x • y • z = x • y • z
⊢ (x • y) • z = x • y • z

Tactic:
rw [smul_eq_mul, mul_smul]

Premises used: smul_eq_mul, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommSemiring R_1
S : Type u_3
inst_1 : CommSemiring S
f_1 : R_1 →+* S
x : Sˣ
R : Type u_4
inst_2 : CommSemiring R
f : R[X]
l : R[T;T⁻¹]
⊢ HMul.hMul (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) l =
    HMul.hMul (β := R[T;T⁻¹]) l ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹])

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
⊢ Eq (α := R[T;T⁻¹]) ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) (HPow.hPow (α := R[X]) X n) : R[T;T⁻¹])
    (T (↑n : ℤ) : R[T;T⁻¹])

Tactic:
Polynomial.toLaurent_X_pow n

Premises used: Polynomial.toLaurent_X_pow
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
⊢ Eq (α := R[T;T⁻¹]) ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹])
    ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
x_1 : ↥(Submonoid.powers X)
t : R[X]
ht : Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) t
obtain :
  ∀ (n : ℕ),
    IsUnit (M := R[T;T⁻¹])
      ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹])
          (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
                ((fun (x : ℕ) ↦ HPow.hPow (α := R[X]) X x) n) ⋯) :
            R[X]) :
        R[T;T⁻¹])
⊢ IsUnit (M := R[T;T⁻¹])
    ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹])
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x) t ht) :
          R[X]) :
      R[T;T⁻¹])

Tactic:
obtain ⟨n, rfl⟩ := ht

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
x_1 : ↥(Submonoid.powers X)
n : ℕ
rw : IsUnit.{u_1} (M := R[T;T⁻¹]) (T (↑n : ℤ))
⊢ IsUnit (M := R[T;T⁻¹])
    ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹])
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := R[X]) X x) n) ⋯) :
          R[X]) :
      R[T;T⁻¹])

Tactic:
rw [algebraMap_eq_toLaurent, toLaurent_X_pow]

Premises used: LaurentPolynomial.algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
x_1 : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit.{u_1} (M := R[T;T⁻¹]) (T (↑n : ℤ))

Tactic:
isUnit_T ↑n

Premises used: Nat.cast, LaurentPolynomial.isUnit_T
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
x_1 : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit.{u_1} (M := R[T;T⁻¹]) (T (↑n : ℤ))

Tactic:
exact isUnit_T ↑n

Premises used: Nat.cast, LaurentPolynomial.isUnit_T
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f_1 : R →+* S
x : Sˣ
f : R[T;T⁻¹]
mul_T :
  ∀ (f : R[X]) (n : ℕ),
    ∃ (x : R[X] × ↥(Submonoid.powers X)),
      HMul.hMul (β := R[T;T⁻¹])
          (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
          ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) (↑x.2 : R[X]) : R[T;T⁻¹]) =
        (algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) x.1
⊢ ∃ (x : R[X] × ↥(Submonoid.powers X)),
    HMul.hMul (β := R[T;T⁻¹]) f ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) (↑x.2 : R[X]) : R[T;T⁻¹]) =
      (algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) x.1

Tactic:
induction f using LaurentPolynomial.induction_on_mul_T with | _ f n
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f_1 : R →+* S
x : Sˣ
f : R[X]
n : ℕ
⊢ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) (HPow.hPow (α := R[X]) X n)

Tactic:
have : X ^ n ∈ Submonoid.powers (X : R[X]) := ⟨n, rfl⟩
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f_1 : R →+* S
x : Sˣ
f : R[X]
n : ℕ
this : Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) (HPow.hPow (α := R[X]) X n)
⊢ ∃ (x : R[X] × ↥(Submonoid.powers X)),
    HMul.hMul (β := R[T;T⁻¹])
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
        ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) (↑x.2 : R[X]) : R[T;T⁻¹]) =
      (algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) x.1

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

Premises used: Prod.mk, Subtype.mk, Exists.intro
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f_1 : R →+* S
x : Sˣ
f : R[X]
n : ℕ
this : Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) (HPow.hPow (α := R[X]) X n)
mul_T :
  HMul.hMul (β := R[T;T⁻¹])
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
      ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹])
          (↑(f,
                  Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
                    (HPow.hPow (α := R[X]) X n) this).2 :
            R[X]) :
        R[T;T⁻¹]) =
    (algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹])
      (f,
          Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
            (HPow.hPow (α := R[X]) X n) this).1
⊢ ∃ (x : R[X] × ↥(Submonoid.powers X)),
    HMul.hMul (β := R[T;T⁻¹])
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
        ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) (↑x.2 : R[X]) : R[T;T⁻¹]) =
      (algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) x.1

Tactic:
refine ⟨(f, ⟨_, this⟩), ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f_1 : R →+* S
x : Sˣ
f : R[X]
n : ℕ
this : Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) (HPow.hPow (α := R[X]) X n)
⊢ HMul.hMul (β := R[T;T⁻¹])
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
      ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹])
          (↑(f,
                  Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
                    (HPow.hPow (α := R[X]) X n) this).2 :
            R[X]) :
        R[T;T⁻¹]) =
    (algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹])
      (f,
          Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
            (HPow.hPow (α := R[X]) X n) this).1

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

Premises used: LaurentPolynomial.mul_T_assoc, LaurentPolynomial.T_zero, LaurentPolynomial.algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow, neg_add_cancel, mul_one
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f_1 : R →+* S
x : Sˣ
f g : R[X]
rw : f = g → ∃ (c : ↥(Submonoid.powers X)), (↑c : R[X]) * f = (↑c : R[X]) * g
⊢ Eq (α := R[T;T⁻¹]) ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹])
      ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) g : R[T;T⁻¹]) →
    ∃ (c : ↥(Submonoid.powers X)), (↑c : R[X]) * f = (↑c : R[X]) * g

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

Premises used: LaurentPolynomial.algebraMap_eq_toLaurent, Polynomial.toLaurent_inj
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f_1 : R →+* S
x : Sˣ
f : R[X]
⊢ ∃ (c : ↥(Submonoid.powers X)), (↑c : R[X]) * f = (↑c : R[X]) * f

Tactic:
⟨1, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S_1 : Type u_2
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f_1 : R →+* S
x : Sˣ
f : R[X]
⊢ ∃ (c : ↥(Submonoid.powers X)), (↑c : R[X]) * f = (↑c : R[X]) * f

Tactic:
exact ⟨1, rfl⟩
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
rw :
  HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
      (IsLocalization.mk' (M := Submonoid.powers X) R[T;T⁻¹] p
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
            (HPow.hPow (α := R[X]) X n) ⋯) :
        R[T;T⁻¹])
      ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (HPow.hPow (α := R[X]) X n) : R[T;T⁻¹]) =
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) p
rw₁ :
  HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
      (IsLocalization.mk' (M := Submonoid.powers X) R[T;T⁻¹] p
          (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
            (HPow.hPow (α := R[X]) X n) ⋯) :
        R[T;T⁻¹])
      ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) (HPow.hPow (α := R[X]) X n) : R[T;T⁻¹]) =
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) p
rw₂ :
  Eq (α := R[T;T⁻¹]) ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹])
    ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹])
rw₃ rw₄ :
  Eq (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹])
    ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹])
⊢ HMul.hMul (α := R[T;T⁻¹])
      (IsLocalization.mk' (M := Submonoid.powers X) R[T;T⁻¹] p
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
          (HPow.hPow (α := R[X]) X n) ⋯))
      (T (↑n : ℤ)) =
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) p

Tactic:
rw [← toLaurent_X_pow, ← algebraMap_eq_toLaurent, IsLocalization.mk'_spec,
    algebraMap_eq_toLaurent]

Premises used: LaurentPolynomial.algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow, IsLocalization.mk'_spec
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
rw :
  HMul.hMul (α := R[T;T⁻¹])
      (IsLocalization.mk' (M := Submonoid.powers X) R[T;T⁻¹] p
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
          (HPow.hPow (α := R[X]) X n) ⋯))
      (T (↑n : ℤ)) =
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) p
⊢ IsLocalization.mk' (M := Submonoid.powers X) R[T;T⁻¹] p
      (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
        (HPow.hPow (α := R[X]) X n) ⋯) =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹]) (T (-(↑n : ℤ)))

Tactic:
rw [← IsUnit.mul_left_inj (isUnit_T n), mul_T_assoc, neg_add_cancel, T_zero, mul_one]

Premises used: LaurentPolynomial.mul_T_assoc, LaurentPolynomial.T_zero, Nat.cast, LaurentPolynomial.isUnit_T, neg_add_cancel, IsUnit.mul_left_inj, mul_one
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ HMul.hMul (α := R[T;T⁻¹])
      (IsLocalization.mk' (M := Submonoid.powers X) R[T;T⁻¹] p
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
          (HPow.hPow (α := R[X]) X n) ⋯))
      (T (↑n : ℤ)) =
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) p

Tactic:
mk'_mul_T p n

Premises used: LaurentPolynomial.mk'_mul_T
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ HMul.hMul (α := R[T;T⁻¹])
      (IsLocalization.mk' (M := Submonoid.powers X) R[T;T⁻¹] p
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
          (HPow.hPow (α := R[X]) X n) ⋯))
      (T (↑n : ℤ)) =
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) p

Tactic:
exact mk'_mul_T p n

Premises used: LaurentPolynomial.mk'_mul_T
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
n : ℕ
rw : HMul.hMul (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) 1) (T (-(↑n : ℤ))) = T (-(↑n : ℤ))
rw₁ : HMul.hMul (α := R[T;T⁻¹]) 1 (T (-(↑n : ℤ))) = T (-(↑n : ℤ))
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (-(↑n : ℤ))) (T (-(↑n : ℤ)))
⊢ Eq (α := R[T;T⁻¹])
    (IsLocalization.mk' (M := Submonoid.powers X) R[T;T⁻¹] 1
      (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
        (HPow.hPow (α := R[X]) X n) ⋯))
    (T (-(↑n : ℤ)))

Tactic:
rw [mk'_eq 1 n, toLaurent_one, one_mul]

Premises used: LaurentPolynomial.mk'_eq, Polynomial.toLaurent_one, OfNat.ofNat, one_mul
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := R[T;T⁻¹])
    (IsLocalization.mk' (M := Submonoid.powers X) R[T;T⁻¹] 1
      (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
        (HPow.hPow (α := R[X]) (β := ℕ) X 1) ⋯))
    (T (-(↑1 : ℤ)))

Tactic:
mk'_one_X_pow 1

Premises used: LaurentPolynomial.mk'_one_X_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
h : X = HPow.hPow (α := R[X]) (β := ℕ) X 1
⊢ Eq.{u_1 + 1} (α := R[T;T⁻¹])
    (IsLocalization.mk' (R := R[X]) (M := Submonoid.powers X) R[T;T⁻¹] 1
      (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x) X ⋯))
    (T (-1))

Tactic:
convert! mk'_one_X_pow 1

Premises used: LaurentPolynomial.mk'_one_X_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
⊢ X = HPow.hPow (α := R[X]) (β := ℕ) X 1

Tactic:
(pow_one X).symm

Premises used: pow_one, Eq.symm, Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
⊢ X = HPow.hPow (α := R[X]) (β := ℕ) X 1

Tactic:
exact (pow_one X).symm

Premises used: pow_one, Eq.symm, Polynomial.X