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

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

Tactic:
exact csInf_singleton 0

Result:
no goals

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

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

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

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

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

Tactic:
exact ((OrderIso.smulRightDual ℝ ha').map_csSup' hs h).symm

Result:
no goals

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

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

Result:
no goals

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

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

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

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

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

Tactic:
by_cases h : BddAbove s

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

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

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

Tactic:
rw [zero_smul_set hs, zero_smul]

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

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

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

Result:
no goals