Try to apply a `simp`

congruence theorem.

## Equations

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

## Instances For

Try to apply `implies_congr`

.

## Equations

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

## Instances For

def
Lean.MVarId.congrN
(mvarId : Lean.MVarId)
(depth : optParam Nat 1000000)
(closePre : optParam Bool true)
(closePost : optParam Bool true)
:

Given a goal of the form `⊢ f as = f bs`

, `⊢ (p → q) = (p' → q')`

, or `⊢ HEq (f as) (f bs)`

, try to apply congruence.
It takes proof irrelevance into account, and the fact that `Decidable p`

is a subsingleton.

- Applies
`congr`

recursively up to depth`depth`

. - If
`closePre := true`

, it will attempt to close new goals using`Eq.refl`

,`HEq.refl`

, and`assumption`

with reducible transparency. - If
`closePost := true`

, it will try again on goals on which`congr`

failed to make progress with default transparency.

## Equations

- mvarId.congrN depth closePre closePost = do let __discr ← (Lean.MVarId.congrN.go closePre closePost depth mvarId).run #[] match __discr with | (fst, s) => pure s.toList

## Instances For

## Equations

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

## Instances For

def
Lean.MVarId.congrN.go
(closePre : optParam Bool true)
(closePost : optParam Bool true)
(n : Nat)
(mvarId : Lean.MVarId)
:

## Equations

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