case h
α : Type u_1
β : Type u_2
γ : Type ?u.48032
δ : Type ?u.48035
ε : Type ?u.48038
ι : Type ?u.48041
f✝ : α →. β
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ core (res f s) t ↔ x ∈ sᶜ ∪ f ⁻¹' t
α : Type u_1
β : Type u_2
γ : Type ?u.48032
δ : Type ?u.48035
ε : Type ?u.48038
ι : Type ?u.48041
f✝ : α →. β
f : α → β
s : Set α
t : Set β
⊢ core (res f s) t = sᶜ ∪ f ⁻¹' t
ext x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.48032
δ : Type ?u.48035
ε : Type ?u.48038
ι : Type ?u.48041
f✝ : α →. β
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
case h
α : Type u_1
β : Type u_2
γ : Type ?u.48032
δ : Type ?u.48035
ε : Type ?u.48038
ι : Type ?u.48041
f✝ : α →. β
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ core (res f s) t ↔ x ∈ sᶜ ∪ f ⁻¹' t
rw [mem_core_res]
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.48032
δ : Type ?u.48035
ε : Type ?u.48038
ι : Type ?u.48041
f✝ : α →. β
f : α → β
s : Set α
t : Set β
x : α
⊢ x ∈ s → f x ∈ t ↔ x ∈ sᶜ ∪ f ⁻¹' t
by_cases h : x ∈ s <;> simp [h]