awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
pos :
  ∀ (a0 : a = 0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
      M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
neg :
  ∀ (a0 : ¬a = 0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
      M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))

Tactic:
by_cases a0 : a = 0
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : a = 0
rw : ((C : (a : R) → R[X]) 0 * HPow.hPow (α := R[X]) X (n + 1)).natDegree = 0
rw₁ : (0 * HPow.hPow (α := R[X]) X (n + 1)).natDegree = 0
rw₂ : natDegree.{u} (R := R) 0 = 0
rw₃ rw₄ : Eq (α := ℕ) 0 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0

Tactic:
rw [a0, C_0, zero_mul, natDegree_zero]

Premises used: Polynomial.C_0, MulZeroClass.zero_mul, Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : a = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))

Tactic:
exact Or.inl (by rw [a0, C_0, zero_mul, natDegree_zero])

Premises used: Or.inl
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : ¬a = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))

Tactic:
Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : ¬a = 0
neg : M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))

Tactic:
refine Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : ¬a = 0
neg : M ((monomial (n + 1) : (a : R) → R[X]) a)
⊢ M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))

Tactic:
rw [C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : ¬a = 0
⊢ M ((monomial (n + 1) : (a : R) → R[X]) a)

Tactic:
h_monomial a0 n.succ_ne_zero

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
M : R[X] → Prop
f : R[X]
f0 : f.natDegree ≠ 0
h_C_add : ∀ {a : R} {p : R[X]}, M p → M (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)
h_add : ∀ {p q : R[X]}, M p → M q → M (p + q)
h_monomial : ∀ {n : ℕ} {a : R}, a ≠ 0 → n ≠ 0 → M ((monomial n : (a : R) → R[X]) a)
n : ℕ
a : R
h :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).natDegree = 0 ∨
    M (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
a0 : ¬a = 0
⊢ M ((monomial (n + 1) : (a : R) → R[X]) a)

Tactic:
exact h_monomial a0 n.succ_ne_zero

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
p q : R[T;T⁻¹]
h : ∀ (a : ℤ), Eq (α := R) ((p : (a : ℤ) → R) a : R) ((q : (a : ℤ) → R) a : R)
⊢ p = q

Tactic:
Finsupp.ext h

Premises used: Finsupp.ext, AddMonoidAlgebra
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
p : R[X]
⊢ Eq (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) p : R[T;T⁻¹])
    (AddMonoidAlgebra.mapDomain Nat.cast p.toFinsupp : R[ℤ])

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := (a : R[X]) → R[T;T⁻¹]) (⇑toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) (⇑toLaurent : (a : R[X]) → R[T;T⁻¹])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : CommSemiring R
f : R[X]
⊢ Eq (α := R[T;T⁻¹]) ((toLaurentAlg : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹])
    ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[ℤ]) (AddMonoidAlgebra.single 0 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq.{u_4 + 1} (α := A[T;T⁻¹]) ((algebraMap R A[T;T⁻¹] : (a : R) → A[T;T⁻¹]) r : A[T;T⁻¹])
    ((C : (a : A) → A[T;T⁻¹]) ((algebraMap R A : (a : R) → A) r) : A[T;T⁻¹])

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_3
inst : CommSemiring R
r : R
⊢ Eq (α := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) ((algebraMap R R[T;T⁻¹] : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ Eq (α := R[T;T⁻¹]) (AddMonoidAlgebra.single 0 r) ((C : (a : R) → R[T;T⁻¹]) r)

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
t : R
n : ℤ
rw : (if 0 = n then t else 0) = if n = 0 then t else 0
⊢ (((C : (a : R) → R[T;T⁻¹]) t : R[T;T⁻¹]) : (a : ℤ) → R) n = if n = 0 then t else 0

Tactic:
rw [← single_eq_C, Finsupp.single_apply]

Premises used: LaurentPolynomial.single_eq_C, Finsupp.single_apply
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
t : R
n : ℤ
⊢ (if 0 = n then t else 0) = if n = 0 then t else 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
m n : ℤ
⊢ Eq.{u_1 + 1} (α := R) ((T n : (a : ℤ) → R) m : R) (if n = m then 1 else 0 : R)

Tactic:
Finsupp.single_apply

Premises used: Finsupp.single_apply
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T 0) 1

Tactic:
rfl

Premises used: LaurentPolynomial.T, rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
m n : ℤ
⊢ T (m + n) = HMul.hMul (α := R[T;T⁻¹]) (T m) (T n)

Tactic:
simp [T, single_mul_single]

Premises used: LaurentPolynomial.T, AddMonoidAlgebra.single_mul_single
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
m n : ℤ
rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (m - n)) (T (m + -n))
rw₁ rw₂ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (m + -n)) (T (m + -n))
⊢ T (m - n) = HMul.hMul (α := R[T;T⁻¹]) (T m) (T (-n))

