case inl
ι : Type ?u.130842
α : Type u_1
β : Type ?u.130848
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
s : Set α
ha✝ : 0 ≤ a
hs : IsGLB s b
ha : 0 < a
⊢ IsGLB ((fun b => a * b) '' s) (a * b)

case inr
ι : Type ?u.130842
α : Type u_1
β : Type ?u.130848
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun b => 0 * b) '' s) (0 * b)
ι : Type ?u.130842
α : Type u_1
β : Type ?u.130848
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b => a * b) '' s) (a * b)
rcases lt_or_eq_of_le ha with (ha | rfl)
no goals
case inl
ι : Type ?u.130842
α : Type u_1
β : Type ?u.130848
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
s : Set α
ha✝ : 0 ≤ a
hs : IsGLB s b
ha : 0 < a
⊢ IsGLB ((fun b => a * b) '' s) (a * b)
exact (OrderIso.mulLeft₀ _ ha).isGLB_image'.2 hs
case inr
ι : Type ?u.130842
α : Type u_1
β : Type ?u.130848
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun a => 0) '' s) 0
case inr
ι : Type ?u.130842
α : Type u_1
β : Type ?u.130848
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun b => 0 * b) '' s) (0 * b)
simp_rw [zero_mul]
case inr
ι : Type ?u.130842
α : Type u_1
β : Type ?u.130848
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB {0} 0
case inr
ι : Type ?u.130842
α : Type u_1
β : Type ?u.130848
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB ((fun a => 0) '' s) 0
rw [hs.nonempty.image_const]
no goals
case inr
ι : Type ?u.130842
α : Type u_1
β : Type ?u.130848
inst✝ : LinearOrderedSemifield α
b c d e : α
m n : ℤ
s : Set α
hs : IsGLB s b
ha : 0 ≤ 0
⊢ IsGLB {0} 0
exact isGLB_singleton