awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ)
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) : ℤ)
⊢ ∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = (f + g) * T (↑n : ℤ)

Tactic:
refine ⟨m + n, fn * X ^ n + gn * X ^ m, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ)
⊢ (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:
simp only [hf, hg, add_mul, add_comm (n : ℤ), map_add, map_mul, Polynomial.toLaurent_X_pow,
      mul_T_assoc, Int.natCast_add]

Premises used: add_mul, LaurentPolynomial.mul_T_assoc, Int.natCast_add, map_add, Polynomial.toLaurent_X_pow, Nat.cast, add_comm, map_mul
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ)
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 : ℤ)
⊢ ∃ (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:
rcases n with n | n
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℕ
⊢ (toLaurent : (a : R[X]) → R[T;T⁻¹])
      (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (Int.ofNat n)) * T (↑0 : ℤ)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Laurent
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.ofNat n)) * T (↑n_1 : ℤ)

Tactic:
exact ⟨0, Polynomial.C a * X ^ n, by simp⟩
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ)

Tactic:
⟨n + 1, Polynomial.C a, ?_⟩

Premises used: Polynomial.C, HAdd.hAdd, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℕ
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) : ℤ)
⊢ ∃ (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:
refine ⟨n + 1, Polynomial.C a, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℕ
⊢ (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:
simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.natCast_succ, mul_T_assoc,
        neg_add_cancel, T_zero, mul_one]

Premises used: LaurentPolynomial.mul_T_assoc, LaurentPolynomial.T_zero, Int.natCast_succ, neg_add_cancel, Int.negSucc_eq, mul_one, Polynomial.toLaurent_C
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ))))
rcases : ∀ (n : ℕ) (f' : R[X]) (hf : (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = f * T (↑n : ℤ)), motive f
⊢ motive f

Tactic:
rcases f.exists_T_pow with ⟨n, f', hf⟩

Premises used: LaurentPolynomial.exists_T_pow
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ)
rw :
  motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f' : R[T;T⁻¹]) (T (-(↑n : ℤ))))
⊢ motive f

Tactic:
rw [← mul_one f, ← T_zero, ← Nat.cast_zero, ← Nat.sub_self n, Nat.cast_sub rfl.le, T_sub,
    ← mul_assoc, ← hf]

Premises used: LaurentPolynomial.T_sub, Nat.cast_sub, mul_assoc, LaurentPolynomial.T_zero, Eq.le, Nat.sub_self, Nat.cast_zero, mul_one, rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f' : R[T;T⁻¹]) (T (-(↑n : ℤ))))

Tactic:
mul_T ..
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f' : R[T;T⁻¹]) (T (-(↑n : ℤ))))

Tactic:
exact mul_T ..
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
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 : ℤ))))
⊢ Q f

Tactic:
induction f using LaurentPolynomial.induction_on_mul_T with | _ f n
-- Module: Mathlib.Algebra.Polynomial.Laurent
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]
⊢ Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑0 : ℤ))))

Tactic:
simpa only [Nat.cast_zero, neg_zero, T_zero, mul_one] using Qf _

Premises used: LaurentPolynomial.T_zero, Nat.cast_zero, mul_one, neg_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
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) : ℤ))))

Tactic:
QT _ _
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ))))
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)
⊢ Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑(n + 1) : ℤ))))

Tactic:
convert! QT _ _
-- Module: Mathlib.Algebra.Polynomial.Laurent
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) : ℤ))) *
      T 1)

Tactic:
simpa using hn
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ))))
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) : ℤ))))
⊢ Q (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (T (-(↑n : ℤ))))

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

Premises used: LaurentPolynomial.T_zero, AddMonoidAlgebra.zero, Nat.cast_zero, mul_one, neg_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℤ
rw : Finsupp.support (AddMonoidAlgebra.single n a) ⊆ {n}
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).support ⊆ {n}

Tactic:
rw [← single_eq_C_mul_T]

Premises used: LaurentPolynomial.single_eq_C_mul_T
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℤ
⊢ Finsupp.support (AddMonoidAlgebra.single n a) ⊆ {n}

Tactic:
support_single_subset

Premises used: Set.Mem, setOf, Finsupp.support_single_subset
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
n : ℤ
⊢ Finsupp.support (AddMonoidAlgebra.single n a) ⊆ {n}

Tactic:
exact support_single_subset

Premises used: Finsupp.support_single_subset
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
rw : Finsupp.support (AddMonoidAlgebra.single n a) = {n}
⊢ (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n)).support = {n}

