-- Mathlib/Algebra/Polynomial/Expand.lean
theorem contract_mul_expand {p : ℕ} (hp : p ≠ 0) (f g : R[X]) :
    contract p (f * expand R p g) = contract p f * g

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : p ∣ y
⊢ f.coeff (x, y).1 * ((expand R p) g).coeff (x, y).2 = 0

Tactic:
obtain ⟨x, rfl⟩ : p ∣ x := (Nat.dvd_add_iff_left h).mpr (eq ▸ dvd_mul_left p n)

Result:
case pos.intro
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n y : ℕ
h : p ∣ y
x : ℕ
eq : (p * x, y).1 + (p * x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, y)
⊢ f.coeff (p * x, y).1 * ((expand R p) g).coeff (p * x, y).2 = 0

Proof state:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff (x.1 * p, x.2 * p).1 * ((expand R p) g).coeff (x.1 * p, x.2 * p).2 =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

Tactic:
simp_rw [coeff_expand_mul hp.bot_lt, coeff_contract hp]

Result:
no goals

Proof state:
case a.h.intro.intro
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
x : ℕ × ℕ
⊢ (x.1 * p, x.2 * p).1 + (x.1 * p, x.2 * p).2 = (x.1 + x.2) * p

Tactic:
simp_rw [add_mul]

Result:
no goals

Proof state:
case pos.intro.intro
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ ((x, y).1 + (x, y).2) * p = n * p

Tactic:
rw [← eq, mul_comm, mul_add]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ ((x, y).1 * p, (x, y).2 * p) = (p * x, p * y)

Tactic:
simp_rw [mul_comm]

Result:
no goals

Proof state:
case a.hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
⊢ f.coeff (x, y).1 * ((expand R p) g).coeff (x, y).2 = 0

Tactic:
by_cases h : p ∣ y

Result:
case pos
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : p ∣ y
⊢ f.coeff (x, y).1 * ((expand R p) g).coeff (x, y).2 = 0

case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
⊢ f.coeff (x, y).1 * ((expand R p) g).coeff (x, y).2 = 0

Proof state:
case a.h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ ⦃x : ℕ × ℕ⦄, (∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) → x.1 + x.2 = n * p

Tactic:
rintro _ ⟨x, rfl, rfl⟩

Result:
case a.h.intro.intro
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
x : ℕ × ℕ
⊢ (x.1 * p, x.2 * p).1 + (x.1 * p, x.2 * p).2 = (x.1 + x.2) * p

Proof state:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ (contract p (f * (expand R p) g)).coeff n = (contract p f * g).coeff n

Tactic:
rw [coeff_contract hp, coeff_mul, coeff_mul, ← sum_subset
  (s₁ := (antidiagonal n).image fun x ↦ (x.1 * p, x.2 * p)), sum_image]

Result:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∑ x ∈ antidiagonal n, f.coeff (x.1 * p, x.2 * p).1 * ((expand R p) g).coeff (x.1 * p, x.2 * p).2 =
    ∑ x ∈ antidiagonal n, (contract p f).coeff x.1 * g.coeff x.2

case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal n, ∀ y ∈ antidiagonal n, (x.1 * p, x.2 * p) = (y.1 * p, y.2 * p) → x = y

case a.h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x => (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

case a.hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x => (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0

Proof state:
case a.hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal (n * p),
    x ∉ image (fun x => (x.1 * p, x.2 * p)) (antidiagonal n) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0

Tactic:
simp_rw [mem_image, mem_antidiagonal]

Result:
case a.hf
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ (x : ℕ × ℕ),
    x.1 + x.2 = n * p → (¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) → f.coeff x.1 * ((expand R p) g).coeff x.2 = 0

Proof state:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ antidiagonal n, ∀ y ∈ antidiagonal n, (x.1 * p, x.2 * p) = (y.1 * p, y.2 * p) → x = y

Tactic:
intro x hx y hy eq

Result:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ antidiagonal n
y : ℕ × ℕ
hy : y ∈ antidiagonal n
eq : (x.1 * p, x.2 * p) = (y.1 * p, y.2 * p)
⊢ x = y

Proof state:
case pos.intro
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n y : ℕ
h : p ∣ y
x : ℕ
eq : (p * x, y).1 + (p * x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, y)
⊢ f.coeff (p * x, y).1 * ((expand R p) g).coeff (p * x, y).2 = 0

Tactic:
obtain ⟨y, rfl⟩ := h

Result:
case pos.intro.intro
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ f.coeff (p * x, p * y).1 * ((expand R p) g).coeff (p * x, p * y).2 = 0

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
⊢ contract p (f * (expand R p) g) = contract p f * g

Tactic:
ext n

Result:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ (contract p (f * (expand R p) g)).coeff n = (contract p f * g).coeff n

Proof state:
case a
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
x : ℕ × ℕ
hx : x ∈ antidiagonal n
y : ℕ × ℕ
hy : y ∈ antidiagonal n
eq : (x.1 * p, x.2 * p) = (y.1 * p, y.2 * p)
⊢ x = y

Tactic:
simpa only [Prod.ext_iff, Nat.mul_right_cancel_iff hp.bot_lt] using eq

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
⊢ f.coeff (x, y).1 * ((expand R p) g).coeff (x, y).2 = 0

Tactic:
rw [coeff_expand hp.bot_lt, if_neg h, mul_zero]

Result:
no goals

Proof state:
case pos.intro.intro
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ f.coeff (p * x, p * y).1 * ((expand R p) g).coeff (p * x, p * y).2 = 0

Tactic:
refine (nex ⟨⟨x, y⟩, (Nat.mul_right_cancel_iff hp.bot_lt).mp ?_, by simp_rw [mul_comm]⟩).elim

Result:
case pos.intro.intro
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ ((x, y).1 + (x, y).2) * p = n * p

Proof state:
case a.h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun x => (x.1 * p, x.2 * p)) (antidiagonal n) ⊆ antidiagonal (n * p)

Tactic:
simp_rw [subset_iff, mem_image, mem_antidiagonal]

Result:
case a.h
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ ⦃x : ℕ × ℕ⦄, (∃ a, a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) → x.1 + x.2 = n * p