Lean4
/-- The `rel` tactic applies "generalized congruence" rules to solve a relational goal by
"substitution". For example,
```
example {a b x c d : ℝ} (h1 : a ≤ b) (h2 : c ≤ d) :
x ^ 2 * a + c ≤ x ^ 2 * b + d := by
rel [h1, h2]
```
In this example we "substitute" the hypotheses `a ≤ b` and `c ≤ d` into the LHS `x ^ 2 * a + c` of
the goal and obtain the RHS `x ^ 2 * b + d`, thus proving the goal.
The "generalized congruence" rules used are the library lemmas which have been tagged with the
attribute `@[gcongr]`. For example, the first example constructs the proof term
```
add_le_add (mul_le_mul_of_nonneg_left h1 (pow_bit0_nonneg x 1)) h2
```
using the generalized congruence lemmas `add_le_add` and `mul_le_mul_of_nonneg_left`. If there are
no applicable generalized congruence lemmas, the tactic fails.
The tactic attempts to discharge side goals to these "generalized congruence" lemmas (such as the
side goal `0 ≤ x ^ 2` in the above application of `mul_le_mul_of_nonneg_left`) using the tactic
`gcongr_discharger`, which wraps `positivity` but can also be extended. If the side goals cannot
be discharged in this way, the tactic fails. -/
@[tactic_parser 1000]
public meta def «tacticRel[_]» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.GCongr.«tacticRel[_]» 1024
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "rel" false✝) (ParserDescr.symbol✝ " ["))
((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
Bool.false✝))
(ParserDescr.symbol✝ "]"))
