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
n : ℤ
r : R
⊢ Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯)
    (toFinsupp (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0))
have pos : ∀ (n0 : 0 ≤ n),
  Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) sorry)
    (toFinsupp ((monomial n.toNat : (a : R) → R[X]) r))
Tactic: split_ifs with n0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
pos :
  ∀ (n0 : 0 ≤ n),
    Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯)
      (toFinsupp ((monomial n.toNat : (a : R) → R[X]) r))
⊢ Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯)
    (toFinsupp (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0))
have neg : ∀ (n0 : ¬0 ≤ n), Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) sorry) (toFinsupp 0)
Tactic: split_ifs with n0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : 0 ≤ n
⊢ Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯) (AddMonoidAlgebra.single n.toNat r)
have pos : ∀ (n : ℕ),
  Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single (↑n : ℤ) r) sorry)
    (AddMonoidAlgebra.single (Int.toNat (↑n : ℤ)) r)
Tactic: lift n to ℕ using n0
Cleared hypotheses: n, n0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
⊢ Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯) (toFinsupp 0)
have neg : Eq (α := R[X]) { toFinsupp := Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) sorry } 0
Tactic: rw [toFinsupp_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
⊢ Eq (α := R[X]) { toFinsupp := Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯ } 0
have neg : ∀ (a : ℕ),
  Polynomial.coeff { toFinsupp := Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) sorry : R[X] } a =
    Polynomial.coeff 0 a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
a : ℕ
⊢ Polynomial.coeff { toFinsupp := Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯ : R[X] } a =
    Polynomial.coeff 0 a
have this : (↑a : ℤ) ≠ n
Tactic: have : a ≠ n := by lia
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ LeftInverse.{u_1 + 1, u_1 + 1} (α := R[X]) (β := R[T;T⁻¹]) (⇑trunc : (a : R[T;T⁻¹]) → R[X])
    (⇑toLaurent : (a : R[X]) → R[T;T⁻¹])
have refine_1 : ∀ (f p q : R[X]),
  (trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p) = p →
    (trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) q) = q →
      (trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (p + q)) = p + q
Tactic: refine fun f => f.induction_on' ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
refine_1 :
  ∀ (f p q : R[X]),
    (trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p) = p →
      (trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) q) = q →
        (trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (p + q)) = p + q
⊢ LeftInverse.{u_1 + 1, u_1 + 1} (α := R[X]) (β := R[T;T⁻¹]) (⇑trunc : (a : R[T;T⁻¹]) → R[X])
    (⇑toLaurent : (a : R[X]) → R[T;T⁻¹])
have refine_2 : ∀ (f : R[X]) (n : ℕ) (a : R),
  Eq (α := R[X])
    ((trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) ((monomial n : (a : R) → R[X]) a)) : R[X])
    ((monomial n : (a : R) → R[X]) a : R[X])
Tactic: refine fun f => f.induction_on' ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
⊢ ∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = f * T (↑n : ℤ)
have refine_1 : ∀ (p q : R[T;T⁻¹]),
  (∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = p * T (↑n : ℤ)) →
    (∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = q * T (↑n : ℤ)) →
      ∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = (p + q) * T (↑n : ℤ)
Tactic: refine f.induction_on' ?_ fun n a => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
refine_1 :
  ∀ (p q : R[T;T⁻¹]),
    (∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = p * T (↑n : ℤ)) →
      (∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = q * T (↑n : ℤ)) →
        ∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = (p + q) * T (↑n : ℤ)
