case inl
X : Type u_1
Y : Type u_2
Z : Type ?u.5782
α : Type ?u.5785
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : IsEmpty X
⊢ ∃ y, f = Function.const X y

case inr
X : Type u_1
Y : Type u_2
Z : Type ?u.5782
α : Type ?u.5785
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : Nonempty X
⊢ ∃ y, f = Function.const X y
X : Type u_1
Y : Type u_2
Z : Type ?u.5782
α : Type ?u.5785
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
⊢ ∃ y, f = Function.const X y
cases' isEmpty_or_nonempty X with h h
no goals
case inl
X : Type u_1
Y : Type u_2
Z : Type ?u.5782
α : Type ?u.5785
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : IsEmpty X
⊢ ∃ y, f = Function.const X y
exact ⟨Classical.arbitrary Y, funext <| h.elim⟩
no goals
case inr
X : Type u_1
Y : Type u_2
Z : Type ?u.5782
α : Type ?u.5785
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
h : Nonempty X
⊢ ∃ y, f = Function.const X y
exact ⟨f (Classical.arbitrary X), hf.eq_const _⟩