Def Mathlib.Tactic.applyFunTarget

Modification history

2023-08-28 21:38
Mathlib/Tactic/ApplyFun.lean
feat: use the function to help elaborate the injectivity lemma in `apply_fun` (#6733)
Modified Mathlib.Tactic.applyFunTargetView on Github →
2023-04-22 23:19
Mathlib/Tactic/ApplyFun.lean
feat: use more function coercions in `apply_fun` (#3582) …
Modified Mathlib.Tactic.applyFunTargetView on Github →
2022-11-07 21:25
Mathlib/Tactic/ApplyFun.lean
feat: port apply_fun (#475) …
Added Mathlib.Tactic.applyFunTargetView on Github →