## Stream: general

### Topic: congr gets stuck on bundled homs

#### Eric Wieser (Dec 05 2021 at 15:33):

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
congr,
assumption,
assumption
end


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

#### Reid Barton (Dec 05 2021 at 15:52):

Does congr care about [congr] lemmas?

AFAIK not.

#### Eric Wieser (Dec 05 2021 at 15:54):

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 (Dec 05 2021 at 15:54):

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

#### Reid Barton (Dec 05 2021 at 15:54):

Right, simp does care about [congr] lemmas

#### Eric Wieser (Dec 05 2021 at 15:55):

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

#### Eric Wieser (Dec 05 2021 at 15:55):

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

#### Reid Barton (Dec 05 2021 at 15:57):

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

#### Gabriel Ebner (Dec 05 2021 at 15:57):

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

#### Eric Wieser (Dec 05 2021 at 15:59):

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

#### Gabriel Ebner (Dec 05 2021 at 16:08):

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

#### Eric Wieser (Dec 05 2021 at 16:09):

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

Last updated: Aug 03 2023 at 10:10 UTC