# The `norm_cast`

family of tactics. #

Prove `a = b`

using the given simp set.

## Equations

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

## Instances For

Prove `a = b`

by simplifying using move and squash lemmas.

## Equations

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

## Instances For

Construct the expression `(e : ty)`

.

## Equations

- Std.Tactic.NormCast.mkCoe e ty = do let __discr ← Lean.Meta.coerce? e ty match __discr with | Lean.LOption.some e' => pure e' | x => failure

## Instances For

Check if an expression is the coercion of some other expression, and if so return that expression.

## Equations

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

## Instances For

This is the main heuristic used alongside the elim and move lemmas. The goal is to help casts move past operators by adding intermediate casts. An expression of the shape: op (↑(x : α) : γ) (↑(y : β) : γ) is rewritten to: op (↑(↑(x : α) : β) : γ) (↑(y : β) : γ) when (↑(↑(x : α) : β) : γ) = (↑(x : α) : γ) can be proven with a squash lemma

## Equations

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

## Instances For

Discharging function used during simplification in the "squash" step.

## Equations

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

## Instances For

Core rewriting function used in the "squash" step, which moves casts upwards and eliminates them.

It tries to rewrite an expression using the elim and move lemmas. On failure, it calls the splitting procedure heuristic.

## Equations

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

## Instances For

If possible, rewrite `(n : α)`

to `(Nat.cast n : α)`

where `n`

is a numeral and `α ≠ ℕ`

.
Returns a pair of the new expression and proof that they are equal.

## Equations

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

## Instances For

The core simplification routine of `normCast`

.

## Equations

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

## Instances For

Term elaborator which uses the expected type to insert coercions.

## Equations

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

## Instances For

Implementation of the `norm_cast`

tactic when operating on the main goal.

## Equations

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

## Instances For

Implementation of the `norm_cast`

tactic when operating on a hypothesis.

## Equations

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

## Instances For

Implementation of `norm_cast`

(the full `norm_cast`

calls `trivial`

afterwards).

## Equations

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

## Instances For

`assumption_mod_cast`

runs `norm_cast`

on the goal. For each local hypothesis `h`

, it also
normalizes `h`

and tries to use that to close the goal.

## Equations

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

## Instances For

The `norm_cast`

family of tactics is used to normalize casts inside expressions.
It is basically a simp tactic with a specific set of lemmas to move casts
upwards in the expression.
Therefore it can be used more safely as a non-terminating tactic.
It also has special handling of numerals.

For instance, given an assumption

```
a b : ℤ
h : ↑a + ↑b < (10 : ℚ)
```

writing `norm_cast at h`

will turn `h`

into

```
h : a + b < 10
```

You can also use `exact_mod_cast`

, `apply_mod_cast`

, `rw_mod_cast`

or `assumption_mod_cast`

.
Writing `exact_mod_cast h`

and `apply_mod_cast h`

will normalize the goal and
`h`

before using `exact h`

or `apply h`

.
Writing `assumption_mod_cast`

will normalize the goal and for every
expression `h`

in the context it will try to normalize `h`

and use
`exact h`

.
`rw_mod_cast`

acts like the `rw`

tactic but it applies `norm_cast`

between steps.

See also `push_cast`

, for move casts inwards.

The implementation and behavior of the `norm_cast`

family is described in detail at

## Equations

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

## Instances For

Rewrite with the given rules and normalize casts between steps.

## Equations

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

## Instances For

Normalize the goal and the given expression, then close the goal with exact.

## Equations

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

## Instances For

Normalize the goal and the given expression, then apply the expression to the goal.

## Equations

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

## Instances For

`norm_cast`

tactic in `conv`

mode.

## Equations

- Std.Tactic.NormCast.convNormCast = Lean.ParserDescr.node `Std.Tactic.NormCast.convNormCast 1024 (Lean.ParserDescr.nonReservedSymbol "norm_cast" false)

## Instances For

`norm_cast`

tactic in `conv`

mode.

## Equations

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

## Instances For

`push_cast`

rewrites the expression to move casts toward the leaf nodes.
This uses `norm_cast`

lemmas in the forward direction.
For example, `↑(a + b)`

will be written to `↑a + ↑b`

.
It is equivalent to `simp only with push_cast`

.
It can also be used at hypotheses with `push_cast at h`

and with extra simp lemmas with `push_cast [int.add_zero]`

.

```
example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
((a + b : ℕ) : ℤ) = 10 :=
begin
push_cast,
push_cast at h1,
push_cast [int.add_zero] at h2,
end
```

The implementation and behavior of the `norm_cast`

family is described in detail at

## Equations

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

## Instances For

`push_cast`

rewrites the expression to move casts toward the leaf nodes.
This uses `norm_cast`

lemmas in the forward direction.
For example, `↑(a + b)`

will be written to `↑a + ↑b`

.
It is equivalent to `simp only with push_cast`

.
It can also be used at hypotheses with `push_cast at h`

and with extra simp lemmas with `push_cast [int.add_zero]`

.

```
example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
((a + b : ℕ) : ℤ) = 10 :=
begin
push_cast,
push_cast at h1,
push_cast [int.add_zero] at h2,
end
```

The implementation and behavior of the `norm_cast`

family is described in detail at

## Equations

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