Collecting terms

Stream: Is there code for X?

[Eric Wieser]

I've found myself with goals along the lines of x • A - y • B + z • A = p • B - q • B + r • A, and I'd like a tactic that splits this into two goals x + z = r and -y = p - q by matching coefficients of A and B respectively. Do we have anything like this?

[Eric Wieser]

Essentially, I guess this breaks down into some tactic to work out the collected goal state, and an abel tactic that knows about smul by non-integers

[Adam Topaz]

I'm not aware of such a tactic. You can pull it off with a good suffices : ... and abel/smul to close the goal it creates.

[Eric Wieser]

I really don't want to do that, as in my real situation I have A B C D, and each appears on each side 4 times with a 3-term coefficient

[Eric Wieser]

So the resulting suffices is huge

[Eric Wieser]

My real goal is

⊢ (x.re * y.re + c₁ * x.im_i * y.im_i + c₂ * x.im_j * y.im_j - c₁ * c₂ * x.im_k * y.im_k) • 1 +
          ((x.re * y.im_i + x.im_i * y.re - c₂ * x.im_j * y.im_k) • q.i + (c₂ * x.im_k * y.im_j) • q.i) +
        (x.re * y.im_j + c₁ * x.im_i * y.im_k + x.im_j * y.re - c₁ * x.im_k * y.im_i) • q.j +
      ((x.re * y.im_k + x.im_i * y.im_j - x.im_j * y.im_i) • q.k + (x.im_k * y.re) • q.k) =
    (y.re * x.re) • 1 + (y.re * x.im_i) • q.i + (y.re * x.im_j) • q.j + (y.re * x.im_k) • q.k +
          ((y.im_i * x.re) • q.i + (y.im_i * x.im_i) • c₁ • 1 + -((y.im_i * x.im_j) • q.k) +
             -((y.im_i * x.im_k * c₁) • q.j)) +
        ((y.im_j * x.re) • q.j + (y.im_j * x.im_i) • q.k + (y.im_j * x.im_j) • c₂ • 1 +
           (y.im_j * x.im_k * c₂) • q.i) +
      ((y.im_k * x.re) • q.k + (y.im_k * x.im_i * c₁) • q.j + -((y.im_k * x.im_j * c₂) • q.i) +
         -((y.im_k * x.im_k * (c₁ * c₂)) • 1))