awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂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) ⋯) :
            R[X]) :
        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₁ : 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]
-- 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₂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) ⋯) :
            R[X]) :
        S)
      ((↑x⁻¹ : S) ^ n)
rw₁ :
  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) ⋯) :
            R[X]) :
        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₂ : 1 =
  Polynomial.eval₂ f (↑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]) *
    (↑x⁻¹ : S) ^ n
Tactic: rw [IsLocalization.lift_mk'_spec, map_one, coe_eval₂RingHom, eval₂_X_pow, ← mul_pow,
    Units.mul_inv, one_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₂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) ⋯) :
            R[X]) :
        S)
      ((↑x⁻¹ : S) ^ n)
rw₁ :
  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) ⋯) :
            R[X]) :
        S)
      ((↑x⁻¹ : S) ^ n)
rw₂ :
  1 =
    Polynomial.eval₂ f (↑x : S)
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
              (HPow.hPow (α := R[X]) X n) ⋯) :
          R[X]) *
      (↑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₃ : 1 = (↑x : S) ^ n * (↑x⁻¹ : S) ^ n
Tactic: rw [IsLocalization.lift_mk'_spec, map_one, coe_eval₂RingHom, eval₂_X_pow, ← mul_pow,
    Units.mul_inv, one_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₂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) ⋯) :
            R[X]) :
        S)
      ((↑x⁻¹ : S) ^ n)
rw₁ :
  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) ⋯) :
            R[X]) :
        S)
      ((↑x⁻¹ : S) ^ n)
rw₂ :
  1 =
    Polynomial.eval₂ f (↑x : S)
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
              (HPow.hPow (α := R[X]) X n) ⋯) :
          R[X]) *
      (↑x⁻¹ : S) ^ n
rw₃ : 1 = (↑x : S) ^ n * (↑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₄ : 1 = ((↑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]
-- 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₂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) ⋯) :
            R[X]) :
        S)
      ((↑x⁻¹ : S) ^ n)
rw₁ :
  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) ⋯) :
            R[X]) :
        S)
      ((↑x⁻¹ : S) ^ n)
rw₂ :
  1 =
    Polynomial.eval₂ f (↑x : S)
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
              (HPow.hPow (α := R[X]) X n) ⋯) :
          R[X]) *
      (↑x⁻¹ : S) ^ n
rw₃ : 1 = (↑x : S) ^ n * (↑x⁻¹ : S) ^ n
rw₄ : 1 = ((↑x : 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₅ : 1 = HPow.hPow (α := S) 1 n
Tactic: rw [IsLocalization.lift_mk'_spec, map_one, coe_eval₂RingHom, eval₂_X_pow, ← mul_pow,
    Units.mul_inv, one_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₂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) ⋯) :
            R[X]) :
        S)
      ((↑x⁻¹ : S) ^ n)
rw₁ :
  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) ⋯) :
            R[X]) :
        S)
      ((↑x⁻¹ : S) ^ n)
rw₂ :
  1 =
    Polynomial.eval₂ f (↑x : S)
        (↑(Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (Submonoid.powers X) x)
              (HPow.hPow (α := R[X]) X n) ⋯) :
          R[X]) *
      (↑x⁻¹ : S) ^ n
rw₃ : 1 = (↑x : S) ^ n * (↑x⁻¹ : S) ^ n
rw₄ : 1 = ((↑x : S) * (↑x⁻¹ : S)) ^ n
rw₅ : 1 = HPow.hPow (α := S) 1 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₆ : Eq.{u_3 + 1} (α := S) 1 1
Tactic: rw [IsLocalization.lift_mk'_spec, map_one, coe_eval₂RingHom, eval₂_X_pow, ← mul_pow,
    Units.mul_inv, one_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 ^ n) : S)
have pos : ∀ (hn : 0 ≤ n), (eval₂ f x : (a : R[T;T⁻¹]) → S) (T n) = (↑(x ^ n) : S)
Tactic: by_cases! hn : 0 ≤ n
-- 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 : ℤ
pos : ∀ (hn : 0 ≤ n), (eval₂ f x : (a : R[T;T⁻¹]) → S) (T n) = (↑(x ^ n) : S)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T n) = (↑(x ^ n) : S)
have neg : ∀ (hn : n < 0), (eval₂ f x : (a : R[T;T⁻¹]) → S) (T n) = (↑(x ^ n) : S)
Tactic: by_cases! hn : 0 ≤ n
-- 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 : ℤ
hn : 0 ≤ n
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T n) = (↑(x ^ n) : S)
have pos : ∀ (n : ℕ), (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (↑n : ℤ)) = (↑(HPow.hPow (β := ℤ) x (↑n : ℤ)) : S)
Tactic: lift n to ℕ using hn
Cleared hypotheses: n, hn
-- 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 : ℤ
hn : n < 0
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T n) = (↑(x ^ n) : S)
have neg : ∀ (m : ℕ) (hn : LT.lt (α := ℤ) (-(↑m : ℤ)) 0),
  (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑m : ℤ))) = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
