apply function to hypothesis

Stream: mathlib4

[Jeremy Salwen]

I want to add a function call to both sides of a hypothesis. I tried apply_fun at but it seems to be picky about how you call it:

import Std.Data.List.Basic
import Mathlib.Tactic.applyFun

open Lean

lemma foo (a b: List α) (P: a = b): True := by
  apply_fun List.length at P
  -- Error: Can not use `apply_fun` with a dependently typed function.

This does work if I replace List.length with @List.length α.

II feel like the same thing could be accomplished with just a lemma, but I can't seem to find an appropriate lemma.

[Sky Wilshaw]

docs4#congr_arg might help.

[Heather Macbeth]

@Jeremy Salwen If you have time, could you check whether it worked in mathlib3? This might be an accidental loss of functionality between the mathlib3 and mathlib4 versions of apply_fun.

[Heather Macbeth]

(@Sky Wilshaw The tactic apply_fun is a wrapper for the lemma congr_arg).

[Jeremy Salwen]

@Heather Macbeth

lemma foo {α} (a b: list α) (P: a = b): a = a := by
  apply_fun list.length at P

Works in lean 3.

[Heather Macbeth]

Thanks for checking! Would you mind opening an issue:
https://github.com/leanprover-community/mathlib4/issues
with the full code snippets (including imports) which work in mathlib3 and don't work in mathlib4?

[Heather Macbeth]

And let's also ping @Scott Morrison, who it seems wrote the mathlib4 apply_fun (mathlib4#475).

[Jeremy Salwen]

@Heather Macbeth done! https://github.com/leanprover-community/mathlib4/issues/1471

[Scott Morrison]

Fixed in mathlib4#1476, although I feel like the extra work being done there perhaps should be done in core in Lean.Meta.mkCongrArg.