case h
α : Type u_1
β : Type u_2
γ : Type ?u.84755
ι : Sort ?u.84758
ι' : Sort ?u.84761
f : ι → α
s✝ t s : Set α
x✝ : β
⊢ x✝ ∈ Sum.inr ⁻¹' (Sum.inl '' s) ↔ x✝ ∈ ∅
α : Type u_1
β : Type u_2
γ : Type ?u.84755
ι : Sort ?u.84758
ι' : Sort ?u.84761
f : ι → α
s✝ t s : Set α
⊢ Sum.inr ⁻¹' (Sum.inl '' s) = ∅
ext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.84755
ι : Sort ?u.84758
ι' : Sort ?u.84761
f : ι → α
s✝ t s : Set α
x✝ : β
⊢ x✝ ∈ Sum.inr ⁻¹' (Sum.inl '' s) ↔ x✝ ∈ ∅
simp