Theorem: Etch.Verification.Stream.le_iff_of_eq_compare (Etch/StreamFusion/Proofs/Imap.lean)

State before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h : compareOfLessAndEq a b = compareOfLessAndEq c d
⊢ a ≤ b ↔ c ≤ d
Tactic:
simp [le_iff_lt_or_eq, lt_iff_of_eq_compare h, eq_iff_of_eq_compare h]
State after:
no goals