case coeff.h
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ coeff (x * y * z) b = coeff (x * (y * z)) b
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
⊢ x * y * z = x * (y * z)
ext b
case coeff.h
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∑ ij in addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b,
      coeff (x * y) ij.fst * coeff z ij.snd =
    ∑ ij in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b,
      coeff x ij.fst * coeff (y * z) ij.snd
case coeff.h
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ coeff (x * y * z) b = coeff (x * (y * z)) b
rw [mul_coeff_left' (x.isPwo_support.add y.isPwo_support) support_mul_subset_add_support,
  mul_coeff_right' (y.isPwo_support.add z.isPwo_support) support_mul_subset_add_support]
case coeff.h
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∑ x_1 in
      Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
        addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst,
      coeff x x_1.snd.fst * coeff y x_1.snd.snd * coeff z x_1.fst.snd =
    ∑ x_1 in
      Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b) fun a =>
        addAntidiagonal (_ : Set.IsPwo (support y)) (_ : Set.IsPwo (support z)) a.snd,
      coeff x x_1.fst.fst * (coeff y x_1.snd.fst * coeff z x_1.snd.snd)
case coeff.h
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∑ ij in addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b,
      coeff (x * y) ij.fst * coeff z ij.snd =
    ∑ ij in addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b,
      coeff x ij.fst * coeff (y * z) ij.snd
simp only [mul_coeff, add_coeff, sum_mul, mul_sum, sum_sigma']
case coeff.h.refine'_1
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∀ (a : (_ : Γ × Γ) × Γ × Γ)
    (h₁ :
      a ∈
        Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
          addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst)
    (h₂ : coeff x a.snd.fst * coeff y a.snd.snd * coeff z a.fst.snd ≠ 0),
    (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁ h₂ ∈
      Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b) fun a =>
        addAntidiagonal (_ : Set.IsPwo (support y)) (_ : Set.IsPwo (support z)) a.snd

case coeff.h.refine'_2
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∀ (a₁ a₂ : (_ : Γ × Γ) × Γ × Γ)
    (h₁₁ :
      a₁ ∈
        Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
          addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst)
    (h₁₂ : coeff x a₁.snd.fst * coeff y a₁.snd.snd * coeff z a₁.fst.snd ≠ 0)
    (h₂₁ :
      a₂ ∈
        Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
          addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst)
    (h₂₂ : coeff x a₂.snd.fst * coeff y a₂.snd.snd * coeff z a₂.fst.snd ≠ 0),
    (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a₁ h₁₁ h₁₂ =
        (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a₂ h₂₁ h₂₂ →
      a₁ = a₂

case coeff.h.refine'_3
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∀ (b_1 : (_ : Γ × Γ) × Γ × Γ),
    (b_1 ∈
        Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b) fun a =>
          addAntidiagonal (_ : Set.IsPwo (support y)) (_ : Set.IsPwo (support z)) a.snd) →
      coeff x b_1.fst.fst * (coeff y b_1.snd.fst * coeff z b_1.snd.snd) ≠ 0 →
        ∃ a h₁ h₂,
          b_1 = (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁ h₂

case coeff.h.refine'_4
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∀ (a : (_ : Γ × Γ) × Γ × Γ)
    (h₁ :
      a ∈
        Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
          addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst)
    (h₂ : coeff x a.snd.fst * coeff y a.snd.snd * coeff z a.fst.snd ≠ 0),
    coeff x a.snd.fst * coeff y a.snd.snd * coeff z a.fst.snd =
      coeff x
          ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁
                h₂).fst.fst *
        (coeff y
            ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁
                  h₂).snd.fst *
          coeff z
            ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁
                  h₂).snd.snd)
case coeff.h
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∑ x_1 in
      Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
        addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst,
      coeff x x_1.snd.fst * coeff y x_1.snd.snd * coeff z x_1.fst.snd =
    ∑ x_1 in
      Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b) fun a =>
        addAntidiagonal (_ : Set.IsPwo (support y)) (_ : Set.IsPwo (support z)) a.snd,
      coeff x x_1.fst.fst * (coeff y x_1.snd.fst * coeff z x_1.snd.snd)
