Def Mathlib.Tactic.applyFunHyp

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.applyFunHypView on Github →
2023-04-22 23:19
Mathlib/Tactic/ApplyFun.lean
feat: use more function coercions in `apply_fun` (#3582) …
Modified Mathlib.Tactic.applyFunHypView on Github →
2023-03-16 03:28
Mathlib/Tactic/ApplyFun.lean
feat: let `apply_fun` use `CoeFun` and dependent functions (#2890) …
Modified Mathlib.Tactic.applyFunHypView on Github →
2022-11-07 21:25
Mathlib/Tactic/ApplyFun.lean
feat: port apply_fun (#475) …
Added Mathlib.Tactic.applyFunHypView on Github →