unexpected `▸` insertion

Stream: lean4

[Eric Wieser]

This theorem is nonsense, but I still don't understand why lean accepts it

set_option pp.proofs true in
example {α} {C : α → Sort u} {a₁ a₂} (h : a₁ = a₂) (c₁ : C a₁) (c₂ : C a₂) :
    h ▸ c₁ = h ▸ c₂ := by
  sorry

when I look in the goal view, the target is h ▸ c₁ = h ▸ Eq.symm h ▸ c₂ not h ▸ c₁ = h ▸ c₂.

Where did the Eq.symm h ▸ come from?

[Damiano Testa]

Hovering over the black triangle of computer science, starts to say

`h ▸ e` is a macro built on top of `Eq.rec` and `Eq.symm` definitions ...

Maybe the "macro" realises that you want to apply it to rewrite a₂ and so needs the use Eq.symm. Kind of like a very obscure ←?

[Damiano Testa]

Also, how many Eq.symm do you expect to see in the goal below?

set_option pp.proofs true in
example {α} {C : α → Sort u} {a₁ a₂} (h : a₁ = a₂) (c₁ : C a₁) (c₂ : C a₂) :
    h ▸ c₁ = Eq.symm h ▸ c₂ := by
  sorry

[Kevin Buzzard]

Fewer than that!

[Damiano Testa]

For the original question, this is what I think happens. Lean interprets that you have given it C a2 as the LHS. Now it tries hard to get the same on the right. But, you've told it that you want the RHS to be C a1... so it invokes the power of the black magic triangle, which allows it to recursively use rewrites and symms, inserting them where it pleases: I suspect that the rule is that there should be at least one.

So, first, it realises that you told it garbage: you cannot rewrite C a2 with h, it had better be Eq.symm h and you get to C a1. But the LHS was C a2, so let's rewrite with h one more time... et voilà!

Nothing could be clearer.

[Damiano Testa]

The second question is left as an exercise.