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

State before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ max x y ≤ min x y ↔ x = y
Tactic:
have h : max x y ≤ min x y ↔ y = x := by simpa using le_antisymm_iff.symm
State after:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : max x y ≤ min x y ↔ y = x
⊢ max x y ≤ min x y ↔ x = y

State before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : max x y ≤ min x y ↔ y = x
⊢ max x y ≤ min x y ↔ x = y
Tactic:
exact h.trans eq_comm
State after:
no goals

State before:
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
inst✝ : LinearOrder α
x y : α
⊢ max x y ≤ min x y ↔ y = x
Tactic:
simpa using le_antisymm_iff.symm
State after:
no goals