Lean4
/-- `generalize_proofs ids* [at locs]?` generalizes proofs in the current goal,
turning them into new local hypotheses.
- `generalize_proofs` generalizes proofs in the target.
- `generalize_proofs at h₁ h₂` generalized proofs in hypotheses `h₁` and `h₂`.
- `generalize_proofs at *` generalizes proofs in the entire local context.
- `generalize_proofs pf₁ pf₂ pf₃` uses names `pf₁`, `pf₂`, and `pf₃` for the generalized proofs.
These can be `_` to not name proofs.
If a proof is already present in the local context, it will use that rather than create a new
local hypothesis.
When doing `generalize_proofs at h`, if `h` is a let binding, its value is cleared,
and furthermore if `h` duplicates a preceding local hypothesis then it is eliminated.
The tactic is able to abstract proofs from under binders, creating universally quantified
proofs in the local context.
To disable this, use `generalize_proofs -abstract`.
The tactic is also set to recursively abstract proofs from the types of the generalized proofs.
This can be controlled with the `maxDepth` configuration option,
with `generalize_proofs (config := { maxDepth := 0 })` turning this feature off.
For example:
```lean
def List.nthLe {α} (l : List α) (n : ℕ) (_h : n < l.length) : α := sorry
example : List.nthLe [1, 2] 1 (by simp) = 2 := by
-- ⊢ [1, 2].nthLe 1 ⋯ = 2
generalize_proofs h
-- h : 1 < [1, 2].length
-- ⊢ [1, 2].nthLe 1 h = 2
```
-/
@[tactic_parser 1000]
public meta def generalizeProofsElab : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.generalizeProofsElab 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "generalize_proofs" false✝)
Lean.Parser.Tactic.optConfig)
(ParserDescr.unary✝ `many
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt)) Lean.binderIdent)))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
