Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
a : Γ
s : Set Γ
hs : Set.IsPwo s
hxs : support x ⊆ s
⊢ ∑ ij in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a, coeff x ij.fst * coeff y ij.snd =
    ∑ ij in addAntidiagonal hs (_ : Set.IsPwo (support y)) a, coeff x ij.fst * coeff y ij.snd
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
a : Γ
s : Set Γ
hs : Set.IsPwo s
hxs : support x ⊆ s
⊢ coeff (x * y) a = ∑ ij in addAntidiagonal hs (_ : Set.IsPwo (support y)) a, coeff x ij.fst * coeff y ij.snd
rw [mul_coeff]
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
a : Γ
s : Set Γ
hs : Set.IsPwo s
hxs : support x ⊆ s
⊢ ∀ (x_1 : Γ × Γ),
    x_1 ∈
        addAntidiagonal hs (_ : Set.IsPwo (support y)) a \
          addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a →
      coeff x x_1.fst * coeff y x_1.snd = 0
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
a : Γ
s : Set Γ
hs : Set.IsPwo s
hxs : support x ⊆ s
⊢ ∑ ij in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a, coeff x ij.fst * coeff y ij.snd =
    ∑ ij in addAntidiagonal hs (_ : Set.IsPwo (support y)) a, coeff x ij.fst * coeff y ij.snd
apply sum_subset_zero_on_sdiff (addAntidiagonal_mono_left hxs) _ fun _ _ => rfl
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
a : Γ
s : Set Γ
hs : Set.IsPwo s
hxs : support x ⊆ s
b : Γ × Γ
hb :
  b ∈
    addAntidiagonal hs (_ : Set.IsPwo (support y)) a \
      addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a
⊢ coeff x b.fst * coeff y b.snd = 0
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
a : Γ
s : Set Γ
hs : Set.IsPwo s
hxs : support x ⊆ s
⊢ ∀ (x_1 : Γ × Γ),
    x_1 ∈
        addAntidiagonal hs (_ : Set.IsPwo (support y)) a \
          addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a →
      coeff x x_1.fst * coeff y x_1.snd = 0
intro b hb
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
a : Γ
s : Set Γ
hs : Set.IsPwo s
hxs : support x ⊆ s
b : Γ × Γ
hb : (b.fst ∈ s ∧ coeff y b.snd ≠ 0 ∧ b.fst + b.snd = a) ∧ (coeff y b.snd ≠ 0 ∧ b.fst + b.snd = a → coeff x b.fst = 0)
⊢ coeff x b.fst * coeff y b.snd = 0
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
a : Γ
s : Set Γ
hs : Set.IsPwo s
hxs : support x ⊆ s
b : Γ × Γ
hb :
  b ∈
    addAntidiagonal hs (_ : Set.IsPwo (support y)) a \
      addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a
⊢ coeff x b.fst * coeff y b.snd = 0
simp only [not_and', mem_sdiff, mem_addAntidiagonal, mem_support, not_ne_iff] at hb
no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : HahnSeries Γ R
a : Γ
s : Set Γ
hs : Set.IsPwo s
hxs : support x ⊆ s
b : Γ × Γ
hb : (b.fst ∈ s ∧ coeff y b.snd ≠ 0 ∧ b.fst + b.snd = a) ∧ (coeff y b.snd ≠ 0 ∧ b.fst + b.snd = a → coeff x b.fst = 0)
⊢ coeff x b.fst * coeff y b.snd = 0
rw [hb.2 ⟨hb.1.2.1, hb.1.2.2⟩, MulZeroClass.zero_mul]