The generalize_proofs tactic

Generalize any proofs occurring in the goal or in chosen hypotheses, replacing them by named hypotheses so that they can be referred to later in the proof easily. Commonly useful when dealing with functions like Classical.choose that produce data from proofs.

For example:

example : List.nthLe [1, 2] 1 dec_trivial = 2 := by
  -- ⊢ [1, 2].nthLe 1 _ = 2
  generalize_proofs h,
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nthLe 1 h = 2

structure Mathlib.Tactic.GeneralizeProofs.State : Type

State for the generalize proofs tactic, contains the remaining names to be used and the list of generalizations so far

• nextIdx : List (Lean.TSyntax `Lean.binderIdent)

  The user provided names, may be anonymous

• curIdx : Array Lean.Meta.GeneralizeArg

  The generalizations made so far

@[inline, reducible]

abbrev Mathlib.Tactic.GeneralizeProofs.M (α : Type) : Type

Monad used by the generalizeProofs tactic, carries an expr cache and state with names to use and previous generalizations

Equations

• Mathlib.Tactic.GeneralizeProofs.M = Lean.MonadCacheT Lean.ExprStructEq Lean.Expr (StateRefT' IO.RealWorld Mathlib.Tactic.GeneralizeProofs.State Lean.MetaM)

partial def Mathlib.Tactic.GeneralizeProofs.visit (e : Lean.Expr) : Mathlib.Tactic.GeneralizeProofs.M Lean.Expr

Recursively generalize proofs occurring in e

def Mathlib.Tactic.GeneralizeProofs.generalizeProofs : Lean.ParserDescr

Generalize proofs in the goal, naming them with the provided list.

For example:

example : List.nthLe [1, 2] 1 dec_trivial = 2 := by
  -- ⊢ [1, 2].nthLe 1 _ = 2
  generalize_proofs h,
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nthLe 1 h = 2

Equations

• One or more equations did not get rendered due to their size.