awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M ((C : (a : R) → R[T;T⁻¹]) a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
h_C_mul_T_Z :
  ∀ (n : ℕ) (a : R),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
A : ∀ {n : ℤ} {a : R}, M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
B :
  ∀ (s : Finset ℤ),
    M
      (∑ n ∈ s,
        HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
a : ℤ
ha : a ∉ p.support
h : Eq (α := R) ((p : (a : ℤ) → R) a : R) (0 : R)
h₁ h₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) (((AddMonoidAlgebra.single a ((p : (a : ℤ) → R) a) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)

Tactic:
rw [single_eq_same, notMem_support_iff.mp ha]

Premises used: Finsupp.single_eq_same, Finsupp.notMem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
⊢ motive p

Tactic:
p.induction_on (fun a => ?_) (fun {p q} => add p q) ?_ ?_

Premises used: LaurentPolynomial.induction_on
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
refine_1 : ∀ (a : R), motive ((C : (a : R) → R[T;T⁻¹]) a)
refine_2 :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      motive
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))
refine_3 :
  ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      motive
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))
⊢ motive p

Tactic:
refine p.induction_on (fun a => ?_) (fun {p q} => add p q) ?_ ?_
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
⊢ ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      motive
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))

Tactic:
fun n f _ => C_mul_T _ f

Premises used: Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
⊢ ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      motive
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))

Tactic:
exact fun n f _ => C_mul_T _ f
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
⊢ ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑n : ℤ))) →
      motive
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)))

Tactic:
try exact fun n f _ => C_mul_T _ f
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
⊢ ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      motive
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))

Tactic:
fun n f _ => C_mul_T _ f

Premises used: HSub.hSub, Nat.cast, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
⊢ ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      motive
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))

Tactic:
exact fun n f _ => C_mul_T _ f
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
⊢ ∀ (n : ℕ) (a : R),
    motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑n : ℤ)))) →
      motive
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)))

Tactic:
try exact fun n f _ => C_mul_T _ f
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
a : R
⊢ motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0))

Tactic:
C_mul_T 0 a

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
a : R
h : (C : (a : R) → R[T;T⁻¹]) a = HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0)
⊢ motive ((C : (a : R) → R[T;T⁻¹]) a)

Tactic:
convert! C_mul_T 0 a

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
a : R
⊢ (C : (a : R) → R[T;T⁻¹]) a = HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0)

Tactic:
(mul_one _).symm

Premises used: LaurentPolynomial.T, mul_one, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
motive : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
add : ∀ (p q : R[T;T⁻¹]), motive p → motive q → motive (p + q)
C_mul_T :
  ∀ (n : ℤ) (a : R), motive (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))
a : R
⊢ (C : (a : R) → R[T;T⁻¹]) a = HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0)

Tactic:
exact (mul_one _).symm

Premises used: mul_one, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
rw :
  Eq (α := R[T;T⁻¹]) (AddMonoidAlgebra.single (n + (0 + m)) (1 * (a * 1)))
    (AddMonoidAlgebra.single (0 + m + n) (a * 1 * 1))
⊢ T n * HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T m) =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T m) * T n

Tactic:
rw [T, T, ← single_eq_C, single_mul_single, single_mul_single, single_mul_single]

Premises used: LaurentPolynomial.T, LaurentPolynomial.single_eq_C, AddMonoidAlgebra.single_mul_single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ Eq (α := R[T;T⁻¹]) (AddMonoidAlgebra.single (n + (0 + m)) (1 * (a * 1)))
    (AddMonoidAlgebra.single (0 + m + n) (a * 1 * 1))

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
f : R[T;T⁻¹]
⊢ T n * f = f * T n

Tactic:
(commute_T n f).eq

Premises used: LaurentPolynomial.commute_T, Commute.eq
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
p q : R[T;T⁻¹]
hp : r • p = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p
hq : r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q
add : r • p + r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
add₁ :
  r • p + r • q =
    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
add₂ :
  HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p + r • q =
    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
add₃ 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 =
    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
⊢ r • (p + q) = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)

Tactic:
rw [smul_add, mul_add, hp, hq]

Premises used: mul_add, smul_add
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℤ
s : R
C_mul_T : Eq (α := R[T;T⁻¹]) (Finsupp.single 0 (r * s)) ((C : (a : R) → R[T;T⁻¹]) (r * s))
⊢ r • HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n) =
    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))

Tactic:
rw [← mul_assoc, ← smul_mul_assoc, mul_left_inj_of_invertible, ← map_mul, ← single_eq_C,
      Finsupp.smul_single']

Premises used: mul_assoc, mul_left_inj_of_invertible, smul_mul_assoc, Finsupp.smul_single', LaurentPolynomial.single_eq_C, map_mul
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℤ
s : R
⊢ Eq (α := R[T;T⁻¹]) (Finsupp.single 0 (r * s)) ((C : (a : R) → R[T;T⁻¹]) (r * s))

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[T;T⁻¹]
add :
  ∀ (p q : R[T;T⁻¹]) (hp : r • p = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) p)
    (hq : r • q = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) q),
    r • (p + q) = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (p + q)
