Theorem: Set.preimage_const' (SciLean/Core/FunctionTransformations/Preimage.lean)

State before:
α : Type u_2
β : Type u_1
γ : Type ?u.57
b : β
s : Set β
⊢ (fun x => b) ⁻¹' s = if b ∈ s then univ else ∅
Tactic:
apply preimage_const
State after:
no goals