refine' sum_bij_ne_zero (fun a _ _ => ⟨⟨a.2.1, a.2.2 + a.1.2⟩, ⟨a.2.2, a.1.2⟩⟩) _ _ _ _
case coeff.h.refine'_1.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i j k l : Γ
H1 :
  { fst := (i, j), snd := (k, l) } ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst
H2 :
  coeff x { fst := (i, j), snd := (k, l) }.snd.fst * coeff y { fst := (i, j), snd := (k, l) }.snd.snd *
      coeff z { fst := (i, j), snd := (k, l) }.fst.snd ≠
    0
⊢ (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
      { fst := (i, j), snd := (k, l) } H1 H2 ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support y)) (_ : Set.IsPwo (support z)) a.snd
case coeff.h.refine'_1
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∀ (a : (_ : Γ × Γ) × Γ × Γ)
    (h₁ :
      a ∈
        Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
          addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst)
    (h₂ : coeff x a.snd.fst * coeff y a.snd.snd * coeff z a.fst.snd ≠ 0),
    (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁ h₂ ∈
      Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b) fun a =>
        addAntidiagonal (_ : Set.IsPwo (support y)) (_ : Set.IsPwo (support z)) a.snd
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ H1 H2
case coeff.h.refine'_1.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i j k l : Γ
H2 : ¬coeff x k * coeff y l * coeff z j = 0
H1 : (i ∈ support x + support y ∧ j ∈ support z ∧ i + j = b) ∧ k ∈ support x ∧ l ∈ support y ∧ k + l = i
⊢ (k ∈ support x ∧ l + j ∈ support y + support z ∧ k + (l + j) = b) ∧ l ∈ support y ∧ j ∈ support z
case coeff.h.refine'_1.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i j k l : Γ
H1 :
  { fst := (i, j), snd := (k, l) } ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst
H2 :
  coeff x { fst := (i, j), snd := (k, l) }.snd.fst * coeff y { fst := (i, j), snd := (k, l) }.snd.snd *
      coeff z { fst := (i, j), snd := (k, l) }.fst.snd ≠
    0
⊢ (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
      { fst := (i, j), snd := (k, l) } H1 H2 ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support y)) (_ : Set.IsPwo (support z)) a.snd
simp only [and_true_iff, Set.image2_add, eq_self_iff_true, mem_addAntidiagonal, Ne.def,
  Set.image_prod, mem_sigma, Set.mem_setOf_eq] at H1 H2⊢
case coeff.h.refine'_1.mk.mk.mk.intro.intro.intro.intro.intro
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
j k l : Γ
H2 : ¬coeff x k * coeff y l * coeff z j = 0
nz : j ∈ support z
nx : k ∈ support x
ny : l ∈ support y
H3 : k + l ∈ support x + support y
⊢ (k ∈ support x ∧ l + j ∈ support y + support z ∧ k + (l + j) = k + l + j) ∧ l ∈ support y ∧ j ∈ support z
case coeff.h.refine'_1.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i j k l : Γ
H2 : ¬coeff x k * coeff y l * coeff z j = 0
H1 : (i ∈ support x + support y ∧ j ∈ support z ∧ i + j = b) ∧ k ∈ support x ∧ l ∈ support y ∧ k + l = i
⊢ (k ∈ support x ∧ l + j ∈ support y + support z ∧ k + (l + j) = b) ∧ l ∈ support y ∧ j ∈ support z
obtain ⟨⟨H3, nz, rfl⟩, nx, ny, rfl⟩ := H1
no goals
case coeff.h.refine'_1.mk.mk.mk.intro.intro.intro.intro.intro
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
j k l : Γ
H2 : ¬coeff x k * coeff y l * coeff z j = 0
nz : j ∈ support z
nx : k ∈ support x
ny : l ∈ support y
H3 : k + l ∈ support x + support y
⊢ (k ∈ support x ∧ l + j ∈ support y + support z ∧ k + (l + j) = k + l + j) ∧ l ∈ support y ∧ j ∈ support z
exact ⟨⟨nx, Set.add_mem_add ny nz, (add_assoc _ _ _).symm⟩, ny, nz⟩
case coeff.h.refine'_2.mk.mk.mk.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i1 j1 k1 l1 i2 j2 k2 l2 : Γ
H1 :
  { fst := (i1, j1), snd := (k1, l1) } ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst
