Apply congruence (recursively) to goals of the form `⊢ f as = f bs⊢ f as = f bs`

and `⊢ HEq (f as) (f bs)⊢ HEq (f as) (f bs)`

.

`congr n`

controls the depth of the recursive applications. This is useful when`congr`

is too aggressive in breaking down the goal. For example, given`⊢ f (g (x + y)) = f (g (y + x))⊢ f (g (x + y)) = f (g (y + x))`

,`congr`

produces the goals`⊢ x = y⊢ x = y`

and`⊢ y = x⊢ y = x`

, while`congr 2`

produces the intended`⊢ x + y = y + x⊢ x + y = y + x`

.- If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
- You can use
`congr with p (: n)?`

to call`ext p (: n)?`

to all subgoals generated by`congr`

. For example, if the goal is`⊢ f '' s = g '' s⊢ f '' s = g '' s`

then`congr with x`

generates the goal`x : α ⊢ f x = g x⊢ f x = g x`

.

## Equations

- One or more equations did not get rendered due to their size.

partial def
Std.Tactic.rcongrCore
(g : Lean.MVarId)
(pats : List (Lean.TSyntax `rcasesPat))
(acc : Array Lean.MVarId)
:

Recursive core of `rcongr`

. Calls `ext pats <;> congr`

and then itself recursively,
unless `ext pats <;> congr`

made no progress.

Repeatedly apply `congr`

and `ext`

, using the given patterns as arguments for `ext`

.

There are two ways this tactic stops:

`congr`

fails (makes no progress), after having already applied`ext`

.`congr`

canceled out the last usage of`ext`

. In this case, the state is reverted to before the`congr`

was applied.

For example, when the goal is

```
⊢ (λ x, f x + 3) '' s = (λ x, g x + 3) '' s
⊢ (λ x, f x + 3) '' s = (λ x, g x + 3) '' s
```

then `rcongr x`

produces the goal

```
x : α ⊢ f x = g x
⊢ f x = g x
```

This gives the same result as `congr; ext x; congr`

.

In contrast, `congr`

would produce

```
⊢ (λ x, f x + 3) = (λ x, g x + 3)
⊢ (λ x, f x + 3) = (λ x, g x + 3)
```

and `congr with x`

(or `congr; ext x`

) would produce

```
x : α ⊢ f x + 3 = g x + 3
⊢ f x + 3 = g x + 3
```

## Equations

- One or more equations did not get rendered due to their size.