Documentation

CatCryptCore.Tactics.LeOfSum

le_of_sum Tactic #

A recursive tactic for proving x ≤ a + b + c + ... goals that arise from showing a single summand is bounded by a left-associated sum. Replaces 8-line calc chains of le_add_self/le_self_add with a single call.

source
def tacticLe_of_sum :
Lean.ParserDescr

Prove x ≤ a + b + c + ... by recursively applying le_self_add and le_add_self. Handles left-associated sums of any depth.

Equations
Instances For

    congr_funext Tactic #

    Closes goals of the form C a₁ ... (fun x => f x) = C a₁ ... (fun x => g x) arising in structural induction on free-monad-like types (SPTree, RawCode, etc.).

    The typical pattern is:

    simp only [defs, ih]; congr 1; funext _; exact ih _

    This tactic replaces the congr 1; funext _; exact ih _ part.

    source
    def tacticCongr_funext :
    Lean.ParserDescr

    Close congr 1; funext _; exact ih _-shaped goals from inductive bind cases. Also handles congr 1; exact ih when no funext is needed (e.g., set cases).

    Equations
    Instances For