motive is not type correct with coe

Stream: new members

[Eric Wieser]

My state is:

q : ↑(x + y) = ↑x + ↑y
⊢ ⟨⇑fₛ r_1 * (↑x + ↑y), _⟩ = ⟨⇑fₛ r_1 * ↑x, _⟩ + ⟨⇑fₛ r_1 * ↑y, _⟩

and the obvious strategy would be rw q. However, this fails with

rewrite tactic failed, motive is not type correct
  λ (_a : G),
    ⟨⇑fₛ r_1 * (↑x + ↑y), _⟩ = ⟨⇑fₛ r_1 * ↑x, _⟩ + ⟨⇑fₛ r_1 * ↑y, _⟩ =
      (⟨⇑fₛ r_1 * (↑x + ↑y), _⟩ = ⟨⇑fₛ r_1 * ↑x, _⟩ + ⟨⇑fₛ r_1 * ↑y, _⟩)

Two questions then:

• How should I read this error message?
• Why won't q substitute?

[Eric Wieser]

Nevermind, I can't read. The error message is confusing though.

[Kevin Buzzard]

simp only [q] might make progress