congr' vs congr

Stream: general

[Eric Wieser]

I have a goal state where congr' 3 closes the goal, but congr gives me an awful a == b goal where a and b are smul_comm_class objects. Does this mean that there's more to congr' than just " stop after n steps"?

[Eric Wieser]

The line in question is https://github.com/leanprover-community/mathlib/pull/5269/files#diff-48c4d86a6f8902ed17b9728588594da05839379ca05b4dcabc31a3999850cf65R749

[Anne Baanen]

congr doesn't always check at each subexpression if the sides of the equality are already defeq:

def const : ℕ → ℕ → ℕ := λ x _, x
example {m n : ℕ} : const 0 m = const 0 n :=
by congr -- Unsolved goals: ⊢ m = n
example {m n : ℕ} : id (const 0 m) = id (const 0 n) :=
by congr -- Succeeds

[Anne Baanen]

Not sure that that is the same thing as your issue, just something interesting I found when investigating it.

[Eric Wieser]

I don't understand what's going on in your example at all, but it's quite likely the same as my problem