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

State before:
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
s : Set α
⊢ image (g ∘ f) s = image g (image f s)
Tactic:
ext
State after:
case h
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
s : Set α
x✝ : γ
⊢ x✝ ∈ image (g ∘ f) s ↔ x✝ ∈ image g (image f s)

State before:
case h
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
s : Set α
x✝ : γ
⊢ x✝ ∈ image (g ∘ f) s ↔ x✝ ∈ image g (image f s)
Tactic:
unfold image
State after:
case h
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
s : Set α
x✝ : γ
⊢ x✝ ∈ {x | ∃ a, a ∈ s ∧ (g ∘ f) a = x} ↔ x✝ ∈ {x | ∃ a, a ∈ {x | ∃ a, a ∈ s ∧ f a = x} ∧ g a = x}

State before:
case h
β : Type u_1
γ : Type u_2
α : Type u_3
g : β → γ
f : α → β
s : Set α
x✝ : γ
⊢ x✝ ∈ {x | ∃ a, a ∈ s ∧ (g ∘ f) a = x} ↔ x✝ ∈ {x | ∃ a, a ∈ {x | ∃ a, a ∈ s ∧ f a = x} ∧ g a = x}
Tactic:
aesop
State after:
no goals