## Stream: new members

### Topic: le and ge not equivalent?

#### Calle Sönne (Feb 22 2019 at 21:07):

Code:

lemma test (L : ℝ) (h : L ≥ 0) (h₁ : 0 ≤ L): L < 0 :=
begin
rw le_iff_eq_or_lt at h₁,
rw le_iff_eq_or_lt at h,
end


Tactic state:

rewrite tactic failed, did not find instance of the pattern in the target expression
?m_3 ≤ ?m_4
state:
L : ℝ,
h : L ≥ 0,
h₁ : 0 = L ∨ 0 < L
⊢ L < 0


why is this happening? In my code where this originally happened I had just proved L ≥ 0 in a have statement, switching it to 0 ≤ L gave no errors as if they were the same.

#### Calle Sönne (Feb 22 2019 at 21:08):

but the test lemma seems to imply they are different?

#### Chris Hughes (Feb 22 2019 at 21:08):

rw requires syntactic equality, whereas have only requires definitional equality. For rw to work they have to look the same more or less.

#### Calle Sönne (Feb 22 2019 at 21:11):

Does simp also require syntactic equality? I switched rw into simp in code above, and it also gives an error.

so I assume yes

#### Patrick Massot (Feb 22 2019 at 21:15):

It would be easier to help if you could provide a true lemma that you'd like to prove

#### Chris Hughes (Feb 22 2019 at 21:19):

Anyway, always use le

#### Kevin Buzzard (Feb 22 2019 at 22:17):

Yes, rewrites are a great example of where definitional equality isn't good enough. I see this a lot in my code now, I don't know why. I have to use show to change my goal to something definitionally equal and then the rw works

Last updated: May 13 2021 at 16:25 UTC