Zulip Chat Archive

Stream: new members

Topic: implicit quantification in goal


view this post on Zulip Chris M (Jul 26 2020 at 13:28):

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

view this post on Zulip Reid Barton (Jul 26 2020 at 13:30):

use [0, 1]

view this post on Zulip Chris M (Jul 26 2020 at 13:32):

:face_palm:


Last updated: May 16 2021 at 21:11 UTC