awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) : ℤ))
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 : ℤ))
⊢ (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 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 : ℤ))
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_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
⊢ (Finsupp.sum (AddMonoidAlgebra.single n r) fun (n : ℤ) (r : R) ↦ r • (↑(x ^ n) : S)) = r • (↑(x ^ n) : S)
have rw : r • (↑(x ^ n) : S) = r • (↑(x ^ n) : S)
Tactic: rw [Finsupp.sum_single_index (zero_smul R (x ^ n).val)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ (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)
have rw : smeval (AddMonoidAlgebra.single n r) x = r • (↑(x ^ n) : S)
Tactic: rw [← single_eq_C_mul_T, smeval_single]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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)
⊢ (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)
have rw₁ : r • (↑(x ^ n) : S) = r • (↑(x ^ n) : S)
Tactic: rw [← single_eq_C_mul_T, smeval_single]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ smeval.{u_1, u_2} (R := R) ((C : (a : R) → R[T;T⁻¹]) r) x = HSMul.hSMul (β := S) r 1
have rw : smeval (AddMonoidAlgebra.single 0 r) x = HSMul.hSMul (β := S) r 1
Tactic: rw [← single_eq_C, smeval_single x (0 : ℤ) r, zpow_zero, Units.val_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ smeval.{u_1, u_2} (R := R) ((C : (a : R) → R[T;T⁻¹]) r) x = HSMul.hSMul (β := S) r 1
have rw₁ : r • (↑(HPow.hPow (β := ℤ) x 0) : S) = HSMul.hSMul (β := S) r 1
Tactic: rw [← single_eq_C, smeval_single x (0 : ℤ) r, zpow_zero, Units.val_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ smeval.{u_1, u_2} (R := R) ((C : (a : R) → R[T;T⁻¹]) r) x = HSMul.hSMul (β := S) r 1
have rw₂ : HSMul.hSMul (β := S) r (↑1 : S) = HSMul.hSMul (β := S) r 1
Tactic: rw [← single_eq_C, smeval_single x (0 : ℤ) r, zpow_zero, Units.val_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ smeval.{u_1, u_2} (R := R) ((C : (a : R) → R[T;T⁻¹]) r) x = HSMul.hSMul (β := S) r 1
have rw₃ : HSMul.hSMul (β := S) r 1 = HSMul.hSMul (β := S) r 1
Tactic: rw [← single_eq_C, smeval_single x (0 : ℤ) r, zpow_zero, Units.val_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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ˣ
⊢ smeval.{u_1, u_2} (R := R) (T n) x = (↑(x ^ n) : S)
have rw : smeval.{u_1, u_2} (R := R) (AddMonoidAlgebra.single n 1) x = (↑(x ^ n) : S)
Tactic: rw [T, smeval_single, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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)
⊢ smeval.{u_1, u_2} (R := R) (T n) x = (↑(x ^ n) : S)
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 (↑(x ^ n) : S) = (↑(x ^ n) : S)
Tactic: rw [T, smeval_single, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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)
⊢ smeval.{u_1, u_2} (R := R) (T n) x = (↑(x ^ n) : S)
have rw₂ : (↑(x ^ n) : S) = (↑(x ^ n) : S)
Tactic: rw [T, smeval_single, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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ˣ
⊢ smeval.{u_1, u_2} (R := R) 1 x = 1
have rw : smeval.{u_1, u_2} (R := R) (T 0) x = 1
Tactic: rw [← T_zero, smeval_T_pow 0 x, zpow_zero, Units.val_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ smeval.{u_1, u_2} (R := R) 1 x = 1
have rw₁ : (↑(HPow.hPow (β := ℤ) x 0) : S) = 1
Tactic: rw [← T_zero, smeval_T_pow 0 x, zpow_zero, Units.val_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ smeval.{u_1, u_2} (R := R) 1 x = 1
have rw₂ : Eq.{u_2 + 1} (α := S) (↑1 : S) 1
Tactic: rw [← T_zero, smeval_T_pow 0 x, zpow_zero, Units.val_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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
⊢ smeval.{u_1, u_2} (R := R) 1 x = 1
have rw₃ : Eq.{u_2 + 1} (α := Sˣ) 1 1
Tactic: rw [← T_zero, smeval_T_pow 0 x, zpow_zero, Units.val_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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ˣ
⊢ (f + g).smeval x = f.smeval x + g.smeval x
have 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))
Tactic: simp only [smeval_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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ˣ
⊢ (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))
have 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))
Tactic: rw [Finsupp.sum_add_index (fun n _ => zero_smul R (x ^ n).val) (fun n _ r r' => add_smul r r' _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x = r • p.smeval x
hq : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x = r • q.smeval x
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)).smeval x = r • (p + q).smeval x
have add : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
        HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval
    x =
  r • (p + q).smeval x
Tactic: rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x = r • p.smeval x
hq : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x = r • q.smeval x
add :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
          HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval
      x =
    r • (p + q).smeval x
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)).smeval x = r • (p + q).smeval x
have add₁ : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
    (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
  r • (p + q).smeval x
Tactic: rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x = r • p.smeval x
hq : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x = r • q.smeval x
add :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
          HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval
      x =
    r • (p + q).smeval x
add₁ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • (p + q).smeval x
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)).smeval x = r • (p + q).smeval x
have add₂ : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
    (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
  r • (p.smeval x + q.smeval x)
Tactic: rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x = r • p.smeval x
hq : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x = r • q.smeval x
add :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
          HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval
      x =
    r • (p + q).smeval x
add₁ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • (p + q).smeval x
add₂ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • (p.smeval x + q.smeval x)
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)).smeval x = r • (p + q).smeval x
have add₃ : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
    (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
  r • p.smeval x + r • q.smeval x
Tactic: rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x = r • p.smeval x
hq : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x = r • q.smeval x
add :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
          HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval
      x =
    r • (p + q).smeval x
add₁ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • (p + q).smeval x
add₂ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • (p.smeval x + q.smeval x)
add₃ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • p.smeval x + r • q.smeval x
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)).smeval x = r • (p + q).smeval x
have add₄ : r • p.smeval x + (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
  r • p.smeval x + r • q.smeval x
Tactic: rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
p q : R[T;T⁻¹]
hp : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x = r • p.smeval x
hq : (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x = r • q.smeval x
add :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p +
          HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval
      x =
    r • (p + q).smeval x
add₁ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • (p + q).smeval x
add₂ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • (p.smeval x + q.smeval x)
add₃ :
  (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p).smeval x +
      (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • p.smeval x + r • q.smeval x
add₄ :
  r • p.smeval x + (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q).smeval x =
    r • p.smeval x + r • q.smeval x
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)).smeval x = r • (p + q).smeval x
have add₅ : r • p.smeval x + r • q.smeval x = r • p.smeval x + r • q.smeval x
Tactic: rw [mul_add, smeval_add, smeval_add, smul_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
n : ℤ
s : R
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
          (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n))).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
