# Documentation

Mathlib.Tactic.NormCast.Tactic

Prove a = b using the given simp set.

Instances For

Prove a = b by simplifying using move and squash lemmas.

Instances For
Instances For
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

Instances For

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

TODO: normCast takes a list of expressions to use as lemmas for the discharger TODO: a tactic to print the results the discharger fails to prove

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.

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.

Instances For

The core simplification routine of normCast.

Instances For
Instances For
Instances For
Instances For
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.

Instances For

Normalize casts at the given locations by moving them "upwards".

Instances For

Rewrite with the given rules and normalize casts between steps.

Instances For

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

Instances For

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

Instances For
Instances For
Instances For
Instances For
Instances For