Tactic:
rw [← single_eq_C_mul_T]

Premises used: LaurentPolynomial.single_eq_C_mul_T
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ Finsupp.support (AddMonoidAlgebra.single n a) = {n}

Tactic:
support_single _ a0

Premises used: Finsupp.support_single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ Finsupp.support (AddMonoidAlgebra.single n a) = {n}

Tactic:
exact support_single _ a0

Premises used: Finsupp.support_single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
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)
⊢ Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding f.support)

Tactic:
generalize hd : f.support = s

Premises used: Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
s : Finset ℕ
hd : f.support = s
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)
⊢ 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
-- Module: Mathlib.Algebra.Polynomial.Laurent
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)

Tactic:
Finset.induction_on s ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 ∅)
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))
⊢ ∀ (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:
refine Finset.induction_on s ?_ ?_
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.support = ∅
refine_1 : f = 0
⊢ Eq (α := Finset ℤ) (Finsupp.support.{0, u_1} (M := R) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f))
    (Finset.map Nat.castEmbedding ∅)

Tactic:
rw [Finset.map_empty, Finsupp.support_eq_empty, toLaurent_eq_zero]

Premises used: Polynomial.toLaurent_eq_zero, Finsupp.support_eq_empty, Finset.map_empty
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.support = ∅
⊢ f = 0

Tactic:
Polynomial.support_eq_empty.mp hf

Premises used: Iff.mp, Polynomial.support_eq_empty
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
hf : f.support = ∅
⊢ f = 0

Tactic:
exact Polynomial.support_eq_empty.mp hf

Premises used: Iff.mp, Polynomial.support_eq_empty
-- Module: Mathlib.Algebra.Polynomial.Laurent
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)

Tactic:
hf (f.erase a) ?_

Premises used: Polynomial.erase
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
refine : (Polynomial.erase a f).support = 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)

Tactic:
refine hf (f.erase a) ?_

Premises used: Polynomial.erase
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
⊢ (Polynomial.erase a f).support = s

Tactic:
simp only [fs, Finset.erase_eq_of_notMem as, Polynomial.support_erase,
        Finset.erase_insert_eq_erase]

Premises used: Finset.erase_insert_eq_erase, Finset.erase_eq_of_notMem, Polynomial.support_erase
-- Module: Mathlib.Algebra.Polynomial.Laurent
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)

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]
-- Module: Mathlib.Algebra.Polynomial.Laurent
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))
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)))
⊢ 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:
rw [← monomial_add_erase f a, Finset.map_insert, ← this, map_add, Polynomial.toLaurent_C_mul_T,
      support_add_eq, Finset.insert_eq]

Premises used: Finset.insert_eq, Polynomial.toLaurent_C_mul_T, Finsupp.support_add_eq, map_add, Finset.map_insert, Polynomial.monomial_add_erase
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 =
    singleton (α := ℤ) ((Nat.castEmbedding : (a : ℕ) → ℤ) a : ℤ)
⊢ (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:
congr
-- Module: Mathlib.Algebra.Polynomial.Laurent
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)
⊢ a ∈ f.support

Tactic:
simp [fs]
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 =
    singleton (α := ℤ) ((Nat.castEmbedding : (a : ℕ) → ℤ) a : ℤ)

Tactic:
exact support_C_mul_T_of_ne_zero (Polynomial.mem_support_iff.mp (by simp [fs])) _

Premises used: Polynomial.mem_support_iff, Iff.mp, LaurentPolynomial.support_C_mul_T_of_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 :
  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)
⊢ 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 [this]
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 (α := Finset ℤ) {(↑a : ℤ)} (Finset.map Nat.castEmbedding s)

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
    (Finset.map Nat.castEmbedding s)

Tactic:
exact Disjoint.mono_left (support_C_mul_T _ _) (by simpa)

Premises used: Disjoint.mono_left
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
⊢ degree.{u_1} (R := R) 0 = ⊥

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, Finset.max, Finset.sup, LaurentPolynomial.degree, List.foldr, rfl, Multiset.fold
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
h : f = 0
rw : degree.{u_1} (R := R) 0 = ⊥
rw₁ rw₂ : Eq (α := WithBot ℤ) ⊥ ⊥
⊢ f.degree = ⊥

Tactic:
rw [h, degree_zero]

Premises used: LaurentPolynomial.degree_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
refine : ∀ (h : f.degree = ⊥), f = 0
⊢ f.degree = ⊥ ↔ f = 0

Tactic:
refine ⟨fun h => ?_, fun h => by rw [h, degree_zero]⟩