⊢ ∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = f * T (↑n : ℤ)
have refine_2 : ∀ (n : ℤ) (a : R),
  ∃ (n_1 : ℕ) (f' : R[X]),
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' =
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n) * T (↑n_1 : ℤ)
Tactic: refine f.induction_on' ?_ fun n a => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : (toLaurent : (a : R[X]) → R[T;T⁻¹]) fn = f * T (↑m : ℤ)
n : ℕ
gn : R[X]
hg : (toLaurent : (a : R[X]) → R[T;T⁻¹]) gn = g * T (↑n : ℤ)
⊢ ∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = (f + g) * T (↑n : ℤ)
have refine_1 : (toLaurent : (a : R[X]) → R[T;T⁻¹]) (fn * HPow.hPow (α := R[X]) X n + gn * HPow.hPow (α := R[X]) X m) =
  (f + g) * T (↑(m + n) : ℤ)
Tactic: refine ⟨m + n, fn * X ^ n + gn * X ^ m, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
⊢ ∃ (n_1 : ℕ) (f' : R[X]),
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' =
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n) * T (↑n_1 : ℤ)
have refine_2 : ∀ (n : ℕ),
  ∃ (n_1 : ℕ) (f' : R[X]),
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' =
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (Int.ofNat n)) * T (↑n_1 : ℤ)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
refine_2 :
  ∀ (n : ℕ),
    ∃ (n_1 : ℕ) (f' : R[X]),
      (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' =
        HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (Int.ofNat n)) *
          T (↑n_1 : ℤ)
⊢ ∃ (n_1 : ℕ) (f' : R[X]),
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' =
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n) * T (↑n_1 : ℤ)
have refine_2₁ : ∀ (n : ℕ),
  ∃ (n_1 : ℕ) (f' : R[X]),
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' =
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (Int.negSucc n)) *
        T (↑n_1 : ℤ)
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℕ
⊢ ∃ (n_1 : ℕ) (f' : R[X]),
    (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' =
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (Int.negSucc n)) *
        T (↑n_1 : ℤ)
have refine_2 : (toLaurent : (a : R[X]) → R[T;T⁻¹]) ((Polynomial.C : (a : R) → R[X]) a) =
  HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (Int.negSucc n)) *
    T (↑(n + 1) : ℤ)
Tactic: refine ⟨n + 1, Polynomial.C a, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T :
  ∀ (f : R[X]) (n : ℕ),
    motive
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
⊢ motive f
have rcases : ∀ (n : ℕ) (f' : R[X]) (hf : (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = f * T (↑n : ℤ)), motive f
Tactic: rcases f.exists_T_pow with ⟨n, f', hf⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
mul_T :
  ∀ (f : R[X]) (n : ℕ),
    motive
      (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
n : ℕ
f' : R[X]
hf : (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = f * T (↑n : ℤ)
⊢ motive f
have rw : motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f' : R[T;T⁻¹]) (T (-(↑n : ℤ))))
Tactic: rw [← mul_one f, ← T_zero, ← Nat.cast_zero, ← Nat.sub_self n, Nat.cast_sub rfl.le, T_sub,
    ← mul_assoc, ← hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
⊢ Q f
have mul_T : ∀ (f : R[X]) (n : ℕ),
  Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
Tactic: induction f using LaurentPolynomial.induction_on_mul_T with | _ f n
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
⊢ Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑(n + 1) : ℤ))))
have mul_T : Q
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑(n + 1) : ℤ))) *
    T 1)
Tactic: convert! QT _ _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
have mul_T : Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑0 : ℤ))))
Tactic: induction n with
  | zero => simpa only [Nat.cast_zero, neg_zero, T_zero, mul_one] using Qf _
  | succ n hn => convert! QT _ _; simpa using hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
mul_T : Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑0 : ℤ))))
⊢ Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))
have mul_T₁ : ∀ (n : ℕ)
  (hn :
    Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))),
  Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑(n + 1) : ℤ))))
Tactic: induction n with
  | zero => simpa only [Nat.cast_zero, neg_zero, T_zero, mul_one] using Qf _
  | succ n hn => convert! QT _ _; simpa using hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℤ
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).support ⊆ {n}
have rw : Finsupp.support (AddMonoidAlgebra.single n a) ⊆ {n}
Tactic: rw [← single_eq_C_mul_T]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).support = {n}
have rw : Finsupp.support (AddMonoidAlgebra.single n a) = {n}
Tactic: rw [← single_eq_C_mul_T]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding f.support)
have generalize : ∀ (s : Finset ℕ) (hd : f.support = s),
  Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding s)
