mathlib3 documentation

tactic.simpa

This is a "finishing" tactic modification of simp. It has two forms.

  • simpa [rules, ...] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

    Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

  • simpa [rules, ...] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.

This is a "finishing" tactic modification of simp. It has two forms.

  • simpa [rules, ...] using e will simplify the goal and the type of e using rules, then try to close the goal using e.

    Simplifying the type of e makes it more likely to match the goal (which has also been simplified). This construction also tends to be more robust under changes to the simp lemma set.

  • simpa [rules, ...] will simplify the goal and the type of a hypothesis this if present in the context, then try to close the goal using the assumption tactic.