Theorem: Etch.Verification.Stream.eq_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 only [compareOfLessAndEq] at h
State after:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h :
  (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if c < d then Ordering.lt else if c = d then Ordering.eq else Ordering.gt
⊢ a = b ↔ c = d

State before:
ι ι' : Type
inst✝¹ : LinearOrder ι
inst✝ : LinearOrder ι'
a b : ι
c d : ι'
h :
  (if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if c < d then Ordering.lt else if c = d then Ordering.eq else Ordering.gt
⊢ a = b ↔ c = d
Tactic:
split_ifs at h with h₁ h₂ <;> aesop
State after:
no goals