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

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

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

case neg
ι : Sort ?u.200
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : ¬BddBelow s
⊢ sInf (a • s) = a • sInf s
case inr.inr
ι : Sort ?u.200
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
⊢ sInf (a • s) = a • sInf s
by_cases h : BddBelow s
no goals
case inl
ι : Sort ?u.200
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
⊢ sInf (a • ∅) = a • sInf ∅
rw [smul_set_empty, Real.sInf_empty, smul_zero]
case inr.inl
ι : Sort ?u.200
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sInf 0 = 0
case inr.inl
ι : Sort ?u.200
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sInf s
rw [zero_smul_set hs, zero_smul]
no goals
case inr.inl
ι : Sort ?u.200
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : Set.Nonempty s
ha : 0 ≤ 0
⊢ sInf 0 = 0
exact csInf_singleton 0
no goals
case pos
ι : Sort ?u.200
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : BddBelow s
⊢ sInf (a • s) = a • sInf s
exact ((OrderIso.smulLeft ℝ ha').map_csInf' hs h).symm
no goals
case neg
ι : Sort ?u.200
α : Type u_1
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : Set.Nonempty s
ha' : 0 < a
h : ¬BddBelow s
⊢ sInf (a • s) = a • sInf s
rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_pos ha').1 h),
    Real.sInf_of_not_bddBelow h, smul_zero]