C_mul_T :
  ∀ (n : ℤ) (s : R),
    r • HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) s : R[T;T⁻¹]) (T n) =
      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))
⊢ r • f = HMul.hMul (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) f

Tactic:
induction f using LaurentPolynomial.induction_on' with
  | add _ _ hp hq =>
    rw [smul_add, mul_add, hp, hq]
  | C_mul_T n s =>
    rw [← mul_assoc, ← smul_mul_assoc, mul_left_inj_of_invertible, ← map_mul, ← single_eq_C,
      Finsupp.smul_single']
    rfl

Premises used: mul_assoc, mul_left_inj_of_invertible, smul_mul_assoc, Finsupp.smul_single', LaurentPolynomial.single_eq_C, map_mul, mul_add, smul_add
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
a :
  Eq (α := R[ℕ])
    ((toFinsuppIso R : (a : R[X]) → R[ℕ])
        ((trunc : (a : R[T;T⁻¹]) → R[X])
          (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T n))) :
      R[ℕ])
    ((toFinsuppIso R : (a : R[X]) → R[ℕ]) (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0) : R[ℕ])
⊢ Eq (α := R[X])
    ((trunc : (a : R[T;T⁻¹]) → R[X])
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T n)) :
      R[X])
    (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0 : R[X])

Tactic:
apply (toFinsuppIso R).injective

Premises used: RingEquiv.injective, Polynomial.toFinsuppIso
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
a :
  Eq (α := R[ℕ])
    (((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ (↑x : ℤ)) ⋯ : (ℤ →₀ R) →+ ℕ →₀ R) : (a : R[T;T⁻¹]) → R[ℕ])
        (AddMonoidAlgebra.single n r) :
      R[ℕ])
    (toFinsupp (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0) : R[ℕ])
⊢ Eq (α := R[ℕ])
    ((toFinsuppIso R : (a : R[X]) → R[ℕ])
        ((trunc : (a : R[T;T⁻¹]) → R[X])
          (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T n))) :
      R[ℕ])
    ((toFinsuppIso R : (a : R[X]) → R[ℕ]) (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0) : R[ℕ])

Tactic:
simp only [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply,
    RingHom.toAddMonoidHom_eq_coe, RingEquiv.toRingHom_eq_coe, Int.ofNat_eq_natCast,
    AddMonoidHom.coe_coe, RingHom.coe_coe, RingEquiv.apply_symm_apply, toFinsuppIso_apply]

Premises used: RingEquiv.apply_symm_apply, RingHom.toAddMonoidHom_eq_coe, RingHom.coe_coe, AddMonoidHom.coe_coe, Int.ofNat_eq_natCast, LaurentPolynomial.trunc, LaurentPolynomial.single_eq_C_mul_T, Polynomial.toFinsuppIso_apply, AddMonoidHom.coe_comp, RingEquiv.toRingHom_eq_coe, Function.comp_apply
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
a :
  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))
⊢ Eq (α := R[ℕ])
    (((comapDomain.addMonoidHom (f := fun (x : ℕ) ↦ (↑x : ℤ)) ⋯ : (ℤ →₀ R) →+ ℕ →₀ R) : (a : R[T;T⁻¹]) → R[ℕ])
        (AddMonoidAlgebra.single n r) :
      R[ℕ])
    (toFinsupp (if 0 ≤ n then (monomial n.toNat : (a : R) → R[X]) r else 0) : R[ℕ])

Tactic:
erw [comapDomain.addMonoidHom_apply Int.ofNat_injective]

Premises used: Int.ofNat_injective, Finsupp.comapDomain.addMonoidHom_apply
-- Module: Mathlib.Algebra.Polynomial.Laurent
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))
neg : ∀ (n0 : ¬0 ≤ n), Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯) (toFinsupp 0)
⊢ 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))

Tactic:
split_ifs with n0
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : 0 ≤ n
⊢ 0 ≤ n

Tactic:
n0
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : 0 ≤ n
pos :
  ∀ (n : ℕ),
    Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single (↑n : ℤ) r) ⋯)
      (AddMonoidAlgebra.single (Int.toNat (↑n : ℤ)) r)
⊢ Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯) (AddMonoidAlgebra.single n.toNat r)

Tactic:
lift n to ℕ using n0
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
⊢ Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single (↑n : ℤ) r) ⋯)
    (AddMonoidAlgebra.single (Int.toNat (↑n : ℤ)) r)

Tactic:
apply comapDomain_single

