Strange behavior of congr tactic

Stream: lean4

[Yuval Filmus]

Consider the following code:

example {n m : Nat} (h : m = 1) :
  n / 1 = n / m := by
  congr
  simp [h]

This doesn't compile (on 4.15.0-rc1) since congr creates a duplicate goal.
If I change it to congr 1 then it compiles correctly.
What is going on here?

[Kyle Miller]

It's going deep into the OfNat expression. You can get a hint of what's going on by doing congr 2 (congr 3 is what congr itself does).

The Mathlib congr! tactic avoids this issue.

[Kyle Miller]

(In any case, there's no problem with congr creating duplicate goals. That just means you have to prove the goal multiple times.)