Lean4
/-- `tauto` breaks down assumptions of the form `_ ∧ _`, `_ ∨ _`, `_ ↔ _` and `∃ _, _`
and splits a goal of the form `_ ∧ _`, `_ ↔ _` or `∃ _, _` until it can be discharged
using `reflexivity` or `solve_by_elim`.
This is a finishing tactic: it either closes the goal or raises an error.
The Lean 3 version of this tactic by default attempted to avoid classical reasoning
where possible. This Lean 4 version makes no such attempt. The `itauto` tactic
is designed for that purpose.
-/
@[tactic_parser 1000]
public meta def tauto : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.Tauto.tauto 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "tauto" false✝) Lean.Parser.Tactic.optConfig)
