le and lt is the same as lt

Stream: Is there code for X?

[Eric Paul]

Is there some single theorem or tactic that can solve this in one go?

import Mathlib

theorem test [LinearOrder α] {a b : α} : a ≤ b ∧ a < b ↔ a < b := by
    constructor
    · rintro ⟨-, this⟩
      exact this
    · intro h
      exact ⟨h.le, h⟩

None of tauto, aesop, and exact? worked for me.

[Yaël Dillies]

I'm pretty sure simp does it, or maybe simp [le_of_lt] (sorry, I don't have Lean open right now)

[Eric Paul]

Strangely enough that leaves the goal as a < b → a ≤ b

[Damiano Testa]

Try

  simp (config := {contextual := true}) [le_of_lt]

[Eric Paul]

That works thank you!

And thanks to the new language reference I was able to easily read about the simp configurations which is cool