congr attribute

Stream: mathlib4

[Kevin Buzzard]

In Lean 3, prod_congr {α₁ β₁ α₂ β₂ : Type*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : α₁ × β₁ ≃ α₂ × β₂ had the @[congr] attribute. In Lean 4 if I try this I get

invalid 'congr' theorem, equality expected
  ?α₁ × ?β₁ ≃ ?α₂ × ?β₂

What do I do? I'm afraid I don't know what the @[congr] tag even does.

[Mario Carneiro]

just remove the tag

[Mario Carneiro]

add a port note

[Kevin Buzzard]

is that -- port note or -- porting note or something more formal?

[Mario Carneiro]

hm, what does grep say

[Mario Carneiro]

I think porting note is more common

[Mario Carneiro]

(often, the reason this kind of thing happens because no one actually knows what it does, we are all just cargo culting the tags, and the developers also forgot and didn't bother to reimplement it)