Close the goal `g`

using `Eq.mp v e`

,
where `v`

is a metavariable asserting that the type of `g`

and `e`

are equal.
Then call `MVarId.congrN!`

(also using local hypotheses and reflexivity) on `v`

,
and return the resulting goals.

With `symm = true`

, reverses the equality in `v`

, and uses `Eq.mpr v e`

instead.
With `depth = some n`

, calls `MVarId.congrN! n`

instead, with `n`

as the max recursion depth.

## Equations

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

## Instances For

Replaces the type of the local declaration `fvarId`

with `typeNew`

,
using `Lean.MVarId.congrN!`

to prove that the old type of `fvarId`

is equal to `typeNew`

.
Uses `Lean.MVarId.replaceLocalDecl`

to replace the type.
Returns the new goal along with the side goals generated by `congrN!`

.

With `symm = true`

, reverses the equality,
changing the goal to prove `typeNew`

is equal to `typeOld`

.
With `depth = some n`

, calls `MVarId.congrN! n`

instead, with `n`

as the max recursion depth.

## Equations

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

## Instances For

The `exact e`

and `refine e`

tactics require a term `e`

whose type is
definitionally equal to the goal. `convert e`

is similar to `refine e`

,
but the type of `e`

is not required to exactly match the
goal. Instead, new goals are created for differences between the type
of `e`

and the goal using the same strategies as the `congr!`

tactic.
For example, in the proof state

```
n : ℕ,
e : Prime (2 * n + 1)
⊢ Prime (n + n + 1)
```

the tactic `convert e using 2`

will change the goal to

```
⊢ n + n = 2 * n
```

In this example, the new goal can be solved using `ring`

.

The `using 2`

indicates it should iterate the congruence algorithm up to two times,
where `convert e`

would use an unrestricted number of iterations and lead to two
impossible goals: `⊢ HAdd.hAdd = HMul.hMul`

and `⊢ n = 2`

.

A variant configuration is `convert (config := .unfoldSameFun) e`

, which only equates function
applications for the same function (while doing so at the higher `default`

transparency).
This gives the same goal of `⊢ n + n = 2 * n`

without needing `using 2`

.

The `convert`

tactic applies congruence lemmas eagerly before reducing,
therefore it can fail in cases where `exact`

succeeds:

```
def p (n : ℕ) := True
example (h : p 0) : p 1 := by exact h -- succeeds
example (h : p 0) : p 1 := by convert h -- fails, with leftover goal `1 = 0`
```

Limiting the depth of recursion can help with this. For example, `convert h using 1`

will work
in this case.

The syntax `convert ← e`

will reverse the direction of the new goals
(producing `⊢ 2 * n = n + n`

in this example).

Internally, `convert e`

works by creating a new goal asserting that
the goal equals the type of `e`

, then simplifying it using
`congr!`

. The syntax `convert e using n`

can be used to control the
depth of matching (like `congr! n`

). In the example, `convert e using 1`

would produce a new goal `⊢ n + n + 1 = 2 * n + 1`

.

Refer to the `congr!`

tactic to understand the congruence operations. One of its many
features is that if `x y : t`

and an instance `Subsingleton t`

is in scope,
then any goals of the form `x = y`

are solved automatically.

Like `congr!`

, `convert`

takes an optional `with`

clause of `rintro`

patterns,
for example `convert e using n with x y z`

.

The `convert`

tactic also takes a configuration option, for example

```
convert (config := {transparency := .default}) h
```

These are passed to `congr!`

. See `Congr!.Config`

for options.

## Equations

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

## Instances For

Elaborates `term`

ensuring the expected type, allowing stuck metavariables.
Returns stuck metavariables as additional goals.

## Equations

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

## Instances For

The `convert_to`

tactic is for changing the type of the target or a local hypothesis,
but unlike the `change`

tactic it will generate equality proof obligations using `congr!`

to resolve discrepancies.

`convert_to ty`

changes the target to`ty`

`convert_to ty using n`

uses`congr! n`

instead of`congr! 1`

`convert_to ty at h`

changes the type of the local hypothesis`h`

to`ty`

. Any remaining`congr!`

goals come first.

Operating on the target, the tactic `convert_to ty using n`

is the same as `convert (?_ : ty) using n`

.
The difference is that `convert_to`

takes a type but `convert`

takes a proof term.

Except for it also being able to operate on local hypotheses,
the syntax for `convert_to`

is the same as for `convert`

, and it has variations such as
`convert_to ← g`

and `convert_to (config := {transparency := .default}) g`

.

Note that `convert_to ty at h`

may leave a copy of `h`

if a later local hypotheses or the target
depends on it, just like in `rw`

or `simp`

.

## Equations

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

## Instances For

`ac_change g using n`

is `convert_to g using n`

followed by `ac_rfl`

. It is useful for
rearranging/reassociating e.g. sums:

```
example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
ac_change a + d + e + f + c + g + b ≤ _
-- ⊢ a + d + e + f + c + g + b ≤ N
```

## Equations

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