awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : Nontrivial R
n : ℤ
⊢ degree.{u_1} (R := R) (T n) = (↑n : WithBot ℤ)
have rw : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) 1) (T n)).degree = (↑n : WithBot ℤ)
Tactic: rw [← one_mul (T n), ← map_one C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
a0 : a ≠ 0
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = 0
have rw : (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0)).degree = 0
Tactic: rw [← mul_one (C a), ← T_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
a : R
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = if a = 0 then ⊥ else 0
have pos : ∀ (h : a = 0), degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = ⊥
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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) = ⊥
⊢ degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = if a = 0 then ⊥ else 0
have neg : ∀ (h : ¬a = 0), degree.{u_1} (R := R) ((C : (a : R) → R[T;T⁻¹]) a) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree ≤ (↑n : WithBot ℤ)
have 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 ℤ)
Tactic: by_cases a0 : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 ℤ)
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree ≤ (↑n : WithBot ℤ)
have 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 ℤ)
Tactic: by_cases a0 : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
⊢ degree.{u_1} (R := R) (T n) = (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) 1) (T n)).degree
have rw : degree.{u_1} (R := R) (T n) = (HMul.hMul (α := R[T;T⁻¹]) 1 (T n)).degree
Tactic: rw [map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ degree.{u_1} (R := R) (T n) = (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) 1) (T n)).degree
have rw₁ : degree.{u_1} (R := R) (T n) = degree.{u_1} (R := R) (T n)
Tactic: rw [map_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ 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
have 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
Tactic: rw [T_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ 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
have 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)
Tactic: rw [T_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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⁻¹]
⊢ (x • y) • z = x • y • z
have rw : (x * y) • z = x • y • z
Tactic: rw [smul_eq_mul, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ (x • y) • z = x • y • z
have rw₁ : x • y • z = x • y • z
Tactic: rw [smul_eq_mul, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ 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⁻¹])
have 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) sorry) :
          R[X]) :
      R[T;T⁻¹])
Tactic: obtain ⟨n, rfl⟩ := ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 (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⁻¹])
have rw : IsUnit.{u_1} (M := R[T;T⁻¹]) (T (↑n : ℤ))
Tactic: rw [algebraMap_eq_toLaurent, toLaurent_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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⁻¹]
⊢ ∃ (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
have 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
Tactic: induction f using LaurentPolynomial.induction_on_mul_T with | _ f n
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (hypothesis)
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 : ℕ
⊢ ∃ (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
have this : 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⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
have 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
Tactic: refine ⟨(f, ⟨_, this⟩), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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]
⊢ 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
have rw : f = g → ∃ (c : ↥(Submonoid.powers X)), (↑c : R[X]) * f = (↑c : R[X]) * g
Tactic: rw [algebraMap_eq_toLaurent, algebraMap_eq_toLaurent, Polynomial.toLaurent_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
have 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) sorry) :
      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
Tactic: rw [← toLaurent_X_pow, ← algebraMap_eq_toLaurent, IsLocalization.mk'_spec,
    algebraMap_eq_toLaurent]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ 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
have 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) sorry) :
      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
Tactic: rw [← toLaurent_X_pow, ← algebraMap_eq_toLaurent, IsLocalization.mk'_spec,
    algebraMap_eq_toLaurent]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ 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
have 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⁻¹])
Tactic: rw [← toLaurent_X_pow, ← algebraMap_eq_toLaurent, IsLocalization.mk'_spec,
    algebraMap_eq_toLaurent]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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⁻¹])
⊢ 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
have 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⁻¹])
Tactic: rw [← toLaurent_X_pow, ← algebraMap_eq_toLaurent, IsLocalization.mk'_spec,
    algebraMap_eq_toLaurent]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
p : R[X]
n : ℕ
⊢ 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 : ℤ)))
have 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) sorry))
    (T (↑n : ℤ)) =
  (toLaurent : (a : R[X]) → R[T;T⁻¹]) p
Tactic: rw [← IsUnit.mul_left_inj (isUnit_T n), mul_T_assoc, neg_add_cancel, T_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
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 : ℤ)))
have rw : HMul.hMul (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) 1) (T (-(↑n : ℤ))) = T (-(↑n : ℤ))
Tactic: rw [mk'_eq 1 n, toLaurent_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : ℤ))
⊢ 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 : ℤ)))
have rw₁ : HMul.hMul (α := R[T;T⁻¹]) 1 (T (-(↑n : ℤ))) = T (-(↑n : ℤ))
Tactic: rw [mk'_eq 1 n, toLaurent_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : ℤ))
⊢ 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 : ℤ)))
have rw₂ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (-(↑n : ℤ))) (T (-(↑n : ℤ)))
Tactic: rw [mk'_eq 1 n, toLaurent_one, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ 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))
have h : X = HPow.hPow (α := R[X]) (β := ℕ) X 1
Tactic: convert! mk'_one_X_pow 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
p : R[X]
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹]) = Polynomial.eval₂ f (↑x : S) p
have unfold : (IsLocalization.lift sorry : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹]) =
  Polynomial.eval₂ f (↑x : S) p