have C_mul_T : (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
          ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) *
        T n).smeval
    x =
  r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
Tactic: rw [← mul_assoc, ← map_mul, smeval_C_mul_T_n, smeval_C_mul_T_n, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
n : ℤ
s : R
C_mul_T :
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
            ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) *
          T n).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
          (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n))).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
have C_mul_T₁ : (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (r * s) : R[T;T⁻¹]) (T n)).smeval x =
  r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
Tactic: rw [← mul_assoc, ← map_mul, smeval_C_mul_T_n, smeval_C_mul_T_n, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
n : ℤ
s : R
C_mul_T :
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
            ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) *
          T n).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
C_mul_T₁ :
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (r * s) : R[T;T⁻¹]) (T n)).smeval x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
          (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n))).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
have C_mul_T₂ : (r * s) • (↑(x ^ n) : S) =
  r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
Tactic: rw [← mul_assoc, ← map_mul, smeval_C_mul_T_n, smeval_C_mul_T_n, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
n : ℤ
s : R
C_mul_T :
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
            ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) *
          T n).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
C_mul_T₁ :
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (r * s) : R[T;T⁻¹]) (T n)).smeval x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
C_mul_T₂ :
  (r * s) • (↑(x ^ n) : S) =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
          (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n))).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
have C_mul_T₃ : (r * s) • (↑(x ^ n) : S) = r • s • (↑(x ^ n) : S)
Tactic: rw [← mul_assoc, ← map_mul, smeval_C_mul_T_n, smeval_C_mul_T_n, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
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 : R[T;T⁻¹]
x : Sˣ
r : R
n : ℤ
s : R
C_mul_T :
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
            ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) *
          T n).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
C_mul_T₁ :
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (r * s) : R[T;T⁻¹]) (T n)).smeval x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
C_mul_T₂ :
  (r * s) • (↑(x ^ n) : S) =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
C_mul_T₃ : (r * s) • (↑(x ^ n) : S) = r • s • (↑(x ^ n) : S)
⊢ (HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
          (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n))).smeval
      x =
    r • (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n)).smeval x
have C_mul_T₄ : r • s • (↑(x ^ n) : S) = r • s • (↑(x ^ n) : S)
Tactic: rw [← mul_assoc, ← map_mul, smeval_C_mul_T_n, smeval_C_mul_T_n, mul_smul]