Theorem: Set.image_id (CategoryTheory/Set.lean)

State before:
α : Type u_1
s : Set α
⊢ image id s = s
Tactic:
ext
State after:
case h
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ image id s ↔ x✝ ∈ s

State before:
case h
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ image id s ↔ x✝ ∈ s
Tactic:
rw [image]
State after:
case h
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ {x | ∃ a, a ∈ s ∧ id a = x} ↔ x✝ ∈ s

State before:
case h
α : Type u_1
s : Set α
x✝ : α
⊢ x✝ ∈ {x | ∃ a, a ∈ s ∧ id a = x} ↔ x✝ ∈ s
Tactic:
simp
State after:
no goals