Tactic: unfold eval₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
p : R[X]
⊢ (IsLocalization.lift ⋯ : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹]) =
    Polynomial.eval₂ f (↑x : S) p
have rw : (IsLocalization.lift sorry : (a : R[T;T⁻¹]) → S) ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹]) =
  Polynomial.eval₂ f (↑x : S) p
Tactic: rw [← algebraMap_eq_toLaurent, IsLocalization.lift_eq, coe_eval₂RingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
p : R[X]
rw :
  (IsLocalization.lift ⋯ : (a : R[T;T⁻¹]) → S) ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹]) =
    Polynomial.eval₂ f (↑x : S) p
⊢ (IsLocalization.lift ⋯ : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹]) =
    Polynomial.eval₂ f (↑x : S) p
have rw₁ : (eval₂RingHom f (↑x : S) : (a : R[X]) → S) p = Polynomial.eval₂ f (↑x : S) p
Tactic: rw [← algebraMap_eq_toLaurent, IsLocalization.lift_eq, coe_eval₂RingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
p : R[X]
rw :
  (IsLocalization.lift ⋯ : (a : R[T;T⁻¹]) → S) ((algebraMap R[X] R[T;T⁻¹] : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹]) =
    Polynomial.eval₂ f (↑x : S) p
rw₁ : (eval₂RingHom f (↑x : S) : (a : R[X]) → S) p = Polynomial.eval₂ f (↑x : S) p
⊢ (IsLocalization.lift ⋯ : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹]) =
    Polynomial.eval₂ f (↑x : S) p
have rw₂ : Polynomial.eval₂ f (↑x : S) p = Polynomial.eval₂ f (↑x : S) p
Tactic: rw [← algebraMap_eq_toLaurent, IsLocalization.lift_eq, coe_eval₂RingHom]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (↑n : ℤ)) = (↑x : S) ^ n
have rw : (eval₂ f x : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (HPow.hPow (α := R[X]) X n) : R[T;T⁻¹]) =
  (↑x : S) ^ n
Tactic: rw [← Polynomial.toLaurent_X_pow, eval₂_toLaurent, eval₂_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
rw :
  (eval₂ f x : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (HPow.hPow (α := R[X]) X n) : R[T;T⁻¹]) =
    (↑x : S) ^ n
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (↑n : ℤ)) = (↑x : S) ^ n
have rw₁ : Polynomial.eval₂ f (↑x : S) (HPow.hPow (α := R[X]) X n) = (↑x : S) ^ n
Tactic: rw [← Polynomial.toLaurent_X_pow, eval₂_toLaurent, eval₂_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
rw :
  (eval₂ f x : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (HPow.hPow (α := R[X]) X n) : R[T;T⁻¹]) =
    (↑x : S) ^ n
rw₁ : Polynomial.eval₂ f (↑x : S) (HPow.hPow (α := R[X]) X n) = (↑x : S) ^ n
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (↑n : ℤ)) = (↑x : S) ^ n
have rw₂ : (↑x : S) ^ n = (↑x : S) ^ n
Tactic: rw [← Polynomial.toLaurent_X_pow, eval₂_toLaurent, eval₂_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑n : ℤ))) = (↑x⁻¹ : S) ^ n
have rw : (eval₂ f x : (a : R[T;T⁻¹]) → S)
    (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) sorry)) =
  (↑x⁻¹ : S) ^ n
Tactic: rw [← mk'_one_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S)
      (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) ⋯)) =
    (↑x⁻¹ : S) ^ n
have unfold : (IsLocalization.lift sorry : (a : R[T;T⁻¹]) → S)
    (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) sorry)) =
  (↑x⁻¹ : S) ^ n
Tactic: unfold eval₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
⊢ (IsLocalization.lift ⋯ : (a : R[T;T⁻¹]) → S)
      (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) ⋯)) =
    (↑x⁻¹ : S) ^ n
have rw : (eval₂RingHom f (↑x : S) : (a : R[X]) → S) 1 =
  HMul.hMul (α := S)
    ((eval₂RingHom f (↑x : S) : (a : R[X]) → S)
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
              (HPow.hPow (α := R[X]) X n) sorry) :
          R[X]) :
      S)
    ((↑x⁻¹ : S) ^ n)
Tactic: rw [IsLocalization.lift_mk'_spec, map_one, coe_eval₂RingHom, eval₂_X_pow, ← mul_pow,
    Units.mul_inv, one_pow]