case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ↑(coeff R n) (φ₁ * φ₂ * φ₃) = ↑(coeff R n) (φ₁ * (φ₂ * φ₃))
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
⊢ φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)
ext1 n
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ x in Finset.sigma (antidiagonal n) fun a => antidiagonal a.fst,
      ↑(coeff R x.snd.fst) φ₁ * ↑(coeff R x.snd.snd) φ₂ * ↑(coeff R x.fst.snd) φ₃ =
    ∑ x in Finset.sigma (antidiagonal n) fun a => antidiagonal a.snd,
      ↑(coeff R x.fst.fst) φ₁ * (↑(coeff R x.snd.fst) φ₂ * ↑(coeff R x.snd.snd) φ₃)
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ↑(coeff R n) (φ₁ * φ₂ * φ₃) = ↑(coeff R n) (φ₁ * (φ₂ * φ₃))
simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma']
case h.refine'_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    a.fst.fst + a.fst.snd = n → a.snd.fst + a.snd.snd = a.fst.fst → a.snd.fst + (a.snd.snd + a.fst.snd) = n ∧ True

case h.refine'_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    a.fst.fst + a.fst.snd = n →
      a.snd.fst + a.snd.snd = a.fst.fst →
        ↑(coeff R a.snd.fst) φ₁ * ↑(coeff R a.snd.snd) φ₂ * ↑(coeff R a.fst.snd) φ₃ =
          ↑(coeff R a.snd.fst) φ₁ * (↑(coeff R a.snd.snd) φ₂ * ↑(coeff R a.fst.snd) φ₃)

