congr' in Lean 4

Stream: lean4

[Bhavik Mehta]

Is there a replacement to Lean 3 congr' in Lean 4? docs#congr doesn't look inside iff goals, seemingly
Lean 3:

import tactic.congr

example {V K : Type} {P : Π (V : Type), (K → nat) → Prop} {n n' : K → nat} : P V n ↔ P V n' :=
begin
  congr' 2,
  show n = n', --works
end

Lean 4:

example {V K : Type} {P : (V : Type) → (K → Nat) → Prop} {n n' : K → Nat} : P V n ↔ P V n' := by
  congr 2
  show n = n' -- error

[Mauricio Collares]

Did you try congr!?

[Bhavik Mehta]

It seems to go too far, like Lean 3 rcongr - it starts using ext lemmas where I didn't want to

[Bhavik Mehta]

Ah, congr' 2 apparently corresponds to congr! 1, got it. Thanks!

[Kyle Miller]

Yeah, mathlib4's congr! is meant to be an analogue for mathlib3's congr'. Unlike rcongr it doesn't use ext lemmas (though it does know about funext and it does intro for you, and you can give congr! a with clause to name introduced variables).

[Bhavik Mehta]

Right, it was the fact that it uses ext on functions and does intro (both of which mathlib3 congr' don't do) that made my life difficult here :)