case h
α : Type u_1
β : Type ?u.15405
γ : Type ?u.15408
r : Rel α β
s : Set α
x : α
⊢ x ∈ image Eq s ↔ x ∈ s
α : Type u_1
β : Type ?u.15405
γ : Type ?u.15408
r : Rel α β
s : Set α
⊢ image Eq s = s
ext x
no goals
case h
α : Type u_1
β : Type ?u.15405
γ : Type ?u.15408
r : Rel α β
s : Set α
x : α
⊢ x ∈ image Eq s ↔ x ∈ s
simp [mem_image]