case h.refine'_3
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (a₁ a₂ : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    a₁.fst.fst + a₁.fst.snd = n →
      a₁.snd.fst + a₁.snd.snd = a₁.fst.fst →
        a₂.fst.fst + a₂.fst.snd = n →
          a₂.snd.fst + a₂.snd.snd = a₂.fst.fst →
            { fst := (a₁.snd.fst, a₁.snd.snd + a₁.fst.snd), snd := (a₁.snd.snd, a₁.fst.snd) } =
                { fst := (a₂.snd.fst, a₂.snd.snd + a₂.fst.snd), snd := (a₂.snd.snd, a₂.fst.snd) } →
              a₁ = a₂

case h.refine'_4
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (b : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    b.fst.fst + b.fst.snd = n →
      b.snd.fst + b.snd.snd = b.fst.snd →
        ∃ a,
          (a.fst.fst + a.fst.snd = n ∧ a.snd.fst + a.snd.snd = a.fst.fst) ∧
            b = { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }
case h
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ x in Finset.sigma (antidiagonal n) fun a => antidiagonal a.fst,
      ↑(coeff R x.snd.fst) φ₁ * ↑(coeff R x.snd.snd) φ₂ * ↑(coeff R x.fst.snd) φ₃ =
    ∑ x in Finset.sigma (antidiagonal n) fun a => antidiagonal a.snd,
      ↑(coeff R x.fst.fst) φ₁ * (↑(coeff R x.snd.fst) φ₂ * ↑(coeff R x.snd.snd) φ₃)
refine' Finset.sum_bij (fun p _ => ⟨(p.2.1, p.2.2 + p.1.2), (p.2.2, p.1.2)⟩) _ _ _ _ <;>
  simp only [mem_antidiagonal, Finset.mem_sigma, heq_iff_eq, Prod.mk.inj_iff, and_imp,
    exists_prop]
case h.refine'_1.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n i j k l : σ →₀ ℕ
⊢ { fst := (i, j), snd := (k, l) }.fst.fst + { fst := (i, j), snd := (k, l) }.fst.snd = n →
    { fst := (i, j), snd := (k, l) }.snd.fst + { fst := (i, j), snd := (k, l) }.snd.snd =
        { fst := (i, j), snd := (k, l) }.fst.fst →
      { fst := (i, j), snd := (k, l) }.snd.fst +
            ({ fst := (i, j), snd := (k, l) }.snd.snd + { fst := (i, j), snd := (k, l) }.fst.snd) =
          n ∧
        True
case h.refine'_1
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    a.fst.fst + a.fst.snd = n → a.snd.fst + a.snd.snd = a.fst.fst → a.snd.fst + (a.snd.snd + a.fst.snd) = n ∧ True
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩
case h.refine'_1.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n i j k l : σ →₀ ℕ
⊢ i + j = n → k + l = i → k + (l + j) = n ∧ True
case h.refine'_1.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n i j k l : σ →₀ ℕ
⊢ { fst := (i, j), snd := (k, l) }.fst.fst + { fst := (i, j), snd := (k, l) }.fst.snd = n →
    { fst := (i, j), snd := (k, l) }.snd.fst + { fst := (i, j), snd := (k, l) }.snd.snd =
        { fst := (i, j), snd := (k, l) }.fst.fst →
      { fst := (i, j), snd := (k, l) }.snd.fst +
            ({ fst := (i, j), snd := (k, l) }.snd.snd + { fst := (i, j), snd := (k, l) }.fst.snd) =
          n ∧
        True
dsimp only
case h.refine'_1.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
j k l : σ →₀ ℕ
⊢ k + (l + j) = k + l + j ∧ True
case h.refine'_1.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n i j k l : σ →₀ ℕ
⊢ i + j = n → k + l = i → k + (l + j) = n ∧ True
rintro rfl rfl
no goals
case h.refine'_1.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
j k l : σ →₀ ℕ
⊢ k + (l + j) = k + l + j ∧ True
simp [add_assoc]
case h.refine'_2.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n a b c d : σ →₀ ℕ
⊢ { fst := (a, b), snd := (c, d) }.fst.fst + { fst := (a, b), snd := (c, d) }.fst.snd = n →
    { fst := (a, b), snd := (c, d) }.snd.fst + { fst := (a, b), snd := (c, d) }.snd.snd =
        { fst := (a, b), snd := (c, d) }.fst.fst →
      ↑(coeff R { fst := (a, b), snd := (c, d) }.snd.fst) φ₁ * ↑(coeff R { fst := (a, b), snd := (c, d) }.snd.snd) φ₂ *
          ↑(coeff R { fst := (a, b), snd := (c, d) }.fst.snd) φ₃ =
        ↑(coeff R { fst := (a, b), snd := (c, d) }.snd.fst) φ₁ *
          (↑(coeff R { fst := (a, b), snd := (c, d) }.snd.snd) φ₂ *
            ↑(coeff R { fst := (a, b), snd := (c, d) }.fst.snd) φ₃)
case h.refine'_2
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    a.fst.fst + a.fst.snd = n →
      a.snd.fst + a.snd.snd = a.fst.fst →
        ↑(coeff R a.snd.fst) φ₁ * ↑(coeff R a.snd.snd) φ₂ * ↑(coeff R a.fst.snd) φ₃ =
          ↑(coeff R a.snd.fst) φ₁ * (↑(coeff R a.snd.snd) φ₂ * ↑(coeff R a.fst.snd) φ₃)
rintro ⟨⟨a, b⟩, ⟨c, d⟩⟩
case h.refine'_2.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n a b c d : σ →₀ ℕ
⊢ a + b = n →
    c + d = a →
      ↑(coeff R c) φ₁ * ↑(coeff R d) φ₂ * ↑(coeff R b) φ₃ = ↑(coeff R c) φ₁ * (↑(coeff R d) φ₂ * ↑(coeff R b) φ₃)
case h.refine'_2.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n a b c d : σ →₀ ℕ
⊢ { fst := (a, b), snd := (c, d) }.fst.fst + { fst := (a, b), snd := (c, d) }.fst.snd = n →
    { fst := (a, b), snd := (c, d) }.snd.fst + { fst := (a, b), snd := (c, d) }.snd.snd =
        { fst := (a, b), snd := (c, d) }.fst.fst →
      ↑(coeff R { fst := (a, b), snd := (c, d) }.snd.fst) φ₁ * ↑(coeff R { fst := (a, b), snd := (c, d) }.snd.snd) φ₂ *
          ↑(coeff R { fst := (a, b), snd := (c, d) }.fst.snd) φ₃ =
        ↑(coeff R { fst := (a, b), snd := (c, d) }.snd.fst) φ₁ *
          (↑(coeff R { fst := (a, b), snd := (c, d) }.snd.snd) φ₂ *
            ↑(coeff R { fst := (a, b), snd := (c, d) }.fst.snd) φ₃)
dsimp only
case h.refine'_2.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
b c d : σ →₀ ℕ
⊢ ↑(coeff R c) φ₁ * ↑(coeff R d) φ₂ * ↑(coeff R b) φ₃ = ↑(coeff R c) φ₁ * (↑(coeff R d) φ₂ * ↑(coeff R b) φ₃)
case h.refine'_2.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n a b c d : σ →₀ ℕ
⊢ a + b = n →
    c + d = a →
      ↑(coeff R c) φ₁ * ↑(coeff R d) φ₂ * ↑(coeff R b) φ₃ = ↑(coeff R c) φ₁ * (↑(coeff R d) φ₂ * ↑(coeff R b) φ₃)
rintro rfl rfl
no goals
case h.refine'_2.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
b c d : σ →₀ ℕ
⊢ ↑(coeff R c) φ₁ * ↑(coeff R d) φ₂ * ↑(coeff R b) φ₃ = ↑(coeff R c) φ₁ * (↑(coeff R d) φ₂ * ↑(coeff R b) φ₃)
apply mul_assoc
case h.refine'_3.mk.mk.mk.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n a b c d i j k l : σ →₀ ℕ
⊢ { fst := (a, b), snd := (c, d) }.fst.fst + { fst := (a, b), snd := (c, d) }.fst.snd = n →
    { fst := (a, b), snd := (c, d) }.snd.fst + { fst := (a, b), snd := (c, d) }.snd.snd =
        { fst := (a, b), snd := (c, d) }.fst.fst →
      { fst := (i, j), snd := (k, l) }.fst.fst + { fst := (i, j), snd := (k, l) }.fst.snd = n →
        { fst := (i, j), snd := (k, l) }.snd.fst + { fst := (i, j), snd := (k, l) }.snd.snd =
            { fst := (i, j), snd := (k, l) }.fst.fst →
          {
                fst :=
                  ({ fst := (a, b), snd := (c, d) }.snd.fst,
                    { fst := (a, b), snd := (c, d) }.snd.snd + { fst := (a, b), snd := (c, d) }.fst.snd),
                snd := ({ fst := (a, b), snd := (c, d) }.snd.snd, { fst := (a, b), snd := (c, d) }.fst.snd) } =
              {
                fst :=
                  ({ fst := (i, j), snd := (k, l) }.snd.fst,
                    { fst := (i, j), snd := (k, l) }.snd.snd + { fst := (i, j), snd := (k, l) }.fst.snd),
                snd := ({ fst := (i, j), snd := (k, l) }.snd.snd, { fst := (i, j), snd := (k, l) }.fst.snd) } →
            { fst := (a, b), snd := (c, d) } = { fst := (i, j), snd := (k, l) }
case h.refine'_3
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (a₁ a₂ : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    a₁.fst.fst + a₁.fst.snd = n →
      a₁.snd.fst + a₁.snd.snd = a₁.fst.fst →
        a₂.fst.fst + a₂.fst.snd = n →
          a₂.snd.fst + a₂.snd.snd = a₂.fst.fst →
            { fst := (a₁.snd.fst, a₁.snd.snd + a₁.fst.snd), snd := (a₁.snd.snd, a₁.fst.snd) } =
                { fst := (a₂.snd.fst, a₂.snd.snd + a₂.fst.snd), snd := (a₂.snd.snd, a₂.fst.snd) } →
              a₁ = a₂
rintro ⟨⟨a, b⟩, ⟨c, d⟩⟩ ⟨⟨i, j⟩, ⟨k, l⟩⟩
case h.refine'_3.mk.mk.mk.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n a b c d i j k l : σ →₀ ℕ
⊢ a + b = n →
    c + d = a →
      i + j = n →
        k + l = i →
          { fst := (c, d + b), snd := (d, b) } = { fst := (k, l + j), snd := (l, j) } →
            { fst := (a, b), snd := (c, d) } = { fst := (i, j), snd := (k, l) }
case h.refine'_3.mk.mk.mk.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n a b c d i j k l : σ →₀ ℕ
⊢ { fst := (a, b), snd := (c, d) }.fst.fst + { fst := (a, b), snd := (c, d) }.fst.snd = n →
    { fst := (a, b), snd := (c, d) }.snd.fst + { fst := (a, b), snd := (c, d) }.snd.snd =
        { fst := (a, b), snd := (c, d) }.fst.fst →
      { fst := (i, j), snd := (k, l) }.fst.fst + { fst := (i, j), snd := (k, l) }.fst.snd = n →
        { fst := (i, j), snd := (k, l) }.snd.fst + { fst := (i, j), snd := (k, l) }.snd.snd =
            { fst := (i, j), snd := (k, l) }.fst.fst →
          {
                fst :=
                  ({ fst := (a, b), snd := (c, d) }.snd.fst,
                    { fst := (a, b), snd := (c, d) }.snd.snd + { fst := (a, b), snd := (c, d) }.fst.snd),
                snd := ({ fst := (a, b), snd := (c, d) }.snd.snd, { fst := (a, b), snd := (c, d) }.fst.snd) } =
              {
                fst :=
                  ({ fst := (i, j), snd := (k, l) }.snd.fst,
                    { fst := (i, j), snd := (k, l) }.snd.snd + { fst := (i, j), snd := (k, l) }.fst.snd),
                snd := ({ fst := (i, j), snd := (k, l) }.snd.snd, { fst := (i, j), snd := (k, l) }.fst.snd) } →
            { fst := (a, b), snd := (c, d) } = { fst := (i, j), snd := (k, l) }
dsimp only
case h.refine'_3.mk.mk.mk.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
b c d j k l : σ →₀ ℕ
⊢ { fst := (c, d + b), snd := (d, b) } = { fst := (k, l + j), snd := (l, j) } →
    { fst := (c + d, b), snd := (c, d) } = { fst := (k + l, j), snd := (k, l) }
case h.refine'_3.mk.mk.mk.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n a b c d i j k l : σ →₀ ℕ
⊢ a + b = n →
    c + d = a →
      i + j = n →
        k + l = i →
          { fst := (c, d + b), snd := (d, b) } = { fst := (k, l + j), snd := (l, j) } →
            { fst := (a, b), snd := (c, d) } = { fst := (i, j), snd := (k, l) }
rintro rfl rfl - rfl
case h.refine'_3.mk.mk.mk.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
b c d j k l : σ →₀ ℕ
⊢ c = k → d + b = l + j → d = l → b = j → (c + d = k + l ∧ b = j) ∧ c = k ∧ d = l
case h.refine'_3.mk.mk.mk.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
b c d j k l : σ →₀ ℕ
⊢ { fst := (c, d + b), snd := (d, b) } = { fst := (k, l + j), snd := (l, j) } →
    { fst := (c + d, b), snd := (c, d) } = { fst := (k + l, j), snd := (k, l) }
simp only [Sigma.mk.inj_iff, Prod.mk.injEq, heq_iff_eq, and_imp]
case h.refine'_3.mk.mk.mk.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
b c d : σ →₀ ℕ
⊢ (c + d = c + d ∧ b = b) ∧ c = c ∧ d = d
case h.refine'_3.mk.mk.mk.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
b c d j k l : σ →₀ ℕ
⊢ c = k → d + b = l + j → d = l → b = j → (c + d = k + l ∧ b = j) ∧ c = k ∧ d = l
rintro rfl - rfl rfl
no goals
case h.refine'_3.mk.mk.mk.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
b c d : σ →₀ ℕ
⊢ (c + d = c + d ∧ b = b) ∧ c = c ∧ d = d
simp only [and_self]
case h.refine'_4.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n i j k l : σ →₀ ℕ
⊢ { fst := (i, j), snd := (k, l) }.fst.fst + { fst := (i, j), snd := (k, l) }.fst.snd = n →
    { fst := (i, j), snd := (k, l) }.snd.fst + { fst := (i, j), snd := (k, l) }.snd.snd =
        { fst := (i, j), snd := (k, l) }.fst.snd →
      ∃ a,
        (a.fst.fst + a.fst.snd = n ∧ a.snd.fst + a.snd.snd = a.fst.fst) ∧
          { fst := (i, j), snd := (k, l) } =
            { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }
case h.refine'_4
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∀ (b : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    b.fst.fst + b.fst.snd = n →
      b.snd.fst + b.snd.snd = b.fst.snd →
        ∃ a,
          (a.fst.fst + a.fst.snd = n ∧ a.snd.fst + a.snd.snd = a.fst.fst) ∧
            b = { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }
rintro ⟨⟨i, j⟩, ⟨k, l⟩⟩
case h.refine'_4.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n i j k l : σ →₀ ℕ
⊢ i + j = n →
    k + l = j →
      ∃ a,
        (a.fst.fst + a.fst.snd = n ∧ a.snd.fst + a.snd.snd = a.fst.fst) ∧
          { fst := (i, j), snd := (k, l) } =
            { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }
case h.refine'_4.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n i j k l : σ →₀ ℕ
⊢ { fst := (i, j), snd := (k, l) }.fst.fst + { fst := (i, j), snd := (k, l) }.fst.snd = n →
    { fst := (i, j), snd := (k, l) }.snd.fst + { fst := (i, j), snd := (k, l) }.snd.snd =
        { fst := (i, j), snd := (k, l) }.fst.snd →
      ∃ a,
        (a.fst.fst + a.fst.snd = n ∧ a.snd.fst + a.snd.snd = a.fst.fst) ∧
          { fst := (i, j), snd := (k, l) } =
            { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }
dsimp only
case h.refine'_4.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
i k l : σ →₀ ℕ
⊢ ∃ a,
    (a.fst.fst + a.fst.snd = i + (k + l) ∧ a.snd.fst + a.snd.snd = a.fst.fst) ∧
      { fst := (i, k + l), snd := (k, l) } =
        { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }
case h.refine'_4.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n✝ : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
n i j k l : σ →₀ ℕ
⊢ i + j = n →
    k + l = j →
      ∃ a,
        (a.fst.fst + a.fst.snd = n ∧ a.snd.fst + a.snd.snd = a.fst.fst) ∧
          { fst := (i, j), snd := (k, l) } =
            { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }
rintro rfl rfl
no goals
case h.refine'_4.mk.mk.mk
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R
i k l : σ →₀ ℕ
⊢ ∃ a,
    (a.fst.fst + a.fst.snd = i + (k + l) ∧ a.snd.fst + a.snd.snd = a.fst.fst) ∧
      { fst := (i, k + l), snd := (k, l) } =
        { fst := (a.snd.fst, a.snd.snd + a.fst.snd), snd := (a.snd.snd, a.fst.snd) }
refine' ⟨⟨(i + k, l), (i, k)⟩, _, _⟩ <;> simp [add_assoc]