Lean4
/-- The `gcongr` tactic applies "generalized congruence" rules, reducing a relational goal
between a LHS and RHS. For example,
```
example {a b x c d : ℝ} (h1 : a + 1 ≤ b + 1) (h2 : c + 2 ≤ d + 2) :
x ^ 2 * a + c ≤ x ^ 2 * b + d := by
gcongr
· linarith
· linarith
```
This example has the goal of proving the relation `≤` between a LHS and RHS both of the pattern
```
x ^ 2 * ?_ + ?_
```
(with inputs `a`, `c` on the left and `b`, `d` on the right); after the use of
`gcongr`, we have the simpler goals `a ≤ b` and `c ≤ d`.
A depth limit or a pattern can be provided explicitly;
this is useful if a non-maximal match is desired:
```
example {a b c d x : ℝ} (h : a + c + 1 ≤ b + d + 1) :
x ^ 2 * (a + c) + 5 ≤ x ^ 2 * (b + d) + 5 := by
gcongr x ^ 2 * ?_ + 5 -- or `gcongr 2`
linarith
```
The "generalized congruence" rules 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 ?_ (Even.pow_nonneg (even_two_mul 1) x)) ?_
```
using the generalized congruence lemmas `add_le_add` and `mul_le_mul_of_nonneg_left`.
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. Side goals not discharged
in this way are left for the user.
`gcongr` will descend into binders (for example sums or suprema). To name the bound variables,
use `with`:
```
example {f g : ℕ → ℝ≥0∞} (h : ∀ n, f n ≤ g n) : ⨆ n, f n ≤ ⨆ n, g n := by
gcongr with i
exact h i
```
-/
@[tactic_parser 1000]
public meta def tacticGcongr___With___ : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.GCongr.tacticGcongr___With___ 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "gcongr" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
(ParserDescr.cat✝ `term 0))))
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with")
(ParserDescr.unary✝ `many1
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
Lean.binderIdent)))))
