Theorem: max_eq_min_iff (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x = y
⊢ min x y = max x y
Tactic:
simp [h]
State after:
no goals