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)))
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 (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)))

Tactic:
fun m => h_C_mul_T_Z 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 (HSub.hSub (α := ℤ) (-(↑i : ℤ)) 1)))

Tactic:
exact fun m => h_C_mul_T_Z 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)))
have :
  ∀
    (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))),
    M p
⊢ M p

Tactic:
have A : ∀ {n : ℤ} {a : R}, M (C a * T n) := by
    intro n a
    refine Int.induction_on n ?_ ?_ ?_
    · simpa only [T_zero, mul_one] using h_C a
    · exact fun m => h_C_mul_T m a
    · exact fun m => h_C_mul_T_Z 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)))
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))
empty :
  M
    (∑ n ∈ ∅,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
insert :
  ∀ (a : ℤ) (s : Finset ℤ),
    a ∉ s →
      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)) →
        M
          (∑ n ∈ Insert.insert a s,
            HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
⊢ ∀ (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))

Tactic:
apply Finset.induction
-- 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))
⊢ M ((C : (a : R) → R[T;T⁻¹]) 0)

Tactic:
h_C 0

Premises used: OfNat.ofNat
-- 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))
h :
  Eq.{u_1 + 1} (α := R[T;T⁻¹])
    (∑ n ∈ ∅,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
    ((C : (a : R) → R[T;T⁻¹]) 0)
⊢ M
    (∑ n ∈ ∅,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))

Tactic:
convert! h_C 0

Premises used: OfNat.ofNat
-- 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))
⊢ Eq.{u_1 + 1} (α := R[T;T⁻¹])
    (∑ n ∈ ∅,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))
    ((C : (a : R) → R[T;T⁻¹]) 0)

Tactic:
simp only [Finset.sum_empty, map_zero]

Premises used: map_zero, Finset.sum_empty
-- 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))
n : ℤ
s : Finset ℤ
ns : n ∉ s
ih :
  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))
insert :
  M
    (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n) +
      ∑ x ∈ s,
        HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) x) : R[T;T⁻¹]) (T x))
⊢ M
    (∑ n ∈ Insert.insert 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))

Tactic:
rw [Finset.sum_insert ns]

Premises used: Finset.sum_insert
-- 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))
n : ℤ
s : Finset ℤ
ns : n ∉ s
ih :
  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))
⊢ M
    (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n) +
      ∑ x ∈ s,
        HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) x) : R[T;T⁻¹]) (T x))

Tactic:
h_add A ih

Premises used: AddMonoidAlgebra
-- 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))
n : ℤ
s : Finset ℤ
ns : n ∉ s
ih :
  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))
⊢ M
    (HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n) +
      ∑ x ∈ s,
        HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) x) : R[T;T⁻¹]) (T x))

Tactic:
exact h_add A ih
-- 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))
⊢ ∀ (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))

Tactic:
have B : ∀ s : Finset ℤ, M (s.sum fun n : ℤ => C (p n) * T n) := by
    apply Finset.induction
    · convert! h_C 0
      simp only [Finset.sum_empty, map_zero]
    · intro n s ns ih
      rw [Finset.sum_insert ns]
      exact h_add A ih
-- 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))
⊢ M
    (∑ n ∈ p.support,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n))

Tactic:
B p.support

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

Tactic:
convert! B p.support

Premises used: Finsupp.support
-- 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))
h :
  ∀ (a : ℤ),
    Eq (α := R) ((p : (a : ℤ) → R) a : R)
      ((∑ n ∈ p.support,
              HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹])
                (T n) :
            (a : ℤ) → R)
          a :
        R)
⊢ p =
    ∑ n ∈ p.support,
      HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹]) (T n)

Tactic:
ext 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)))
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 : ℤ
h :
  Eq (α := R) ((p : (a : ℤ) → R) a : R)
    ((∑ x ∈ p.support, AddMonoidAlgebra.single x ((p : (a : ℤ) → R) x) : (a : ℤ) → R) a : R)
⊢ Eq (α := R) ((p : (a : ℤ) → R) a : R)
    ((∑ n ∈ p.support,
            HMul.hMul (α := R[T;T⁻¹]) (β := R[T;T⁻¹]) ((C : (a : R) → R[T;T⁻¹]) ((p : (a : ℤ) → R) n) : R[T;T⁻¹])
              (T n) :
          (a : ℤ) → R)
        a :
      R)

Tactic:
simp_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
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 : ℤ
h :
  ∀ b ∈ p.support,
    b ≠ a → Eq (α := R) (((AddMonoidAlgebra.single b ((p : (a : ℤ) → R) b) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)
h₁ :
  a ∉ p.support → Eq (α := R) (((AddMonoidAlgebra.single a ((p : (a : ℤ) → R) a) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)
⊢ Eq (α := R) ((p : (a : ℤ) → R) a : R)
    ((∑ x ∈ p.support, AddMonoidAlgebra.single x ((p : (a : ℤ) → R) x) : (a : ℤ) → R) a : R)

Tactic:
rw [Finset.sum_apply', Finset.sum_eq_single a, single_eq_same]

Premises used: Finsupp.single_eq_same, Finset.sum_apply', Finset.sum_eq_single
-- 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 b : ℤ
h :
  b ∈ p.support →
    b ≠ a → Eq (α := R) (((AddMonoidAlgebra.single b ((p : (a : ℤ) → R) b) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)
⊢ b ∈ p.support →
    b ≠ a → Eq (α := R) (((AddMonoidAlgebra.single b ((p : (a : ℤ) → R) b) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)

Tactic:
_
-- 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 b : ℤ
h_1 : b ∈ p.support
hb : b ≠ a
h h₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq (α := R) (((AddMonoidAlgebra.single b ((p : (a : ℤ) → R) b) : R[ℤ]) : (a : ℤ) → R) a : R) (0 : R)

Tactic:
rw [single_eq_of_ne' hb]

Premises used: Finsupp.single_eq_of_ne'