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

State before:
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ image f {x} = {f x}
Tactic:
ext x
State after:
case h
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ image f {x✝} ↔ x ∈ {f x✝}

State before:
case h
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ image f {x✝} ↔ x ∈ {f x✝}
Tactic:
constructor
State after:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ image f {x✝} → x ∈ {f x✝}

case h.mpr
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ {f x✝} → x ∈ image f {x✝}

State before:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ image f {x✝} → x ∈ {f x✝}
Tactic:
rintro ⟨_, rfl, rfl⟩
State after:
case h.mp.intro.intro
α : Type u_1
β : Type u_2
f : α → β
w✝ : α
⊢ f w✝ ∈ {f w✝}

State before:
case h.mp.intro.intro
α : Type u_1
β : Type u_2
f : α → β
w✝ : α
⊢ f w✝ ∈ {f w✝}
Tactic:
rfl
State after:
no goals

State before:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
x✝ : α
x : β
⊢ x ∈ {f x✝} → x ∈ image f {x✝}
Tactic:
rintro rfl
State after:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ f x ∈ image f {x}

State before:
case h.mpr
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ f x ∈ image f {x}
Tactic:
exact ⟨x, rfl, rfl⟩
State after:
no goals