Theorem: Prod.Lex.mk_min (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✝¹ : LinearOrder α
inst✝ : LinearOrder β
x : α
y₁✝ y₂✝ y₁ y₂ : β
⊢ y₁ ≤ y₂ → (fun y => (x, y)) y₁ ≤ (fun y => (x, y)) y₂
Tactic:
simp
State after:
no goals