awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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ˣ
n : ℕ
⊢ IsUnit (M := 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)
              ((fun (x : ℕ) ↦ HPow.hPow (α := R[X]) X x) n) ⋯) :
          R[X]) :
      S)

Tactic:
simpa only [coe_eval₂RingHom, eval₂_X_pow] using x.isUnit.pow n

Premises used: Polynomial.eval₂_X_pow, IsUnit.pow, Units.isUnit, Polynomial.coe_eval₂RingHom
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
p : R[X]
unfold :
  (IsLocalization.lift ⋯ : (a : R[T;T⁻¹]) → S) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹]) =
    Polynomial.eval₂ f (↑x : S) p
⊢ (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

Tactic:
unfold eval₂

Premises used: LaurentPolynomial.eval₂
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
rw₂ rw₃ : Polynomial.eval₂ f (↑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

Tactic:
rw [← algebraMap_eq_toLaurent, IsLocalization.lift_eq, coe_eval₂RingHom]

Premises used: IsLocalization.lift_eq, LaurentPolynomial.algebraMap_eq_toLaurent, Polynomial.coe_eval₂RingHom
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
rw₂ rw₃ : (↑x : S) ^ n = (↑x : S) ^ n
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (↑n : ℤ)) = (↑x : S) ^ n

Tactic:
rw [← Polynomial.toLaurent_X_pow, eval₂_toLaurent, eval₂_X_pow]

Premises used: Polynomial.eval₂_X_pow, Polynomial.toLaurent_X_pow, LaurentPolynomial.eval₂_toLaurent
-- Module: Mathlib.Algebra.Polynomial.Laurent
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)
      (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
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑n : ℤ))) = (↑x⁻¹ : S) ^ n

Tactic:
rw [← mk'_one_X_pow]

Premises used: LaurentPolynomial.mk'_one_X_pow
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_3
inst_1 : CommSemiring S
f : R →+* S
x : Sˣ
n : ℕ
unfold :
  (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
⊢ (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

Tactic:
unfold eval₂

Premises used: LaurentPolynomial.eval₂
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
rw₆ rw₇ : Eq.{u_3 + 1} (α := S) 1 1
⊢ (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

Tactic:
rw [IsLocalization.lift_mk'_spec, map_one, coe_eval₂RingHom, eval₂_X_pow, ← mul_pow,
    Units.mul_inv, one_pow]

Premises used: one_pow, Polynomial.eval₂_X_pow, IsLocalization.lift_mk'_spec, Units.mul_inv, map_one, mul_pow, Polynomial.coe_eval₂RingHom
-- Module: Mathlib.Algebra.Polynomial.Laurent
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)
neg : ∀ (hn : n < 0), (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)

Tactic:
by_cases! hn : 0 ≤ n
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
⊢ 0 ≤ n

Tactic:
hn
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
pos : ∀ (n : ℕ), (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (↑n : ℤ)) = (↑(HPow.hPow (β := ℤ) x (↑n : ℤ)) : S)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T n) = (↑(x ^ n) : S)

Tactic:
lift n to ℕ using hn
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ)) = (↑(HPow.hPow (β := ℤ) x (↑n : ℤ)) : S)

Tactic:
apply eval₂_T_n

Premises used: LaurentPolynomial.eval₂_T_n
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
neg :
  ∀ (m : ℕ) (hn : LT.lt (α := ℤ) (-(↑m : ℤ)) 0),
    (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑m : ℤ))) = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T n) = (↑(x ^ n) : S)

Tactic:
obtain ⟨m, rfl⟩ := Int.exists_eq_neg_ofNat hn.le

Premises used: LT.lt.le, Int.exists_eq_neg_ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
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)
neg₄ neg₅ : (↑x⁻¹ : S) ^ m = (↑x⁻¹ : S) ^ m
⊢ (eval₂ f x : (a : R[T;T⁻¹]) → S) (T (-(↑m : ℤ))) = (↑(HPow.hPow (β := ℤ) x (-(↑m : ℤ))) : S)

Tactic:
rw [eval₂_T_neg_n, zpow_neg, zpow_natCast, ← inv_pow, Units.val_pow_eq_pow_val]

Premises used: zpow_natCast, inv_pow, zpow_neg, LaurentPolynomial.eval₂_T_neg_n, Units.val_pow_eq_pow_val
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
rw₂ rw₃ : Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) r : 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)

Tactic:
rw [← toLaurent_C, eval₂_toLaurent, Polynomial.eval₂_C]

