funProp tactic syntax

def Mathlib.Meta.FunProp.elabFunPropConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Config

fun_prop config elaborator

def Mathlib.Meta.FunProp.funPropTacStx : Lean.ParserDescr

fun_prop solves a goal of the form P f, where P is a predicate and f is a function, by decomposing f into a composition of elementary functions, and proving P on each of those by matching against a set of @[fun_prop] lemmas.

If fun_prop fails to solve a goal with the error "No theorems found", you can solve this issue by importing or adding new theorems tagged with the @[fun_prop] attribute. See the module documentation for Mathlib/Tactic/FunProp.lean for a detailed explanation.

• fun_prop (disch := tac) uses tac to solve potential side goals. Setting this option is required to solve ContinuousAt/On/Within goals.
• fun_prop [c, ...] will unfold the constant(s) c, ... before decomposing f.
• fun_prop (config := cfg) sets advanced configuration options using cfg : FunProp.Config (see FunProp.Config for details). These options can be combined: fun_prop (config := cfg) (disch := tac) [c]

Examples:

example : Continuous (fun x : ℝ ↦ x * sin x) := by fun_prop

-- Specify a discharger to solve `ContinuousAt`/`Within`/`On` goals:
example (y : ℝ) (hy : y ≠ 0) : ContinuousAt (fun x : ℝ ↦ 1/x) y := by
  fun_prop (disch := assumption)

example (y : ℝ) (hy : y ≠ 0) : ContinuousAt (fun x => x * (Real.log x) ^ 2 - Real.exp x / x) y := by
  fun_prop (disch := aesop)

def Mathlib.Meta.FunProp.funPropTac : Lean.Elab.Tactic.Tactic

Tactic to prove function properties

def Mathlib.Meta.FunProp.«command#print_fun_prop_theorems__» : Lean.ParserDescr

Command that prints all function properties attached to a function.

For example

#print_fun_prop_theorems HAdd.hAdd

might print out

Continuous
  continuous_add, args: [4,5], priority: 1000
  continuous_const_add, args: [5], priority: 1000
  continuous_add_const, args [4], priority: 1000
  ...
Differentiable
  Differentiable.add, args: [4,5], priority: 1000
  Differentiable.add_const, args: [4], priority: 1000
  Differentiable.const_add, args: [5], priority: 1000
  ...

You can also see only theorems about a concrete function property

#print_fun_prop_theorems HAdd.hAdd Continuous