case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
⊢ coeff (↑(single a) r * ↑(single b) s) x = coeff (↑(single (a + b)) (r * s)) x
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
⊢ ↑(single a) r * ↑(single b) s = ↑(single (a + b)) (r * s)
ext x
case pos
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ coeff (↑(single a) r * ↑(single b) s) x = coeff (↑(single (a + b)) (r * s)) x

case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ coeff (↑(single a) r * ↑(single b) s) x = coeff (↑(single (a + b)) (r * s)) x
case coeff.h
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
⊢ coeff (↑(single a) r * ↑(single b) s) x = coeff (↑(single (a + b)) (r * s)) x
by_cases h : x = a + b
case pos
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ coeff (↑(single a) r) a * s = coeff (↑(single (a + b)) (r * s)) (a + b)
case pos
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ coeff (↑(single a) r * ↑(single b) s) x = coeff (↑(single (a + b)) (r * s)) x
rw [h, mul_single_coeff_add]
no goals
case pos
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : x = a + b
⊢ coeff (↑(single a) r) a * s = coeff (↑(single (a + b)) (r * s)) (a + b)
simp
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀ (x_1 : Γ × Γ),
    x_1 ∈ addAntidiagonal (_ : Set.IsPwo (support (↑(single a) r))) (_ : Set.IsPwo (support (↑(single b) s))) x →
      coeff (↑(single a) r) x_1.fst * coeff (↑(single b) s) x_1.snd = 0
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ coeff (↑(single a) r * ↑(single b) s) x = coeff (↑(single (a + b)) (r * s)) x
rw [single_coeff_of_ne h, mul_coeff, sum_eq_zero]
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀ (x_1 : Γ × Γ),
    x_1.fst ∈ support (↑(single a) r) ∧ x_1.snd ∈ support (↑(single b) s) ∧ x_1.fst + x_1.snd = x →
      coeff (↑(single a) r) x_1.fst * coeff (↑(single b) s) x_1.snd = 0
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀ (x_1 : Γ × Γ),
    x_1 ∈ addAntidiagonal (_ : Set.IsPwo (support (↑(single a) r))) (_ : Set.IsPwo (support (↑(single b) s))) x →
      coeff (↑(single a) r) x_1.fst * coeff (↑(single b) s) x_1.snd = 0
simp_rw [mem_addAntidiagonal]
case neg.mk.intro.intro
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : (y, z).fst ∈ support (↑(single a) r)
hz : (y, z).snd ∈ support (↑(single b) s)
h : ¬(y, z).fst + (y, z).snd = a + b
⊢ coeff (↑(single a) r) (y, z).fst * coeff (↑(single b) s) (y, z).snd = 0
case neg
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
x : Γ
h : ¬x = a + b
⊢ ∀ (x_1 : Γ × Γ),
    x_1.fst ∈ support (↑(single a) r) ∧ x_1.snd ∈ support (↑(single b) s) ∧ x_1.fst + x_1.snd = x →
      coeff (↑(single a) r) x_1.fst * coeff (↑(single b) s) x_1.snd = 0
rintro ⟨y, z⟩ ⟨hy, hz, rfl⟩
case neg.mk.intro.intro
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : (y, z).fst ∈ support (↑(single a) r)
hz : (y, z).snd ∈ support (↑(single b) s)
h : ¬a + b = a + b
⊢ coeff (↑(single a) r) (y, z).fst * coeff (↑(single b) s) (y, z).snd = 0
case neg.mk.intro.intro
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : (y, z).fst ∈ support (↑(single a) r)
hz : (y, z).snd ∈ support (↑(single b) s)
h : ¬(y, z).fst + (y, z).snd = a + b
⊢ coeff (↑(single a) r) (y, z).fst * coeff (↑(single b) s) (y, z).snd = 0
rw [eq_of_mem_support_single hy, eq_of_mem_support_single hz] at h
no goals
case neg.mk.intro.intro
Γ : Type u_1
R : Type u_2
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
a b : Γ
r s : R
y z : Γ
hy : (y, z).fst ∈ support (↑(single a) r)
hz : (y, z).snd ∈ support (↑(single b) s)
h : ¬a + b = a + b
⊢ coeff (↑(single a) r) (y, z).fst * coeff (↑(single b) s) (y, z).snd = 0
exact (h rfl).elim