Premises used: Finsupp.comapDomain_single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
neg : Eq (α := R[X]) { toFinsupp := Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯ } 0
⊢ Eq (α := R[ℕ]) (Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯) (toFinsupp 0)

Tactic:
rw [toFinsupp_inj]

Premises used: Polynomial.toFinsupp_inj
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
neg :
  ∀ (a : ℕ),
    Polynomial.coeff { toFinsupp := Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯ : R[X] } a =
      Polynomial.coeff 0 a
⊢ Eq (α := R[X]) { toFinsupp := Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯ } 0

Tactic:
ext a
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
a : ℕ
⊢ (↑a : ℤ) ≠ n

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
a : ℕ
⊢ (↑a : ℤ) ≠ n

Tactic:
have : a ≠ n := by lia
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
r : R
n0 : ¬0 ≤ n
a : ℕ
this : (↑a : ℤ) ≠ n
⊢ Polynomial.coeff { toFinsupp := Finsupp.comapDomain Int.ofNat (AddMonoidAlgebra.single n r) ⋯ : R[X] } a =
    Polynomial.coeff 0 a

Tactic:
simp only [coeff_ofFinsupp, comapDomain_apply, Int.ofNat_eq_natCast, Polynomial.coeff_zero,
      single_eq_of_ne this]

Premises used: Polynomial.coeff_ofFinsupp, Finsupp.single_eq_of_ne, Int.ofNat_eq_natCast, Finsupp.comapDomain_apply, Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
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⁻¹])

Tactic:
fun f => f.induction_on' ?_ ?_

Premises used: Function.LeftInverse, Polynomial.induction_on'
-- Module: Mathlib.Algebra.Polynomial.Laurent
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
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])
⊢ 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⁻¹])

Tactic:
refine fun f => f.induction_on' ?_ ?_
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f_1 f g : R[X]
hf : (trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f) = f
hg : (trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) g) = g
⊢ (trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (f + g)) = f + g

Tactic:
simp only [hf, hg, map_add]

Premises used: map_add
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
r : R
⊢ Eq (α := R[X])
    ((trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) ((monomial n : (a : R) → R[X]) r)) : R[X])
    ((monomial n : (a : R) → R[X]) r : R[X])

Tactic:
simp only [Polynomial.toLaurent_C_mul_T, trunc_C_mul_T, Int.natCast_nonneg, Int.toNat_natCast,
      if_true]

Premises used: Int.toNat_natCast, if_true, Polynomial.toLaurent_C_mul_T, LaurentPolynomial.trunc_C_mul_T, Int.natCast_nonneg
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ (trunc : (a : R[T;T⁻¹]) → R[X]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f) = f

Tactic:
leftInverse_trunc_toLaurent _

Premises used: LaurentPolynomial.leftInverse_trunc_toLaurent
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
⊢ Injective.{u_1 + 1, u_1 + 1} (α := R[X]) (β := R[T;T⁻¹]) (⇑toLaurent : (a : R[X]) → R[T;T⁻¹])

Tactic:
leftInverse_trunc_toLaurent.injective

Premises used: Function.LeftInverse.injective, LaurentPolynomial.leftInverse_trunc_toLaurent
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
⊢ Eq (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹])
      ((toLaurent : (a : R[X]) → R[T;T⁻¹]) g : R[T;T⁻¹]) ↔
    f = g

Tactic:
⟨fun h => Polynomial.toLaurent_injective h, congr_arg _⟩

Premises used: Polynomial.toLaurent_injective, congr_arg, Iff.intro
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ Ne (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (0 : R[T;T⁻¹]) ↔ f ≠ 0

Tactic:
map_ne_zero_iff _ Polynomial.toLaurent_injective

Premises used: Polynomial.toLaurent_injective, map_ne_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ Eq (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹]) (0 : R[T;T⁻¹]) ↔ f = 0

Tactic:
map_eq_zero_iff _ Polynomial.toLaurent_injective

Premises used: Polynomial.toLaurent_injective, map_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ)

Tactic:
f.induction_on' ?_ fun n a => ?_

Premises used: LaurentPolynomial.induction_on'
-- Module: Mathlib.Algebra.Polynomial.Laurent
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 : ℤ)
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 : ℤ)
⊢ ∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = f * T (↑n : ℤ)

Tactic:
refine f.induction_on' ?_ fun n a => ?_
-- 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 : ℤ)
⊢ ∃ (n : ℕ) (f' : R[X]), (toLaurent : (a : R[X]) → R[T;T⁻¹]) f' = (f + g) * T (↑n : ℤ)

Tactic:
⟨m + n, fn * X ^ n + gn * X ^ m, ?_⟩

Premises used: HMul.hMul, HPow.hPow, HAdd.hAdd, Exists.intro, Polynomial.X