Premises used: LaurentPolynomial.eval₂_toLaurent, Polynomial.eval₂_C, Polynomial.toLaurent_C
-- Module: Mathlib.Algebra.Polynomial.Laurent
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)
rw₂ 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)
⊢ (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)

Tactic:
rw [← Polynomial.toLaurent_C_mul_T, eval₂_toLaurent, eval₂_monomial]

Premises used: Polynomial.eval₂_monomial, Polynomial.toLaurent_C_mul_T, LaurentPolynomial.eval₂_toLaurent
-- Module: Mathlib.Algebra.Polynomial.Laurent
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)
rw₂ 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)
⊢ (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)

Tactic:
rw [map_mul, eval₂_T_neg_n, eval₂_C]

Premises used: map_mul, LaurentPolynomial.eval₂_C, LaurentPolynomial.eval₂_T_neg_n
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 ^ n) : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
n : ℤ
⊢ Eq.{u_3 + 1} (α := R[T;T⁻¹]) ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) (T n) : R[T;T⁻¹]) (T (-n) : R[T;T⁻¹])

Tactic:
AddMonoidAlgebra.domCongr_single ..

Premises used: LaurentPolynomial.T, AddMonoidAlgebra.domCongr_single, Int.neg, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
f : R[T;T⁻¹]
n : ℤ
⊢ Eq (α := R) ((((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) f : R[T;T⁻¹]) : (a : ℤ) → R) n : R) ((f : (a : ℤ) → R) (-n) : R)

Tactic:
simp [invert]

Premises used: LaurentPolynomial.invert
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
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)
⊢ 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⁻¹])

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
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:
simp
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
t : R
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)
⊢ 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⁻¹])

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
t : R
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:
simp
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
x : R[T;T⁻¹]
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)
⊢ (invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) ((invert : (a : R[T;T⁻¹]) → R[T;T⁻¹]) x) = x

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
x : R[T;T⁻¹]
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:
simp
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
⊢ Eq.{u_3 + 1} (α := R[T;T⁻¹] ≃ₐ[R] R[T;T⁻¹]) (AlgEquiv.symm invert) invert

Tactic:
rfl

Premises used: AlgEquiv.symm, AddEquiv.neg, LaurentPolynomial.invert, Equiv.symm, rfl, AddEquiv.symm, AddMonoidAlgebra.domCongr
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
p : R[X]
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
h : Nontrivial R
⊢ (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:
simp
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
h : Nontrivial R
p : R[X]
a : R
h_1 : p.coeff 0 = 0
h_2 : 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:
simp [add_mul, ← ih]

Premises used: add_mul
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
h : Nontrivial R
p : R[X]
hp : p ≠ 0
h_1 :
  (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⁻¹]) (p * 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⁻¹]) (p * X)) : R[T;T⁻¹])
      (T (↑(p * X).natDegree : ℤ))

Tactic:
simpa [natDegree_mul_X hp]

Premises used: Polynomial.natDegree_mul_X
-- Module: Mathlib.Algebra.Polynomial.Laurent
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) : ℤ))
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 : ℤ))
MX :
  ∀ (p : R[X]) (hp : p ≠ 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 : ℤ)) →
      (toLaurent : (a : R[X]) → R[T;T⁻¹]) (p * 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⁻¹]) (p * X)) : R[T;T⁻¹])
          (T (↑(p * X).natDegree : ℤ))
⊢ (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 : ℤ))

Tactic:
induction p using Polynomial.recOnHorner with
  | M0 => simp
  | MC _ _ _ _ ih => simp [add_mul, ← ih]
  | MX _ hp => simpa [natDegree_mul_X hp]

Premises used: add_mul
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : SMulWithZero R S
inst_3 : Monoid S
f : R[T;T⁻¹]
x : Sˣ
⊢ f.smeval x = Finsupp.sum f fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S)

Tactic:
rfl

Premises used: rfl, LaurentPolynomial.smeval
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : SMulWithZero R S
inst_3 : Monoid S
f : R[T;T⁻¹]
x : Sˣ
⊢ f.smeval x = f.smeval x

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : SMulWithZero R S
inst_3 : Monoid S
x : Sˣ
⊢ smeval.{u_1, u_2} (R := R) 0 x = 0

Tactic:
simp only [smeval_eq_sum, Finsupp.sum_zero_index]

Premises used: LaurentPolynomial.smeval_eq_sum, Finsupp.sum_zero_index
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : SMulWithZero R S
inst_3 : Monoid S
x : Sˣ
n : ℤ
r : R
rw rw₁ : r • (↑(x ^ n) : S) = r • (↑(x ^ n) : S)
⊢ (Finsupp.sum (AddMonoidAlgebra.single n r) fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S)) = r • (↑(x ^ n) : S)

