case h
α : Type u_1
β : Type u_2
γ : Type ?u.43744
δ : Type ?u.43747
ε : Type ?u.43750
ι : Type ?u.43753
f : α →. β
x✝ : α
⊢ x✝ ∈ preimage f Set.univ ↔ x✝ ∈ Dom f
α : Type u_1
β : Type u_2
γ : Type ?u.43744
δ : Type ?u.43747
ε : Type ?u.43750
ι : Type ?u.43753
f : α →. β
⊢ preimage f Set.univ = Dom f
ext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.43744
δ : Type ?u.43747
ε : Type ?u.43750
ι : Type ?u.43753
f : α →. β
x✝ : α
⊢ x✝ ∈ preimage f Set.univ ↔ x✝ ∈ Dom f
simp [mem_preimage, mem_dom]