bug in refine or apply_fun

Stream: mathlib4

[Yury G. Kudryashov]

This #mwe doesn't work:

import Mathlib.Tactic.ApplyFun

example : ∀ m n : ℕ, m = n → (m < 2) = (n < 2) := by
  refine fun m n h => ?_
  apply_fun (· < 2) at h

[Yury G. Kudryashov]

This #mwe works:

import Mathlib.Tactic.ApplyFun

example : ∀ m n : ℕ, m = n → (m < 2) = (n < 2) := by
  intro m n h
  apply_fun (· < 2) at h
  exact h

[Yury G. Kudryashov]

@Mario Carneiro Is this a missing withMainContext again? If yes, in which tactic?

[Yury G. Kudryashov]

How does refine fun m n h => ?_ differ from intro m n h?

[Mario Carneiro]

more like a missing instantiateMVars

[Mario Carneiro]

probably in apply_fun

[Mario Carneiro]

does it say it's not an equality?

[Mario Carneiro]

!4#2291

[Yury G. Kudryashov]

Yes. In fact, it doesn't know that h is a variable.