Tactic:
rw [Finsupp.sum_single_index (zero_smul R (x ^ n).val)]

Premises used: Finsupp.sum_single_index
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : SMulWithZero R S
inst_3 : Monoid S
x : Sˣ
n : ℤ
r : R
rw : smeval (AddMonoidAlgebra.single n r) x = r • (↑(x ^ n) : S)
rw₁ rw₂ : r • (↑(x ^ n) : S) = r • (↑(x ^ n) : S)
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T n)).smeval x =
    r • (↑(x ^ n) : S)

Tactic:
rw [← single_eq_C_mul_T, smeval_single]

Premises used: LaurentPolynomial.single_eq_C_mul_T, LaurentPolynomial.smeval_single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : SMulWithZero R S
inst_3 : Monoid S
x : Sˣ
r : R
rw : smeval (AddMonoidAlgebra.single 0 r) x = HSMul.hSMul (β := S) r 1
rw₁ : r • (↑(HPow.hPow (β := ℤ) x 0) : S) = HSMul.hSMul (β := S) r 1
rw₂ : HSMul.hSMul (β := S) r (↑1 : S) = HSMul.hSMul (β := S) r 1
rw₃ rw₄ : HSMul.hSMul (β := S) r 1 = HSMul.hSMul (β := S) r 1
⊢ smeval.{u_1, u_2} (R := R) ((C : (a : R) → R[T;T⁻¹]) r) x = HSMul.hSMul (β := S) r 1

Tactic:
rw [← single_eq_C, smeval_single x (0 : ℤ) r, zpow_zero, Units.val_one]

Premises used: zpow_zero, LaurentPolynomial.single_eq_C, LaurentPolynomial.smeval_single, Units.val_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : MulActionWithZero R S
inst_3 : Monoid S
n : ℤ
x : Sˣ
rw : smeval.{u_1, u_2} (R := R) (AddMonoidAlgebra.single n 1) x = (↑(x ^ n) : S)
rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (↑(x ^ n) : S) = (↑(x ^ n) : S)
rw₂ rw₃ : (↑(x ^ n) : S) = (↑(x ^ n) : S)
⊢ smeval.{u_1, u_2} (R := R) (T n) x = (↑(x ^ n) : S)

Tactic:
rw [T, smeval_single, one_smul]

Premises used: LaurentPolynomial.T, one_smul, LaurentPolynomial.smeval_single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : MulActionWithZero R S
inst_3 : Monoid S
x : Sˣ
rw : smeval.{u_1, u_2} (R := R) (T 0) x = 1
rw₁ : (↑(HPow.hPow (β := ℤ) x 0) : S) = 1
rw₂ : Eq.{u_2 + 1} (α := S) (↑1 : S) 1
rw₃ rw₄ : Eq.{u_2 + 1} (α := Sˣ) 1 1
⊢ smeval.{u_1, u_2} (R := R) 1 x = 1

Tactic:
rw [← T_zero, smeval_T_pow 0 x, zpow_zero, Units.val_eq_one]

Premises used: LaurentPolynomial.smeval_T_pow, zpow_zero, LaurentPolynomial.T_zero, Units.val_eq_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : Module R S
inst_3 : Monoid S
f g : R[T;T⁻¹]
x : Sˣ
simp :
  (Finsupp.sum (f + g) fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S)) =
    HAdd.hAdd (α := S) (Finsupp.sum f fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S))
      (Finsupp.sum g fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S))
⊢ (f + g).smeval x = f.smeval x + g.smeval x

Tactic:
simp only [smeval_eq_sum]

Premises used: LaurentPolynomial.smeval_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid S
inst_2 : Module R S
inst_3 : Monoid S
f g : R[T;T⁻¹]
x : Sˣ
rw rw₁ :
  HAdd.hAdd (α := S) (Finsupp.sum f fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S))
      (Finsupp.sum g fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S)) =
    HAdd.hAdd (α := S) (Finsupp.sum f fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S))
      (Finsupp.sum g fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S))
⊢ (Finsupp.sum (f + g) fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S)) =
    HAdd.hAdd (α := S) (Finsupp.sum f fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S))
      (Finsupp.sum g fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S))

Tactic:
rw [Finsupp.sum_add_index (fun n _ => zero_smul R (x ^ n).val) (fun n _ r r' => add_smul r r' _)]

Premises used: Finsupp.sum_add_index