case inl
ι : Type ?u.190062
α : Type u_1
β : Type ?u.190068
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
s : Set α
ha✝ : 0 ≤ a
hs : IsLUB s b
ha : 0 < a
⊢ IsLUB ((fun b => a * b) '' s) (a * b)

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