Tactic: generalize hd : f.support = s
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
s : Finset ℕ
hd : f.support = s
⊢ Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding s)
have revert : ∀ (f : R[X]) (hd : f.support = s),
  Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding s)
Tactic: revert f
Cleared hypotheses: f, hd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
s : Finset ℕ
⊢ ∀ (f : R[X]) (hd : f.support = s),
    Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
      (Finset.map Nat.castEmbedding s)
have refine_1 : ∀ (f : R[X]) (hd : f.support = ∅),
  Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding ∅)
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
s : Finset ℕ
refine_1 :
  ∀ (f : R[X]) (hd : f.support = ∅),
    Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
      (Finset.map Nat.castEmbedding ∅)
⊢ ∀ (f : R[X]) (hd : f.support = s),
    Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
      (Finset.map Nat.castEmbedding s)
have refine_2 : ∀ (a : ℕ) (s : Finset ℕ),
  a ∉ s →
    (∀ (f : R[X]) (hd : f.support = s),
        Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
          (Finset.map Nat.castEmbedding s)) →
      ∀ (f : R[X]) (hd : f.support = insert a s),
        Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
          (Finset.map Nat.castEmbedding (insert a s))
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.support = ∅
⊢ Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding ∅)
have refine_1 : f = 0
Tactic: rw [Finset.map_empty, Finsupp.support_eq_empty, toLaurent_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf :
  ∀ (f : R[X]) (hd : f.support = s),
    Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
      (Finset.map Nat.castEmbedding s)
f : R[X]
fs : f.support = insert a s
⊢ Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)))
    (Finset.map Nat.castEmbedding s)
have refine : (Polynomial.erase a f).support = s
Tactic: refine hf (f.erase a) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf :
  ∀ (f : R[X]) (hd : f.support = s),
    Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
      (Finset.map Nat.castEmbedding s)
f : R[X]
fs : f.support = insert a s
⊢ Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding (insert a s))
have this : Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)))
  (Finset.map Nat.castEmbedding s)
Tactic: have : (erase a f).toLaurent.support = s.map Nat.castEmbedding := by
      refine hf (f.erase a) ?_
      simp only [fs, Finset.erase_eq_of_notMem as, Polynomial.support_erase,
        Finset.erase_insert_eq_erase]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf :
  ∀ (f : R[X]) (hd : f.support = s),
    Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
      (Finset.map Nat.castEmbedding s)
f : R[X]
fs : f.support = insert a s
this :
  Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)))
    (Finset.map Nat.castEmbedding s)
⊢ Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding (insert a s))
have refine_2 : (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (f.coeff a) : R[T;T⁻¹]) (T (↑a : ℤ))).support ∪
    Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)) =
  singleton (α := ℤ) ((Nat.castEmbedding : (a : ℕ) → ℤ) a : ℤ) ∪
    Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f))
Tactic: rw [← monomial_add_erase f a, Finset.map_insert, ← this, map_add, Polynomial.toLaurent_C_mul_T,
      support_add_eq, Finset.insert_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf :
  ∀ (f : R[X]) (hd : f.support = s),
    Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
      (Finset.map Nat.castEmbedding s)
f : R[X]
fs : f.support = insert a s
this :
  Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)))
    (Finset.map Nat.castEmbedding s)
refine_2 :
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (f.coeff a) : R[T;T⁻¹]) (T (↑a : ℤ))).support ∪
      Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)) =
    singleton (α := ℤ) ((Nat.castEmbedding : (a : ℕ) → ℤ) a : ℤ) ∪
      Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f))
