case h
α : Type u_2
β : Type u_1
γ : Type ?u.48707
δ : Type ?u.48710
ε : Type ?u.48713
ι : Type ?u.48716
f✝ : α →. β
f : α → β
s : Set β
x : α
⊢ x ∈ core (↑f) s ↔ x ∈ f ⁻¹' s
α : Type u_2
β : Type u_1
γ : Type ?u.48707
δ : Type ?u.48710
ε : Type ?u.48713
ι : Type ?u.48716
f✝ : α →. β
f : α → β
s : Set β
⊢ core (↑f) s = f ⁻¹' s
ext x
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.48707
δ : Type ?u.48710
ε : Type ?u.48713
ι : Type ?u.48716
f✝ : α →. β
f : α → β
s : Set β
x : α
⊢ x ∈ core (↑f) s ↔ x ∈ f ⁻¹' s
simp [core_def]