Function elaborating `Congr.Config`

## Instances For

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

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

.
The optional parameter is 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))`

,
`congr`

produces the goals `⊢ x = y`

and `⊢ y = x`

,
while `congr 2`

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

.

## Instances For

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

and `⊢ 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))`

,`congr`

produces the goals`⊢ x = y`

and`⊢ y = x`

, while`congr 2`

produces the intended`⊢ 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`

then`congr with x`

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

.

## Instances For

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

```
⊢ (fun x => f x + 3) '' s = (fun x => g x + 3) '' s
```

then `rcongr x`

produces the goal

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

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

.

In contrast, `congr`

would produce

```
⊢ (fun x => f x + 3) = (fun x => g x + 3)
```

and `congr with x`

(or `congr; ext x`

) would produce

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