Tactic: obtain ⟨m, rfl⟩ := Int.exists_eq_neg_ofNat hn.le
Cleared hypotheses: n, hn
-- 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ˣ
m : ℕ
hn : LT.lt (α := ℤ) (-(↑m : ℤ)) 0
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑m : ℤ))) = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
have neg : (↑x⁻¹ : S) ^ m = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
Tactic: rw [eval₂_T_neg_n, zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val]
-- 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ˣ
m : ℕ
hn : LT.lt (α := ℤ) (-(↑m : ℤ)) 0
neg : (↑x⁻¹ : S) ^ m = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑m : ℤ))) = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
have neg₁ : (↑x⁻¹ : S) ^ m = (↑(HPow.hPow (β := ℤ) x (↑m : ℤ))⁻¹ : S)
Tactic: rw [eval₂_T_neg_n, zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val]
-- 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ˣ
m : ℕ
hn : LT.lt (α := ℤ) (-(↑m : ℤ)) 0
neg : (↑x⁻¹ : S) ^ m = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
neg₁ : (↑x⁻¹ : S) ^ m = (↑(HPow.hPow (β := ℤ) x (↑m : ℤ))⁻¹ : S)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑m : ℤ))) = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
have neg₂ : (↑x⁻¹ : S) ^ m = (↑(x ^ m)⁻¹ : S)
Tactic: rw [eval₂_T_neg_n, zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val]
-- 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ˣ
m : ℕ
hn : LT.lt (α := ℤ) (-(↑m : ℤ)) 0
neg : (↑x⁻¹ : S) ^ m = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
neg₁ : (↑x⁻¹ : S) ^ m = (↑(HPow.hPow (β := ℤ) x (↑m : ℤ))⁻¹ : S)
neg₂ : (↑x⁻¹ : S) ^ m = (↑(x ^ m)⁻¹ : S)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑m : ℤ))) = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
have neg₃ : (↑x⁻¹ : S) ^ m = (↑(x⁻¹ ^ m) : S)
Tactic: rw [eval₂_T_neg_n, zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val]
-- 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ˣ
m : ℕ
hn : LT.lt (α := ℤ) (-(↑m : ℤ)) 0
neg : (↑x⁻¹ : S) ^ m = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
neg₁ : (↑x⁻¹ : S) ^ m = (↑(HPow.hPow (β := ℤ) x (↑m : ℤ))⁻¹ : S)
neg₂ : (↑x⁻¹ : S) ^ m = (↑(x ^ m)⁻¹ : S)
neg₃ : (↑x⁻¹ : S) ^ m = (↑(x⁻¹ ^ m) : S)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑m : ℤ))) = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
have neg₄ : (↑x⁻¹ : S) ^ m = (↑x⁻¹ : S) ^ m
Tactic: rw [eval₂_T_neg_n, zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val]
-- 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ˣ
r : R
⊢ Eq.{u_3 + 1} (α := S) ((eval₂ f x : (a : R[T;T⁻¹]) → S) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) : S)
    ((f : (a : R) → S) r : S)
have rw : Eq.{u_3 + 1} (α := S)
  ((eval₂ f x : (a : R[T;T⁻¹]) → S)
      ((toLaurent : (a : R[X]) → R[T;T⁻¹]) ((Polynomial.C : (a : R) → R[X]) r) : R[T;T⁻¹]) :
    S)
  ((f : (a : R) → S) r : S)
Tactic: rw [← toLaurent_C, eval₂_toLaurent, Polynomial.eval₂_C]
-- 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ˣ
r : R
rw :
  Eq.{u_3 + 1} (α := S)
    ((eval₂ f x : (a : R[T;T⁻¹]) → S)
        ((toLaurent : (a : R[X]) → R[T;T⁻¹]) ((Polynomial.C : (a : R) → R[X]) r) : R[T;T⁻¹]) :
      S)
    ((f : (a : R) → S) r : S)
