# `rsuffices` tactic #

The `rsuffices` tactic is an alternative version of `suffices`, that allows the usage of any syntax that would be valid in an `obtain` block. This tactic just calls `obtain` on the expression, and then `rotate_left`.

source
def Mathlib.Tactic.rsuffices :
Lean.ParserDescr

The `rsuffices` tactic is an alternative version of `suffices`, that allows the usage of any syntax that would be valid in an `obtain` block. This tactic just calls `obtain` on the expression, and then `rotate_left`.

Equations

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

Instances For