congr gets stuck on bundled homs

Stream: general

[Eric Wieser]

What's going on here?

import algebra.direct_sum.basic

lemma of_congr {ι} [decidable_eq ι] (A : ι → Type*) [Π i, add_comm_monoid (A i)]
  (i j : ι) (xi : A i) (xj : A j) (h : i = j)
  (h' : xi == xj) : direct_sum.of A i xi = direct_sum.of A j xj :=
begin
  -- doesn't work without this line
  dsimp only [direct_sum.of, dfinsupp.single_add_hom_apply],
  congr,
  assumption,
  assumption
end

is it possible to write a @[congr] lemma such that lean doesn't need the dsimp?

[Reid Barton]

Does congr care about [congr] lemmas?

[Gabriel Ebner]

AFAIK not.

[Eric Wieser]

Ah, then this is sort of an #xy, as my actual problem was that simp wasn't able to simplify the express for i due to the dependent type in xi

[Eric Wieser]

I'm guessing we don't have much documentation for attr#congr (that link doesn't work)

[Reid Barton]

Right, simp does care about [congr] lemmas

[Eric Wieser]

Is there any way for me to teach congr about this case, if [congr] isn't the way?

[Eric Wieser]

If not, and if simp also can't be taught, then maybe we need to unbundled direct_sum.of

[Reid Barton]

We can already tell this was an #xy question because it uses heq

[Gabriel Ebner]

@[congr] is the way, but the teaching involves changing the congr tactic which is in core Lean.

[Eric Wieser]

Does congr' understand @[congr], and is it implemented in a way that we wouldn't need to modify core?

[Gabriel Ebner]

Yes, you could also just change it in congr'. That can be done inside mathlib.

[Eric Wieser]

There's the separate problem here though that I can't work out how to even declare something that @[congr] accepts here