case intro.intro
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
y x : α
hx : x ∈ s
hxy : (fun x => a • x) x ≤ y
⊢ y ∈ a • s
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
⊢ IsUpperSet (a • s)
rintro _ y hxy ⟨x, hx, rfl⟩
no goals
case intro.intro
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
hs : IsUpperSet s
y x : α
hx : x ∈ s
hxy : (fun x => a • x) x ≤ y
⊢ y ∈ a • s
exact mem_smul_set_iff_inv_smul_mem.2 (hs (le_inv_mul_iff_mul_le.2 hxy) hx)