H2 :
  coeff x { fst := (i1, j1), snd := (k1, l1) }.snd.fst * coeff y { fst := (i1, j1), snd := (k1, l1) }.snd.snd *
      coeff z { fst := (i1, j1), snd := (k1, l1) }.fst.snd ≠
    0
H3 :
  { fst := (i2, j2), snd := (k2, l2) } ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst
H4 :
  coeff x { fst := (i2, j2), snd := (k2, l2) }.snd.fst * coeff y { fst := (i2, j2), snd := (k2, l2) }.snd.snd *
      coeff z { fst := (i2, j2), snd := (k2, l2) }.fst.snd ≠
    0
H5 :
  (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
      { fst := (i1, j1), snd := (k1, l1) } H1 H2 =
    (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
      { fst := (i2, j2), snd := (k2, l2) } H3 H4
⊢ { fst := (i1, j1), snd := (k1, l1) } = { fst := (i2, j2), snd := (k2, l2) }
case coeff.h.refine'_2
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∀ (a₁ a₂ : (_ : Γ × Γ) × Γ × Γ)
    (h₁₁ :
      a₁ ∈
        Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
          addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst)
    (h₁₂ : coeff x a₁.snd.fst * coeff y a₁.snd.snd * coeff z a₁.fst.snd ≠ 0)
    (h₂₁ :
      a₂ ∈
        Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
          addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst)
    (h₂₂ : coeff x a₂.snd.fst * coeff y a₂.snd.snd * coeff z a₂.fst.snd ≠ 0),
    (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a₁ h₁₁ h₁₂ =
        (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a₂ h₂₁ h₂₂ →
      a₁ = a₂
rintro ⟨⟨i1, j1⟩, k1, l1⟩ ⟨⟨i2, j2⟩, k2, l2⟩ H1 H2 H3 H4 H5
case coeff.h.refine'_2.mk.mk.mk.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i1 j1 k1 l1 i2 j2 k2 l2 : Γ
H2 :
  coeff x { fst := (i1, j1), snd := (k1, l1) }.snd.fst * coeff y { fst := (i1, j1), snd := (k1, l1) }.snd.snd *
      coeff z { fst := (i1, j1), snd := (k1, l1) }.fst.snd ≠
    0
H4 :
  coeff x { fst := (i2, j2), snd := (k2, l2) }.snd.fst * coeff y { fst := (i2, j2), snd := (k2, l2) }.snd.snd *
      coeff z { fst := (i2, j2), snd := (k2, l2) }.fst.snd ≠
    0
H5 : { fst := (k1, l1 + j1), snd := (l1, j1) } = { fst := (k2, l2 + j2), snd := (l2, j2) }
H1 : (i1 ∈ support x + support y ∧ j1 ∈ support z ∧ i1 + j1 = b) ∧ k1 ∈ support x ∧ l1 ∈ support y ∧ k1 + l1 = i1
H3 : (i2 ∈ support x + support y ∧ j2 ∈ support z ∧ i2 + j2 = b) ∧ k2 ∈ support x ∧ l2 ∈ support y ∧ k2 + l2 = i2
⊢ { fst := (i1, j1), snd := (k1, l1) } = { fst := (i2, j2), snd := (k2, l2) }
case coeff.h.refine'_2.mk.mk.mk.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i1 j1 k1 l1 i2 j2 k2 l2 : Γ
H1 :
  { fst := (i1, j1), snd := (k1, l1) } ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst
H2 :
  coeff x { fst := (i1, j1), snd := (k1, l1) }.snd.fst * coeff y { fst := (i1, j1), snd := (k1, l1) }.snd.snd *
      coeff z { fst := (i1, j1), snd := (k1, l1) }.fst.snd ≠
    0
H3 :
  { fst := (i2, j2), snd := (k2, l2) } ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst
H4 :
  coeff x { fst := (i2, j2), snd := (k2, l2) }.snd.fst * coeff y { fst := (i2, j2), snd := (k2, l2) }.snd.snd *
      coeff z { fst := (i2, j2), snd := (k2, l2) }.fst.snd ≠
    0
H5 :
  (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
      { fst := (i1, j1), snd := (k1, l1) } H1 H2 =
    (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
      { fst := (i2, j2), snd := (k2, l2) } H3 H4
⊢ { fst := (i1, j1), snd := (k1, l1) } = { fst := (i2, j2), snd := (k2, l2) }
simp only [Set.image2_add, Prod.mk.inj_iff, mem_addAntidiagonal, Ne.def, Set.image_prod,
  mem_sigma, Set.mem_setOf_eq, heq_iff_eq] at H1 H3 H5
case coeff.h.refine'_2.mk.mk.mk.mk.mk.mk.intro.intro.intro
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i1 j1 k1 l1 i2 : Γ
H2 :
  coeff x { fst := (i1, j1), snd := (k1, l1) }.snd.fst * coeff y { fst := (i1, j1), snd := (k1, l1) }.snd.snd *
      coeff z { fst := (i1, j1), snd := (k1, l1) }.fst.snd ≠
    0
H1 : (i1 ∈ support x + support y ∧ j1 ∈ support z ∧ i1 + j1 = b) ∧ k1 ∈ support x ∧ l1 ∈ support y ∧ k1 + l1 = i1
right✝ : l1 + j1 = l1 + j1
H4 :
  coeff x { fst := (i2, j1), snd := (k1, l1) }.snd.fst * coeff y { fst := (i2, j1), snd := (k1, l1) }.snd.snd *
      coeff z { fst := (i2, j1), snd := (k1, l1) }.fst.snd ≠
    0
H5 : { fst := (k1, l1 + j1), snd := (l1, j1) } = { fst := (k1, l1 + j1), snd := (l1, j1) }
H3 : (i2 ∈ support x + support y ∧ j1 ∈ support z ∧ i2 + j1 = b) ∧ k1 ∈ support x ∧ l1 ∈ support y ∧ k1 + l1 = i2
⊢ { fst := (i1, j1), snd := (k1, l1) } = { fst := (i2, j1), snd := (k1, l1) }
case coeff.h.refine'_2.mk.mk.mk.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i1 j1 k1 l1 i2 j2 k2 l2 : Γ
H2 :
  coeff x { fst := (i1, j1), snd := (k1, l1) }.snd.fst * coeff y { fst := (i1, j1), snd := (k1, l1) }.snd.snd *
      coeff z { fst := (i1, j1), snd := (k1, l1) }.fst.snd ≠
    0
H4 :
  coeff x { fst := (i2, j2), snd := (k2, l2) }.snd.fst * coeff y { fst := (i2, j2), snd := (k2, l2) }.snd.snd *
      coeff z { fst := (i2, j2), snd := (k2, l2) }.fst.snd ≠
    0
H5 : { fst := (k1, l1 + j1), snd := (l1, j1) } = { fst := (k2, l2 + j2), snd := (l2, j2) }
H1 : (i1 ∈ support x + support y ∧ j1 ∈ support z ∧ i1 + j1 = b) ∧ k1 ∈ support x ∧ l1 ∈ support y ∧ k1 + l1 = i1
H3 : (i2 ∈ support x + support y ∧ j2 ∈ support z ∧ i2 + j2 = b) ∧ k2 ∈ support x ∧ l2 ∈ support y ∧ k2 + l2 = i2
⊢ { fst := (i1, j1), snd := (k1, l1) } = { fst := (i2, j2), snd := (k2, l2) }
obtain (⟨⟨rfl, _⟩, rfl, rfl⟩ : (k1 = k2 ∧ l1 + j1 = l2 + j2) ∧ l1 = l2 ∧ j1 = j2) :=
  by simpa using H5
no goals
case coeff.h.refine'_2.mk.mk.mk.mk.mk.mk.intro.intro.intro
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i1 j1 k1 l1 i2 : Γ
H2 :
  coeff x { fst := (i1, j1), snd := (k1, l1) }.snd.fst * coeff y { fst := (i1, j1), snd := (k1, l1) }.snd.snd *
      coeff z { fst := (i1, j1), snd := (k1, l1) }.fst.snd ≠
    0
H1 : (i1 ∈ support x + support y ∧ j1 ∈ support z ∧ i1 + j1 = b) ∧ k1 ∈ support x ∧ l1 ∈ support y ∧ k1 + l1 = i1
right✝ : l1 + j1 = l1 + j1
H4 :
  coeff x { fst := (i2, j1), snd := (k1, l1) }.snd.fst * coeff y { fst := (i2, j1), snd := (k1, l1) }.snd.snd *
      coeff z { fst := (i2, j1), snd := (k1, l1) }.fst.snd ≠
    0
H5 : { fst := (k1, l1 + j1), snd := (l1, j1) } = { fst := (k1, l1 + j1), snd := (l1, j1) }
H3 : (i2 ∈ support x + support y ∧ j1 ∈ support z ∧ i2 + j1 = b) ∧ k1 ∈ support x ∧ l1 ∈ support y ∧ k1 + l1 = i2
⊢ { fst := (i1, j1), snd := (k1, l1) } = { fst := (i2, j1), snd := (k1, l1) }
simp only [and_true_iff, Prod.mk.inj_iff, eq_self_iff_true, heq_iff_eq, ← H1.2.2.2, ← H3.2.2.2]
no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i1 j1 k1 l1 i2 j2 k2 l2 : Γ
H2 :
  coeff x { fst := (i1, j1), snd := (k1, l1) }.snd.fst * coeff y { fst := (i1, j1), snd := (k1, l1) }.snd.snd *
      coeff z { fst := (i1, j1), snd := (k1, l1) }.fst.snd ≠
    0
H4 :
  coeff x { fst := (i2, j2), snd := (k2, l2) }.snd.fst * coeff y { fst := (i2, j2), snd := (k2, l2) }.snd.snd *
      coeff z { fst := (i2, j2), snd := (k2, l2) }.fst.snd ≠
    0
H5 : { fst := (k1, l1 + j1), snd := (l1, j1) } = { fst := (k2, l2 + j2), snd := (l2, j2) }
H1 : (i1 ∈ support x + support y ∧ j1 ∈ support z ∧ i1 + j1 = b) ∧ k1 ∈ support x ∧ l1 ∈ support y ∧ k1 + l1 = i1
H3 : (i2 ∈ support x + support y ∧ j2 ∈ support z ∧ i2 + j2 = b) ∧ k2 ∈ support x ∧ l2 ∈ support y ∧ k2 + l2 = i2
⊢ (k1 = k2 ∧ l1 + j1 = l2 + j2) ∧ l1 = l2 ∧ j1 = j2
simpa using H5
case coeff.h.refine'_3.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i j k l : Γ
H1 :
  { fst := (i, j), snd := (k, l) } ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support y)) (_ : Set.IsPwo (support z)) a.snd
H2 :
  coeff x { fst := (i, j), snd := (k, l) }.fst.fst *
      (coeff y { fst := (i, j), snd := (k, l) }.snd.fst * coeff z { fst := (i, j), snd := (k, l) }.snd.snd) ≠
    0
⊢ ∃ a h₁ h₂,
    { fst := (i, j), snd := (k, l) } =
      (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁ h₂
case coeff.h.refine'_3
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∀ (b_1 : (_ : Γ × Γ) × Γ × Γ),
    (b_1 ∈
        Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b) fun a =>
          addAntidiagonal (_ : Set.IsPwo (support y)) (_ : Set.IsPwo (support z)) a.snd) →
      coeff x b_1.fst.fst * (coeff y b_1.snd.fst * coeff z b_1.snd.snd) ≠ 0 →
        ∃ a h₁ h₂,
          b_1 = (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁ h₂
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ H1 H2
case coeff.h.refine'_3.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i j k l : Γ
H2 : ¬coeff x i * (coeff y k * coeff z l) = 0
H1 : (i ∈ support x ∧ j ∈ support y + support z ∧ i + j = b) ∧ k ∈ support y ∧ l ∈ support z ∧ k + l = j
⊢ ∃ a b_1 a_1 b_2,
    ((a ∈ support x + support y ∧ b_1 ∈ support z ∧ a + b_1 = b) ∧ a_1 ∈ support x ∧ b_2 ∈ support y ∧ a_1 + b_2 = a) ∧
      ¬coeff x a_1 * coeff y b_2 * coeff z b_1 = 0 ∧
        { fst := (i, j), snd := (k, l) } = { fst := (a_1, b_2 + b_1), snd := (b_2, b_1) }
case coeff.h.refine'_3.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i j k l : Γ
H1 :
  { fst := (i, j), snd := (k, l) } ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y + support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support y)) (_ : Set.IsPwo (support z)) a.snd
H2 :
  coeff x { fst := (i, j), snd := (k, l) }.fst.fst *
      (coeff y { fst := (i, j), snd := (k, l) }.snd.fst * coeff z { fst := (i, j), snd := (k, l) }.snd.snd) ≠
    0
⊢ ∃ a h₁ h₂,
    { fst := (i, j), snd := (k, l) } =
      (fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁ h₂
simp only [exists_prop, Set.image2_add, Prod.mk.inj_iff, mem_addAntidiagonal, Sigma.exists,
  Ne.def, Set.image_prod, mem_sigma, Set.mem_setOf_eq, heq_iff_eq, Prod.exists] at H1 H2⊢
case coeff.h.refine'_3.mk.mk.mk.intro.intro.intro.intro.intro
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
i k l : Γ
H2 : ¬coeff x i * (coeff y k * coeff z l) = 0
nx : i ∈ support x
ny : k ∈ support y
nz : l ∈ support z
H : k + l ∈ support y + support z
⊢ ∃ a b a_1 b_1,
    ((a ∈ support x + support y ∧ b ∈ support z ∧ a + b = i + (k + l)) ∧
        a_1 ∈ support x ∧ b_1 ∈ support y ∧ a_1 + b_1 = a) ∧
      ¬coeff x a_1 * coeff y b_1 * coeff z b = 0 ∧
        { fst := (i, k + l), snd := (k, l) } = { fst := (a_1, b_1 + b), snd := (b_1, b) }
case coeff.h.refine'_3.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i j k l : Γ
H2 : ¬coeff x i * (coeff y k * coeff z l) = 0
H1 : (i ∈ support x ∧ j ∈ support y + support z ∧ i + j = b) ∧ k ∈ support y ∧ l ∈ support z ∧ k + l = j
⊢ ∃ a b_1 a_1 b_2,
    ((a ∈ support x + support y ∧ b_1 ∈ support z ∧ a + b_1 = b) ∧ a_1 ∈ support x ∧ b_2 ∈ support y ∧ a_1 + b_2 = a) ∧
      ¬coeff x a_1 * coeff y b_2 * coeff z b_1 = 0 ∧
        { fst := (i, j), snd := (k, l) } = { fst := (a_1, b_2 + b_1), snd := (b_2, b_1) }
obtain ⟨⟨nx, H, rfl⟩, ny, nz, rfl⟩ := H1
no goals
case coeff.h.refine'_3.mk.mk.mk.intro.intro.intro.intro.intro
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
i k l : Γ
H2 : ¬coeff x i * (coeff y k * coeff z l) = 0
nx : i ∈ support x
ny : k ∈ support y
nz : l ∈ support z
H : k + l ∈ support y + support z
⊢ ∃ a b a_1 b_1,
    ((a ∈ support x + support y ∧ b ∈ support z ∧ a + b = i + (k + l)) ∧
        a_1 ∈ support x ∧ b_1 ∈ support y ∧ a_1 + b_1 = a) ∧
      ¬coeff x a_1 * coeff y b_1 * coeff z b = 0 ∧
        { fst := (i, k + l), snd := (k, l) } = { fst := (a_1, b_1 + b), snd := (b_1, b) }
exact
  ⟨i + k, l, i, k, ⟨⟨Set.add_mem_add nx ny, nz, add_assoc _ _ _⟩ , nx, ny, rfl⟩,
    fun h => H2 <| by rw [←h, mul_assoc], rfl⟩
no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
i k l : Γ
H2 : ¬coeff x i * (coeff y k * coeff z l) = 0
nx : i ∈ support x
ny : k ∈ support y
nz : l ∈ support z
H : k + l ∈ support y + support z
h : coeff x i * coeff y k * coeff z l = 0
⊢ coeff x i * (coeff y k * coeff z l) = 0
rw [←h, mul_assoc]
case coeff.h.refine'_4.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i j k l : Γ
h₁✝ :
  { fst := (i, j), snd := (k, l) } ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst
h₂✝ :
  coeff x { fst := (i, j), snd := (k, l) }.snd.fst * coeff y { fst := (i, j), snd := (k, l) }.snd.snd *
      coeff z { fst := (i, j), snd := (k, l) }.fst.snd ≠
    0
⊢ coeff x { fst := (i, j), snd := (k, l) }.snd.fst * coeff y { fst := (i, j), snd := (k, l) }.snd.snd *
      coeff z { fst := (i, j), snd := (k, l) }.fst.snd =
    coeff x
        ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
              { fst := (i, j), snd := (k, l) } h₁✝ h₂✝).fst.fst *
      (coeff y
          ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
                { fst := (i, j), snd := (k, l) } h₁✝ h₂✝).snd.fst *
        coeff z
          ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
                { fst := (i, j), snd := (k, l) } h₁✝ h₂✝).snd.snd)
case coeff.h.refine'_4
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b : Γ
⊢ ∀ (a : (_ : Γ × Γ) × Γ × Γ)
    (h₁ :
      a ∈
        Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
          addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst)
    (h₂ : coeff x a.snd.fst * coeff y a.snd.snd * coeff z a.fst.snd ≠ 0),
    coeff x a.snd.fst * coeff y a.snd.snd * coeff z a.fst.snd =
      coeff x
          ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁
                h₂).fst.fst *
        (coeff y
            ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁
                  h₂).snd.fst *
          coeff z
            ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }) a h₁
                  h₂).snd.snd)
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩ _ _
no goals
case coeff.h.refine'_4.mk.mk.mk
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalSemiring R
x y z : HahnSeries Γ R
b i j k l : Γ
h₁✝ :
  { fst := (i, j), snd := (k, l) } ∈
    Finset.sigma (addAntidiagonal (_ : Set.IsPwo (support x + support y)) (_ : Set.IsPwo (support z)) b) fun a =>
      addAntidiagonal (_ : Set.IsPwo (support x)) (_ : Set.IsPwo (support y)) a.fst
h₂✝ :
  coeff x { fst := (i, j), snd := (k, l) }.snd.fst * coeff y { fst := (i, j), snd := (k, l) }.snd.snd *
      coeff z { fst := (i, j), snd := (k, l) }.fst.snd ≠
    0
⊢ coeff x { fst := (i, j), snd := (k, l) }.snd.fst * coeff y { fst := (i, j), snd := (k, l) }.snd.snd *
      coeff z { fst := (i, j), snd := (k, l) }.fst.snd =
    coeff x
        ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
              { fst := (i, j), snd := (k, l) } h₁✝ h₂✝).fst.fst *
      (coeff y
          ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
                { fst := (i, j), snd := (k, l) } h₁✝ h₂✝).snd.fst *
        coeff z
          ((fun a x_1 x => { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) })
                { fst := (i, j), snd := (k, l) } h₁✝ h₂✝).snd.snd)
simp [mul_assoc]