Theorem: Prod.Lex.mk_snd_mono_le_iff (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝² : Monad m
α : Type u_1
β : Type u_2
r₁ : α → α → Prop
r₂ : β → β → Prop
inst✝¹ : PartialOrder α
inst✝ : Preorder β
x₁ x₂ : α
y : β
⊢ (x₁, y) ≤ (x₂, y) ↔ x₁ ≤ x₂
Tactic:
simp [le_iff'']
State after:
no goals