case inl
α : Type u_2
β : Type u_1
γ : Type ?u.10654
ι : Sort ?u.10657
ι' : Sort ?u.10660
f : α → β
g : β → γ
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
hb : b ∈ s
⊢ (fun x => b) ⁻¹' s = univ

case inr
α : Type u_2
β : Type u_1
γ : Type ?u.10654
ι : Sort ?u.10657
ι' : Sort ?u.10660
f : α → β
g : β → γ
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
hb : ¬b ∈ s
⊢ (fun x => b) ⁻¹' s = ∅
α : Type u_2
β : Type u_1
γ : Type ?u.10654
ι : Sort ?u.10657
ι' : Sort ?u.10660
f : α → β
g : β → γ
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
⊢ (fun x => b) ⁻¹' s = if b ∈ s then univ else ∅
split_ifs with hb
no goals
case inl
α : Type u_2
β : Type u_1
γ : Type ?u.10654
ι : Sort ?u.10657
ι' : Sort ?u.10660
f : α → β
g : β → γ
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
hb : b ∈ s
⊢ (fun x => b) ⁻¹' s = univ

case inr
α : Type u_2
β : Type u_1
γ : Type ?u.10654
ι : Sort ?u.10657
ι' : Sort ?u.10660
f : α → β
g : β → γ
b : β
s : Set β
inst✝ : Decidable (b ∈ s)
hb : ¬b ∈ s
⊢ (fun x => b) ⁻¹' s = ∅
exacts [preimage_const_of_mem hb, preimage_const_of_not_mem hb]