Commit 2022-11-07 21:25 23409b46

View on Github →

feat: port apply_fun (#475) This will need minor additions once the tactic mono is ported, and some additional testing after Logic.Equiv.Basic and Order.Hom.Basic are ported.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Created Mathlib/Tactic/ApplyFun.lean

added def Lean.MVarId.note

added def Mathlib.Tactic.applyFunHyp

added def Mathlib.Tactic.applyFunTarget

added def Mathlib.Tactic.applyFunTargetFailure

Created test/apply_fun.lean