case inl.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.24519
α : Type ?u.24522
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
x : X
⊢ ∃ y, f = const X y

case inr
X : Type u_1
Y : Type u_2
Z : Type ?u.24519
α : Type ?u.24522
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
hX : ¬Nonempty X
⊢ ∃ y, f = const X y
X : Type u_1
Y : Type u_2
Z : Type ?u.24519
α : Type ?u.24522
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
⊢ ∃ y, f = const X y
rcases Classical.em (Nonempty X) with (⟨⟨x⟩⟩ | hX)
no goals
case inl.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.24519
α : Type ?u.24522
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
x : X
⊢ ∃ y, f = const X y
exact ⟨f x, f.eq_const x⟩
no goals
case inr
X : Type u_1
Y : Type u_2
Z : Type ?u.24519
α : Type ?u.24522
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
hX : ¬Nonempty X
⊢ ∃ y, f = const X y
exact ⟨Classical.arbitrary Y, ext fun x => (hX ⟨x⟩).elim⟩