case inl
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
⊢ sSup (a • ∅) = a • sSup ∅

case inr
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
⊢ sSup (a • s) = a • sSup s
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
⊢ sSup (a • s) = a • sSup s
obtain rfl | hs := s.eq_empty_or_nonempty
case inr.inl
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sSup s

case inr.inr
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
⊢ sSup (a • s) = a • sSup s
case inr
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
⊢ sSup (a • s) = a • sSup s
obtain rfl | ha' := ha.eq_or_lt
case pos
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : BddAbove s
⊢ sSup (a • s) = a • sSup s

case neg
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : ¬BddAbove s
⊢ sSup (a • s) = a • sSup s
case inr.inr
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
⊢ sSup (a • s) = a • sSup s
by_cases h : BddAbove s
no goals
case inl
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
⊢ sSup (a • ∅) = a • sSup ∅
rw [smul_set_empty, Real.sSup_empty, smul_zero]
case inr.inl
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sSup 0 = 0
case inr.inl
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sSup (0 • s) = 0 • sSup s
rw [zero_smul_set hs, zero_smul]
no goals
case inr.inl
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sSup 0 = 0
exact csSup_singleton 0
no goals
case pos
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : BddAbove s
⊢ sSup (a • s) = a • sSup s
exact ((OrderIso.smulLeft ℝ ha').map_csSup' hs h).symm
no goals
case neg
ι : Sort ?u.3544
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : ¬BddAbove s
⊢ sSup (a • s) = a • sSup s
rw [Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_pos ha').1 h),
    Real.sSup_of_not_bddAbove h, smul_zero]