case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
⊢ p = ∑ n in p.support, ↑C (toFun p n) * T n
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M p
convert B p.support
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ↑(∑ n in p.support, ↑C (toFun p n) * T n) a
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
⊢ p = ∑ n in p.support, ↑C (toFun p n) * T n
ext a
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ↑(∑ x in p.support, Finsupp.single x (toFun p x)) a
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ↑(∑ n in p.support, ↑C (toFun p n) * T n) a
simp_rw [← single_eq_C_mul_T]
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ∑ k in p.support, ↑(Finsupp.single k (toFun p k)) a
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ↑(∑ x in p.support, Finsupp.single x (toFun p x)) a
rw [Finset.sum_apply']
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = if a ∈ p.support then toFun p a else 0
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ∑ k in p.support, ↑(Finsupp.single k (toFun p k)) a
simp_rw [Finsupp.single_apply, Finset.sum_ite_eq']
case h.e'_1.h.inl
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
h : a ∈ p.support
⊢ ↑p a = toFun p a

case h.e'_1.h.inr
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
h : ¬a ∈ p.support
⊢ ↑p a = 0
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = if a ∈ p.support then toFun p a else 0
split_ifs with h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ M (↑C a * T n)
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
⊢ ∀ {n : ℤ} {a : R}, M (↑C a * T n)
intro n a
case refine_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ M (↑C a * T 0)

case refine_2
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ ∀ (i : ℕ), M (↑C a * T ↑i) → M (↑C a * T (↑i + 1))

case refine_3
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ ∀ (i : ℕ), M (↑C a * T (-↑i)) → M (↑C a * T (-↑i - 1))
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ M (↑C a * T n)
refine Int.induction_on n ?_ ?_ ?_
no goals
case refine_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ M (↑C a * T 0)
simpa only [T_zero, mul_one] using h_C a
no goals
case refine_2
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ ∀ (i : ℕ), M (↑C a * T ↑i) → M (↑C a * T (↑i + 1))
exact fun m => h_C_mul_T m a
no goals
case refine_3
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ ∀ (i : ℕ), M (↑C a * T (-↑i)) → M (↑C a * T (-↑i - 1))
exact fun m => h_C_mul_T_Z m a
case empty
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ M (∑ n in ∅, ↑C (toFun p n) * T n)

case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∀ ⦃a : ℤ⦄ {s : Finset ℤ}, ¬a ∈ s → M (∑ n in s, ↑C (toFun p n) * T n) → M (∑ n in insert a s, ↑C (toFun p n) * T n)
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
apply Finset.induction
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∑ n in ∅, ↑C (toFun p n) * T n = ↑C 0
case empty
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ M (∑ n in ∅, ↑C (toFun p n) * T n)
convert h_C 0
no goals
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∑ n in ∅, ↑C (toFun p n) * T n = ↑C 0
simp only [Finset.sum_empty, _root_.map_zero]
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
n : ℤ
s : Finset ℤ
ns : ¬n ∈ s
ih : M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M (∑ n in insert n s, ↑C (toFun p n) * T n)
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∀ ⦃a : ℤ⦄ {s : Finset ℤ}, ¬a ∈ s → M (∑ n in s, ↑C (toFun p n) * T n) → M (∑ n in insert a s, ↑C (toFun p n) * T n)
intro n s ns ih
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
n : ℤ
s : Finset ℤ
ns : ¬n ∈ s
ih : M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M (↑C (toFun p n) * T n + ∑ x in s, ↑C (toFun p x) * T x)
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
n : ℤ
s : Finset ℤ
ns : ¬n ∈ s
ih : M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M (∑ n in insert n s, ↑C (toFun p n) * T n)
rw [Finset.sum_insert ns]
no goals
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
n : ℤ
s : Finset ℤ
ns : ¬n ∈ s
ih : M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M (↑C (toFun p n) * T n + ∑ x in s, ↑C (toFun p x) * T x)
exact h_add A ih
no goals
case h.e'_1.h.inl
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
h : a ∈ p.support
⊢ ↑p a = toFun p a
rfl
no goals
case h.e'_1.h.inr
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
h : ¬a ∈ p.support
⊢ ↑p a = 0
exact Finsupp.not_mem_support_iff.mp h