Unexpected behaviour

Stream: new members

[Maris Ozols]

I'm doing an exercise from the "Mathematics in Lean" book and run into a problem:

import Mathlib.Data.Real.Basic

example : ¬∀ {f : ℝ → ℝ}, Monotone f → ∀ {a b}, f a ≤ f b → a ≤ b := by
  intro h
  let f := fun x : ℝ ↦ (0 : ℝ)
  have monof : Monotone f := by
    intro x y _
    dsimp [f]
    norm_num
  have h' : f 1 ≤ f 0 := le_refl _
  apply h at monof
  apply monof at h'
  sorry

I was expecting the last command to produce h' : 1 ≤ 0 but it produced h' : ?a ≤ ?b. Any explanations for this? I'm not familiar with synthetic holes yet.

[Johan Commelin]

Hmm, that's a bit annoying. But apply @monof 1 0 at h' works.