implicit quantification in goal

Stream: new members

[Chris M]

I have a goal state with implicit quantification ∃ ⦃a b : ℝ⦄ as follows:

h1 : 0 ≤ 1,
h2 : -1 < 0,
h3 : -0 = 0
⊢ ∃ ⦃a b : ℝ⦄, a ≤ b ∧ -b < -a

I want to say use 0 1, but it seems that because the quantification is implicit I can't.

This is the context:

import data.real.basic
import tactic

open function

example : ¬ monotone (λ x : ℝ, -x) :=
begin
    rw monotone,
    push_neg,
    have h1: 0 ≤ 1, {exact zero_le 1},
    have h2: -(1:ℝ)  < 0, {exact neg_one_lt_zero},
    have h3: -(0:ℝ)=0, {exact neg_zero},
end

[Reid Barton]

use [0, 1]

[Chris M]

:face_palm: