rw [Set.mem_Ioo]
s : ℝ
h : ∃ a b c d, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ s = a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
⊢ s ∈ solution_set
s : ℝ
h : ∃ a b c d, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧ s = a / (a + b + d) + b / (a + b + c) + c / (b + c + d) + d / (a + c + d)
⊢ 1 < s ∧ s < 2