Basic question

Stream: new members

[Takuya]

I'm just doing some exercises. I run into problem with this one:

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 a b hab
    change 0 ≤ 0
    norm_num
  have h' : f 1 ≤ f 0 := le_refl _
  have _ : 1 ≤ 0 := h monof h'
  norm_num

The problem is that the compiler don't think h monof h' is a proof of 1 ≤ 0. What's the correct way to write it?

[Aaron Liu]

Apparently you have to say "the real number one" otherwise it defaults to natural numbers

  have _ : (1 : ℝ) ≤ 0 := h monof h'