-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem _root_.Polynomial.coeff_prod_mem_ideal_pow_tsub {ι : Type*} (s : Finset ι) (f : ι → R[X])
    (I : Ideal R) (n : ι → ℕ) (h : ∀ i ∈ s, ∀ (k), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ) :
    (s.prod f).coeff k ∈ I ^ (s.sum n - k)

Proof state:
case insert.h.mk.a
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a - i + (∑ x ∈ s, n x - j))

Tactic:
rw [pow_add]

Result:
case insert.h.mk.a
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a - i) * I ^ (∑ x ∈ s, n x - j)

Proof state:
case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ((insert a s).prod f).coeff k ∈ I ^ ((insert a s).sum n - k)

Tactic:
rw [sum_insert ha, prod_insert ha, coeff_mul]

Result:
case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ∑ x ∈ antidiagonal k, (f a).coeff x.1 * (∏ x ∈ s, f x).coeff x.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Proof state:
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (s.prod f).coeff k ∈ I ^ (s.sum n - k)

Tactic:
induction' s using Finset.induction with a s ha hs generalizing k

Result:
case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (∅.prod f).coeff k ∈ I ^ (∅.sum n - k)

case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ((insert a s).prod f).coeff k ∈ I ^ ((insert a s).sum n - k)

Proof state:
case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (∅.prod f).coeff k ∈ I ^ (∅.sum n - k)

Tactic:
rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]

Result:
case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (if k = 0 then 1 else 0) ∈ ⊤

Proof state:
case insert.h.mk.a
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a - i) * I ^ (∑ x ∈ s, n x - j)

Tactic:
exact
  Ideal.mul_mem_mul (h _ (Finset.mem_insert.mpr <| Or.inl rfl) _)
    (hs (fun i hi k => h _ (Finset.mem_insert.mpr <| Or.inr hi) _) j)

Result:
no goals

Proof state:
case insert.h.mk
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k i j : ℕ
e : (i, j) ∈ antidiagonal k
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Tactic:
obtain rfl : i + j = k := mem_antidiagonal.mp e

Result:
case insert.h.mk
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - (i + j))

Proof state:
case empty
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ ∅, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (if k = 0 then 1 else 0) ∈ ⊤

Tactic:
exact Submodule.mem_top

Result:
no goals

Proof state:
case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ∑ x ∈ antidiagonal k, (f a).coeff x.1 * (∏ x ∈ s, f x).coeff x.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Tactic:
apply sum_mem

Result:
case insert.h
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ∀ c ∈ antidiagonal k, (f a).coeff c.1 * (∏ x ∈ s, f x).coeff c.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Proof state:
case insert.h
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ∀ c ∈ antidiagonal k, (f a).coeff c.1 * (∏ x ∈ s, f x).coeff c.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Tactic:
rintro ⟨i, j⟩ e

Result:
case insert.h.mk
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k i j : ℕ
e : (i, j) ∈ antidiagonal k
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Proof state:
case insert.h.mk
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - (i + j))

Tactic:
apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub

Result:
case insert.h.mk.a
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ antidiagonal (i + j)
⊢ (f a).coeff (i, j).1 * (∏ x ∈ s, f x).coeff (i, j).2 ∈ I ^ (n a - i + (∑ x ∈ s, n x - j))