Lean4
/-- The `simp_intro` tactic is a combination of `simp` and `intro`: it will simplify the types of
variables as it introduces them and uses the new variables to simplify later arguments
and the goal.
* `simp_intro x y z` introduces variables named `x y z`
* `simp_intro x y z ..` introduces variables named `x y z` and then keeps introducing `_` binders
* `simp_intro (config := cfg) (discharger := tac) x y .. only [h₁, h₂]`:
`simp_intro` takes the same options as `simp` (see `simp`)
```
example : x + 0 = y → x = z := by
simp_intro h
-- h: x = y ⊢ y = z
sorry
```
-/
@[tactic_parser 1000]
public meta def «tacticSimp_intro_____..Only_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.«tacticSimp_intro_____..Only_» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "simp_intro" false✝)
Lean.Parser.Tactic.optConfig)
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.discharger))
(ParserDescr.unary✝ `many
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
Lean.binderIdent)))
(ParserDescr.unary✝ `optional (ParserDescr.symbol✝ " ..")))
(ParserDescr.unary✝ `optional ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) " only" false✝)))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.simpArgs))
