mathlib3
f3cd150b - fix(tactic/apply_fun.lean): instantiate mvars in apply_fun (#14882)

Commit

3 years ago

fix(tactic/apply_fun.lean): instantiate mvars in apply_fun (#14882) Fixes leanprover-community/lean#733

Author

digama0

Parents