⊢ Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding (insert a s))
have refine_2₁ : Disjoint
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (f.coeff a) : R[T;T⁻¹]) (T (↑a : ℤ))).support
  (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)))
Tactic: rw [← monomial_add_erase f a, Finset.map_insert, ← this, map_add, Polynomial.toLaurent_C_mul_T,
      support_add_eq, Finset.insert_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf :
  ∀ (f : R[X]) (hd : f.support = s),
    Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
      (Finset.map Nat.castEmbedding s)
f : R[X]
fs : f.support = insert a s
this :
  Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)))
    (Finset.map Nat.castEmbedding s)
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (f.coeff a) : R[T;T⁻¹]) (T (↑a : ℤ))).support ∪
      Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)) =
    singleton (α := ℤ) ((Nat.castEmbedding : (a : ℕ) → ℤ) a : ℤ) ∪
      Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f))
have refine_2 : (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (f.coeff a) : R[T;T⁻¹]) (T (↑a : ℤ))).support =
  singleton (α := ℤ) ((Nat.castEmbedding : (a : ℕ) → ℤ) a : ℤ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf :
  ∀ (f : R[X]) (hd : f.support = s),
    Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
      (Finset.map Nat.castEmbedding s)
f : R[X]
fs : f.support = insert a s
this :
  Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)))
    (Finset.map Nat.castEmbedding s)
⊢ Disjoint
    (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (f.coeff a) : R[T;T⁻¹]) (T (↑a : ℤ))).support
    (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (Polynomial.erase a f)))
have refine_2 : Disjoint
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) (f.coeff a) : R[T;T⁻¹]) (T (↑a : ℤ))).support
  (Finset.map Nat.castEmbedding s)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
h : f = 0
⊢ f.degree = ⊥
have rw : degree.{u_1} (R := R) 0 = ⊥
Tactic: rw [h, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
h : f = 0
rw : degree.{u_1} (R := R) 0 = ⊥
⊢ f.degree = ⊥
have rw₁ : Eq (α := WithBot ℤ) ⊥ ⊥
Tactic: rw [h, degree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
⊢ f.degree = ⊥ ↔ f = 0
have refine : ∀ (h : f.degree = ⊥), f = 0
Tactic: refine ⟨fun h => ?_, fun h => by rw [h, degree_zero]⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
⊢ f = 0
have h₁ : ∀ (n : ℤ), Eq (α := R) ((f : (a : ℤ) → R) n : R) ((0 : (a : ℤ) → R) n : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
n : ℤ
⊢ Eq (α := R) ((f : (a : ℤ) → R) n : R) ((0 : (a : ℤ) → R) n : R)
have h₁ : Eq (α := R) ((f : (a : ℤ) → R) n : R) (0 : R)
Tactic: simp only [coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
h : f.degree = ⊥
n : ℤ
⊢ Eq (α := R) ((f : (a : ℤ) → R) n : R) (0 : R)
have h₁ : ∀ (s : ℤ), Eq (α := R) ((f : (a : ℤ) → R) s : R) (0 : R)
Tactic: simp_rw [degree, Finset.max_eq_sup_withBot, Finset.sup_eq_bot_iff, Finsupp.mem_support_iff, Ne,
    WithBot.coe_ne_bot, imp_false, not_not] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree = (↑n : WithBot ℤ)
have rw : Finset.max {n} = (↑n : WithBot ℤ)
Tactic: rw [degree, support_C_mul_T_of_ne_zero a0 n]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Laurent (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq 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 =
    if a = 0 then ⊥ else (↑n : WithBot ℤ)
have pos : ∀ (h : a = 0), (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree = ⊥
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
n : ℤ
a : R
pos :
  ∀ (h : a = 0), (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree = ⊥
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree =
    if a = 0 then ⊥ else (↑n : WithBot ℤ)
have neg : ∀ (h : ¬a = 0),
  (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).degree = (↑n : WithBot ℤ)
Tactic: split_ifs with h