case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
⊢ ↑(coeff R k) (↑(monomial R m) a * ↑(monomial R n) b) = ↑(coeff R k) (↑(monomial R (m + n)) (a * b))
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
⊢ ↑(monomial R m) a * ↑(monomial R n) b = ↑(monomial R (m + n)) (a * b)
ext k
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
⊢ (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
⊢ ↑(coeff R k) (↑(monomial R m) a * ↑(monomial R n) b) = ↑(coeff R k) (↑(monomial R (m + n)) (a * b))
simp only [coeff_mul_monomial, coeff_monomial]
case h.inl.inl.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = m + n
⊢ a * b = 0

case h.inl.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : k = m + n
⊢ 0 * b = a * b

case h.inl.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : ¬k = m + n
⊢ 0 * b = 0

case h.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : k = m + n
⊢ 0 = a * b
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
⊢ (if n ≤ k then (if k - n = m then a else 0) * b else 0) = if k = m + n then a * b else 0
split_ifs with h₁ h₂ h₃ h₃ h₂ <;> try rfl
no goals
case h.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : ¬k = m + n
⊢ 0 = 0
rfl
case h.inl.inl.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = k
⊢ a * b = 0
case h.inl.inl.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = m + n
⊢ a * b = 0
rw [← h₂, tsub_add_cancel_of_le h₁] at h₃
no goals
case h.inl.inl.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : k - n = m
h₃ : ¬k = k
⊢ a * b = 0
exact (h₃ rfl).elim
case h.inl.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬m = m
h₃ : k = m + n
⊢ 0 * b = a * b
case h.inl.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : k = m + n
⊢ 0 * b = a * b
rw [h₃, add_tsub_cancel_right] at h₂
no goals
case h.inl.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬m = m
h₃ : k = m + n
⊢ 0 * b = a * b
exact (h₂ rfl).elim
no goals
case h.inl.inr.inr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : n ≤ k
h₂ : ¬k - n = m
h₃ : ¬k = m + n
⊢ 0 * b = 0
exact MulZeroClass.zero_mul b
case h.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ m + n
h₂ : k = m + n
⊢ 0 = a * b
case h.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ k
h₂ : k = m + n
⊢ 0 = a * b
rw [h₂] at h₁
no goals
case h.inr.inl
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
a b : R
k : σ →₀ ℕ
h₁ : ¬n ≤ m + n
h₂ : k = m + n
⊢ 0 = a * b
exact (h₁ <| le_add_left le_rfl).elim