exact hy' hy''
case mp.intro.intro
G : Type
inst✝¹ : Group G
X : Type u_1
Y : Type u_2
inst✝ : PartialOrder X
f : Y → X
hf : Function.Injective f
s : Set Y
y : Y
hy : isInf (f '' s) (f y)
y' : Y
hy' : y' ∈ lowerBounds s
x : X
y'' : Y
hy'' : y'' ∈ s
H : f y'' = x
⊢ f y' ≤ f y''
no goals