[Merged by Bors] - feat: let apply_fun use CoeFun and dependent functions

[kmill]

Changes apply_fun to use the main function application elaborator, then uses Lean.MVarId.congrN to solve for a congruence proof. This means that apply_fun f at h should work whenever f applies to both sides of the equation h (even when coercions need to be involved).

---

[kmill]

@semorrison The TermElab monad ends up being very helpful here, and I was able to delete a lot of what I wrote. Floris mentioned Term.elabAppArgs to me today, which ends up doing most of the work. It's nice being able to use this rather than writing my own half-baked version of the elaborator!

Who would have thought apply_fun could do this?

example (f : ℤ ≃ ℤ) (a b : ℕ) (h : a = b) : True := by
  apply_fun f at h
  guard_hyp h : f a = f b -- coercions on `f`, `a`, and `b`!

[semorrison]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style