case inl
x y : ℝ
α : Sort u_1
h✝ : IsEmpty α
⊢ (⨅ (x : α), 0) = 0

case inr
x y : ℝ
α : Sort u_1
h✝ : Nonempty α
⊢ (⨅ (x : α), 0) = 0
x y : ℝ
α : Sort u_1
⊢ (⨅ (x : α), 0) = 0
cases isEmpty_or_nonempty α
no goals
case inl
x y : ℝ
α : Sort u_1
h✝ : IsEmpty α
⊢ (⨅ (x : α), 0) = 0
exact Real.ciInf_empty _
no goals
case inr
x y : ℝ
α : Sort u_1
h✝ : Nonempty α
⊢ (⨅ (x : α), 0) = 0
exact ciInf_const