-- Mathlib/Data/Real/Pointwise.lean
theorem Real.sInf_smul_of_nonneg (ha : 0 ≤ a) (s : Set ℝ) : sInf (a • s) = a • sInf s

Proof state:
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
⊢ sInf (a • s) = a • sInf s

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Result:
case inl
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
⊢ sInf (a • ∅) = a • sInf ∅

case inr
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
⊢ sInf (a • s) = a • sInf s

Proof state:
case neg
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddBelow s
⊢ sInf (a • s) = a • sInf s

Tactic:
rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_pos ha').1 h),
    Real.sInf_of_not_bddBelow h, smul_zero]

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : BddBelow s
⊢ sInf (a • s) = a • sInf s

Tactic:
exact ((OrderIso.smulRight ha').map_csInf' hs h).symm

Result:
no goals

Proof state:
case inr
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
⊢ sInf (a • s) = a • sInf s

Tactic:
obtain rfl | ha' := ha.eq_or_lt

Result:
case inr.inl
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sInf s

case inr.inr
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
⊢ sInf (a • s) = a • sInf s

Proof state:
case inr.inl
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf 0 = 0

Tactic:
exact csInf_singleton 0

Result:
no goals

Proof state:
case inl
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
⊢ sInf (a • ∅) = a • sInf ∅

Tactic:
rw [smul_set_empty, Real.sInf_empty, smul_zero]

Result:
no goals

Proof state:
case inr.inr
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
⊢ sInf (a • s) = a • sInf s

Tactic:
by_cases h : BddBelow s

Result:
case pos
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : BddBelow s
⊢ sInf (a • s) = a • sInf s

case neg
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
a : α
ha : 0 ≤ a
s : Set ℝ
hs : s.Nonempty
ha' : 0 < a
h : ¬BddBelow s
⊢ sInf (a • s) = a • sInf s

Proof state:
case inr.inl
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf (0 • s) = 0 • sInf s

Tactic:
rw [zero_smul_set hs, zero_smul]

Result:
case inr.inl
α : Type u_2
inst✝² : LinearOrderedField α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : OrderedSMul α ℝ
s : Set ℝ
hs : s.Nonempty
ha : 0 ≤ 0
⊢ sInf 0 = 0