Tactic:
rw [← T_add, sub_eq_add_neg]

Premises used: sub_eq_add_neg, LaurentPolynomial.T_add
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
m : ℤ
n : ℕ
rw : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = T ((↑n : ℤ) * m)
rw₁ : HPow.hPow (α := R[T;T⁻¹]) (AddMonoidAlgebra.single m 1) n = AddMonoidAlgebra.single ((↑n : ℤ) * m) 1
rw₂ :
  Eq (α := R[T;T⁻¹]) (AddMonoidAlgebra.single (n • m) (HPow.hPow (α := R) 1 n))
    (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1)
rw₃ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (AddMonoidAlgebra.single (n • m) 1) (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1)
rw₄ rw₅ :
  Eq.{u_1 + 1} (α := R[T;T⁻¹]) (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1) (AddMonoidAlgebra.single ((↑n : ℤ) * m) 1)
⊢ HPow.hPow (α := R[T;T⁻¹]) (T m) n = T ((↑n : ℤ) * m)

Tactic:
rw [T, T, single_pow, one_pow, nsmul_eq_mul]

Premises used: LaurentPolynomial.T, one_pow, nsmul_eq_mul, AddMonoidAlgebra.single_pow
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
f : R[T;T⁻¹]
m n : ℤ
⊢ f * T m * T n = f * T (m + n)

Tactic:
simp [← T_add, mul_assoc]

Premises used: mul_assoc, LaurentPolynomial.T_add
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℤ
⊢ AddMonoidAlgebra.single n r = HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T n)

Tactic:
simp [C, T, single_mul_single]

Premises used: LaurentPolynomial.T, AddMonoidAlgebra.single_mul_single, LaurentPolynomial.C
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : R
⊢ (toLaurent : (a : R[X]) → R[T;T⁻¹]) ((monomial n : (a : R) → R[X]) r) =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (↑n : ℤ))

Tactic:
simp [toLaurent]

Premises used: Polynomial.toLaurent
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ (toLaurent : (a : R[X]) → R[T;T⁻¹]) ((monomial 0 : (a : R) → R[X]) r) =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (↑0 : ℤ))

Tactic:
Polynomial.toLaurent_C_mul_T 0 r

Premises used: Polynomial.toLaurent_C_mul_T, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
h :
  (C : (a : R) → R[T;T⁻¹]) r =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (↑0 : ℤ))
⊢ Eq (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) ((Polynomial.C : (a : R) → R[X]) r) : R[T;T⁻¹])
    ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])

Tactic:
convert! Polynomial.toLaurent_C_mul_T 0 r

Premises used: Polynomial.toLaurent_C_mul_T, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ (C : (a : R) → R[T;T⁻¹]) r =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (↑0 : ℤ))

Tactic:
simp only [Int.ofNat_zero, T_zero, mul_one]

Premises used: LaurentPolynomial.T_zero, Int.ofNat_zero, mul_one
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R → R[T;T⁻¹])
    (Function.comp (β := R[X]) (⇑toLaurent : (a : R[X]) → R[T;T⁻¹]) (⇑Polynomial.C : (a : R) → R[X]))
    (⇑C : (a : R) → R[T;T⁻¹])

Tactic:
funext Polynomial.toLaurent_C

Premises used: funext, Polynomial.toLaurent_C
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X]) X ((monomial 1 : (a : R) → R[X]) 1)

Tactic:
simp [← C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X]) X ((monomial 1 : (a : R) → R[X]) 1)