⊢ Eq.{u_3 + 1} (α := S) ((eval₂ f x : (a : R[T;T⁻¹]) → S) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) : S)
    ((f : (a : R) → S) r : S)
have rw₁ : Polynomial.eval₂ f (↑x : S) ((Polynomial.C : (a : R) → R[X]) r) = (f : (a : R) → S) r
Tactic: rw [← toLaurent_C, eval₂_toLaurent, Polynomial.eval₂_C]
-- 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ˣ
r : R
rw :
  Eq.{u_3 + 1} (α := S)
    ((eval₂ f x : (a : R[T;T⁻¹]) → S)
        ((toLaurent : (a : R[X]) → R[T;T⁻¹]) ((Polynomial.C : (a : R) → R[X]) r) : R[T;T⁻¹]) :
      S)
    ((f : (a : R) → S) r : S)
rw₁ : Polynomial.eval₂ f (↑x : S) ((Polynomial.C : (a : R) → R[X]) r) = (f : (a : R) → S) r
⊢ Eq.{u_3 + 1} (α := S) ((eval₂ f x : (a : R[T;T⁻¹]) → S) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) : S)
    ((f : (a : R) → S) r : S)
have rw₂ : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) r : S) ((f : (a : R) → S) r : S)
Tactic: rw [← toLaurent_C, eval₂_toLaurent, Polynomial.eval₂_C]
-- 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ˣ
r : R
n : ℕ
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S)
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (↑n : ℤ))) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x : S) ^ n)
have rw : (eval₂ f x : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) ((monomial n : (a : R) → R[X]) r) : R[T;T⁻¹]) =
  HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x : S) ^ n)
Tactic: rw [← Polynomial.toLaurent_C_mul_T, eval₂_toLaurent, eval₂_monomial]
-- 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ˣ
r : R
n : ℕ
rw :
  (eval₂ f x : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) ((monomial n : (a : R) → R[X]) r) : R[T;T⁻¹]) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x : S) ^ n)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S)
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (↑n : ℤ))) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x : S) ^ n)
have rw₁ : Polynomial.eval₂ f (↑x : S) ((monomial n : (a : R) → R[X]) r) =
  HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x : S) ^ n)
Tactic: rw [← Polynomial.toLaurent_C_mul_T, eval₂_toLaurent, eval₂_monomial]
-- 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ˣ
r : R
n : ℕ
rw :
  (eval₂ f x : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) ((monomial n : (a : R) → R[X]) r) : R[T;T⁻¹]) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x : S) ^ n)
rw₁ :
  Polynomial.eval₂ f (↑x : S) ((monomial n : (a : R) → R[X]) r) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x : S) ^ n)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S)
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (↑n : ℤ))) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x : S) ^ n)
have rw₂ : HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x : S) ^ n) =
  HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x : S) ^ n)
Tactic: rw [← Polynomial.toLaurent_C_mul_T, eval₂_toLaurent, eval₂_monomial]
-- 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ˣ
r : R
n : ℕ
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S)
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (-(↑n : ℤ)))) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x⁻¹ : S) ^ n)
have rw : HMul.hMul (α := S) (β := S) ((eval₂ f x : (a : R[T;T⁻¹]) → S) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) : S)
    ((eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑n : ℤ))) : S) =
  HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x⁻¹ : S) ^ n)
Tactic: rw [map_mul, eval₂_T_neg_n, eval₂_C]
-- 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ˣ
r : R
n : ℕ
rw :
  HMul.hMul (α := S) (β := S) ((eval₂ f x : (a : R[T;T⁻¹]) → S) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) : S)
      ((eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑n : ℤ))) : S) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x⁻¹ : S) ^ n)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S)
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (-(↑n : ℤ)))) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x⁻¹ : S) ^ n)
have rw₁ : HMul.hMul (α := S) ((eval₂ f x : (a : R[T;T⁻¹]) → S) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) : S) ((↑x⁻¹ : S) ^ n) =
  HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x⁻¹ : S) ^ n)
Tactic: rw [map_mul, eval₂_T_neg_n, eval₂_C]
-- 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ˣ
r : R
n : ℕ
rw :
  HMul.hMul (α := S) (β := S) ((eval₂ f x : (a : R[T;T⁻¹]) → S) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) : S)
      ((eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑n : ℤ))) : S) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x⁻¹ : S) ^ n)
rw₁ :
  HMul.hMul (α := S) ((eval₂ f x : (a : R[T;T⁻¹]) → S) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) : S) ((↑x⁻¹ : S) ^ n) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x⁻¹ : S) ^ n)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S)
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (-(↑n : ℤ)))) =
    HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x⁻¹ : S) ^ n)
