congr'

Stream: mathlib4

[Patrick Massot]

Mathport is translating congr' to congr so I thought the Lean 4 congr was meant to be as good as congr', but compare:

import data.set.basic

example (α β : Type) (R : set (α × β)) (a : α) (b c : β) :
   (a, b) ∈ R  ↔ (a, c)  ∈ R :=
begin
 congr',
 sorry
end

which works with

import Mathlib.Data.Set.Basic

example (α β : Type) (R : Set (α × β)) (a : α) (b c : β) :
   (a, b) ∈ R  ↔ (a, c)  ∈ R := by
 congr
 sorry

which doesn't.

[Kyle Miller]

It probably should translate congr' to congr!

[Patrick Massot]

Indeed congr! is good enough. Thanks!