Tactic:
have : (Polynomial.X : R[X]) = monomial 1 1 := by simp [← C_mul_X_pow_eq_monomial]
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
this : Eq.{u_1 + 1} (α := R[X]) X ((monomial 1 : (a : R) → R[X]) 1)
⊢ Eq.{u_1 + 1} (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) X : R[T;T⁻¹]) (T 1 : R[T;T⁻¹])

Tactic:
simp [this, Polynomial.toLaurent_C_mul_T]

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

Tactic:
map_one Polynomial.toLaurent

Premises used: Polynomial.toLaurent, map_one
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
r : R
f : R[X]
⊢ (toLaurent : (a : R[X]) → R[T;T⁻¹]) (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) f) =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹])
      ((toLaurent : (a : R[X]) → R[T;T⁻¹]) f : R[T;T⁻¹])

Tactic:
simp only [map_mul, Polynomial.toLaurent_C]

Premises used: map_mul, Polynomial.toLaurent_C
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Eq (α := R[T;T⁻¹]) ((toLaurent : (a : R[X]) → R[T;T⁻¹]) (HPow.hPow (α := R[X]) X n) : R[T;T⁻¹])
    (T (↑n : ℤ) : R[T;T⁻¹])

Tactic:
simp only [map_pow, Polynomial.toLaurent_X, T_pow, mul_one]

Premises used: LaurentPolynomial.T_pow, map_pow, mul_one, Polynomial.toLaurent_X
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : R
⊢ (toLaurent : (a : R[X]) → R[T;T⁻¹])
      (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) r : R[T;T⁻¹]) (T (↑n : ℤ))

Tactic:
simp only [map_mul, Polynomial.toLaurent_C, Polynomial.toLaurent_X_pow]

Premises used: Polynomial.toLaurent_X_pow, map_mul, Polynomial.toLaurent_C
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
n : ℤ
rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (-n + n)) 1
rw₁ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T 0) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) 1 1
⊢ HMul.hMul (α := R[T;T⁻¹]) (T (-n)) (T n) = 1

Tactic:
rw [← T_add, neg_add_cancel, T_zero]

Premises used: LaurentPolynomial.T_zero, neg_add_cancel, LaurentPolynomial.T_add
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
n : ℤ
rw : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T (n + -n)) 1
rw₁ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) (T 0) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[T;T⁻¹]) 1 1
⊢ HMul.hMul (α := R[T;T⁻¹]) (T n) (T (-n)) = 1

Tactic:
rw [← T_add, add_neg_cancel, T_zero]

Premises used: add_neg_cancel, LaurentPolynomial.T_zero, LaurentPolynomial.T_add
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
⊢ Eq.{u_1 + 1} (α := R[T;T⁻¹]) (@Invertible.invOf _ AddMonoidAlgebra.instMul zero (T n) _) (T (-n))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Laurent
Goal:
R : Type u_1
inst : Semiring R
n : ℤ
⊢ IsUnit.{u_1} (M := R[T;T⁻¹]) (T n)

Tactic:
isUnit_of_invertible _

Premises used: isUnit_of_invertible
-- 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)))
n : ℤ
a : R
⊢ M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))

Tactic:
Int.induction_on n ?_ ?_ ?_

Premises used: Int.induction_on
-- 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)))
n : ℤ
a : R
refine_1 : M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0))
refine_2 :
  ∀ (i : ℕ),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑i : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)))
refine_3 :
  ∀ (i : ℕ),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (-(↑i : ℤ)))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)))
⊢ M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T n))

Tactic:
refine Int.induction_on n ?_ ?_ ?_
-- 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)))
n : ℤ
a : R
⊢ M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T 0))

Tactic:
simpa only [T_zero, mul_one] using h_C a

Premises used: LaurentPolynomial.T_zero, mul_one
-- 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)))
n : ℤ
a : R
⊢ ∀ (i : ℕ),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑i : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)))

Tactic:
fun m => h_C_mul_T m a
-- 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)))
n : ℤ
a : R
⊢ ∀ (i : ℕ),
    M (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹]) (T (↑i : ℤ))) →
      M
        (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) a : R[T;T⁻¹])
          (T (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1)))

Tactic:
exact fun m => h_C_mul_T m a