have rw₂ : HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x⁻¹ : S) ^ n) =
  HMul.hMul (α := S) ((f : (a : R) → S) r : S) ((↑x⁻¹ : S) ^ n)
Tactic: rw [map_mul, eval₂_T_neg_n, eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_3
inst : CommSemiring R
⊢ Eq.{u_3 + 1} (α := R → R[T;T⁻¹])
    (Function.comp (β := R[T;T⁻¹]) (⇑invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) (⇑C : (a : R) → R[T;T⁻¹]))
    (⇑C : (a : R) → R[T;T⁻¹])
have h : ∀ (x : R) (a : ℤ),
  Eq (α := R)
    ((Function.comp (β := R[T;T⁻¹]) (⇑invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) (⇑C : (a : R) → R[T;T⁻¹]) x : (a : ℤ) → R) a :
      R)
    ((((C : (a : R) → R[T;T⁻¹]) x : R[T;T⁻¹]) : (a : ℤ) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_3
inst : CommSemiring R
t : R
⊢ Eq (α := R[T;T⁻¹]) ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) t) : R[T;T⁻¹])
    ((C : (a : R) → R[T;T⁻¹]) t : R[T;T⁻¹])
have h : ∀ (a : ℤ),
  Eq (α := R) ((((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) t) : R[T;T⁻¹]) : (a : ℤ) → R) a : R)
    ((((C : (a : R) → R[T;T⁻¹]) t : R[T;T⁻¹]) : (a : ℤ) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_3
inst : CommSemiring R
x : R[T;T⁻¹]
⊢ (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) x) = x
have h : ∀ (a : ℤ),
  Eq (α := R)
    ((((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) x) : R[T;T⁻¹]) : (a : ℤ) → R) a : R)
    ((x : (a : ℤ) → R) a : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (hypothesis)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
⊢ (toLaurent : (a : R[X]) → R[T;T⁻¹]) p.reverse =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
      ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p) : R[T;T⁻¹]) (T (↑p.natDegree : ℤ))
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h : Nontrivial R
⊢ (toLaurent : (a : R[X]) → R[T;T⁻¹]) p.reverse =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
      ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p) : R[T;T⁻¹]) (T (↑p.natDegree : ℤ))
have M0 : (toLaurent : (a : R[X]) → R[T;T⁻¹]) (reverse 0) =
  HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
    ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) 0) : R[T;T⁻¹])
    (T (↑(natDegree.{u_3} (R := R) 0) : ℤ))
Tactic: induction p using Polynomial.recOnHorner with
  | M0 => simp
  | MC _ _ _ _ ih => simp [add_mul, ← ih]
  | MX _ hp => simpa [natDegree_mul_X hp]
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
h : Nontrivial R
M0 :
  (toLaurent : (a : R[X]) → R[T;T⁻¹]) (reverse 0) =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
      ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) 0) : R[T;T⁻¹])
      (T (↑(natDegree.{u_3} (R := R) 0) : ℤ))
⊢ (toLaurent : (a : R[X]) → R[T;T⁻¹]) p.reverse =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
      ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p) : R[T;T⁻¹]) (T (↑p.natDegree : ℤ))
have MC : ∀ (p : R[X]) (a : R),
  p.coeff 0 = 0 →
    a ≠ 0 →
      ∀
        (ih :
          (toLaurent : (a : R[X]) → R[T;T⁻¹]) p.reverse =
            HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
              ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p) : R[T;T⁻¹])
              (T (↑p.natDegree : ℤ))),
        (toLaurent : (a : R[X]) → R[T;T⁻¹])
            (HAdd.hAdd (β := R[X]) p ((Polynomial.C : (a : R) → R[X]) a : R[X])).reverse =
          HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹])
            ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹])
                ((toLaurent : (a : R[X]) → R[T;T⁻¹])
                  (HAdd.hAdd (β := R[X]) p ((Polynomial.C : (a : R) → R[X]) a : R[X]))) :
              R[T;T⁻¹])
            (T (↑(HAdd.hAdd (β := R[X]) p ((Polynomial.C : (a : R) → R[X]) a : R[X])).natDegree : ℤ))
Tactic: induction p using Polynomial.recOnHorner with
  | M0 => simp
  | MC _ _ _ _ ih => simp [add_mul, ← ih]
  | MX _ hp => simpa [natDegree_mul_X hp]
Cleared hypotheses: p