Congr, but with more control?

Stream: new members

[Arnoud van der Leer]

In UniMath, we have a lemma maponpaths, that takes a function f and an equality a = b, and returns f a = f b. How is such functionality implemented in lean?
From Mathematics In Lean, I gathered that there is a congr tactic, but it seems that I have no control over which "function" is applied. For example,

⊢ (stdSimplex.map (SimplexCategory.δ 1) ≫ hom_inv_id) ≫ g =
  (stdSimplex.map ((SimplexCategory.σ 0).op.unop ≫ (SimplexCategory.δ 1).op.unop) ≫ hom) ≫ g

I want to remove the ≫ g part on both sides. But if I use congr, I get 4 new goals:

⊢ 1 + 1 = 1
⊢ 1 + 1 = 1
⊢ SimplexCategory.δ 1 ≍ (SimplexCategory.σ 0).op.unop ≫ (SimplexCategory.δ 1).op.unop
⊢ hom_inv_id ≍ hom

Is there a tactic or lemma version of congr that provides more control?

[Yaël Dillies]

docs#congr_arg is the exact thing you ask for

[Arnoud van der Leer]

Ah, right. Thanks! ^^

[Yaël Dillies]

But a more general option would to use congr(f $h) where h : a = b

[Arnoud van der Leer]

Can you give an example of how you'd use the congr tactic here?

[Jakub Nowak]

congr converts f a_1 ... a_n = g b_1 ... b_n to goals f = g, a_1 = b_1, ..., a_n = b_n. You can use congr 1 to get two goals: f a_1 ... a_{n-1} = g b_1 ... b_{n-1} and a_n = b_n. You didn't provide an #mwe but I'm guessing you probably want to use congr 1 or congr 2.

[Weiyi Wang]

you can also do things like congrm constant + ?_ + $h for a goal constant + a + b = constant + c + d. ?_ creates a new subgoal a = c. $h plugs in an existing hypothesis h: b = d

[Arnoud van der Leer]

Thanks! That gives a lot of good options

[Yaël Dillies]

Arnoud van der Leer said:

Can you give an example of how you'd use the congr tactic here?

I would do something like congr 1, or whatever small number makes it most useful

[Mirek Olšák]

Weiyi Wang said:

you can also do things like congrm constant + ?_ + $h for a goal constant + a + b = constant + c + d. ?_ creates a new subgoal a = c. $h plugs in an existing hypothesis h: b = d

And congrm? as an interactive version (filling the pattern automatically by user's click).

[Arnoud van der Leer]

That is really useful!