Theorem: Set.comp_map (GMLInit/Data/Set/Basic.lean)

State before:
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
⊢ Set.map (g ∘ f) s = Set.map g (Set.map f s)
Tactic:
apply Set.ext
State after:
case a
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
⊢ ∀ (x : γ), x ∈ Set.map (g ∘ f) s ↔ x ∈ Set.map g (Set.map f s)

State before:
case a
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
⊢ ∀ (x : γ), x ∈ Set.map (g ∘ f) s ↔ x ∈ Set.map g (Set.map f s)
Tactic:
intro z
State after:
case a
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map (g ∘ f) s ↔ z ∈ Set.map g (Set.map f s)

State before:
case a
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map (g ∘ f) s ↔ z ∈ Set.map g (Set.map f s)
Tactic:
constructor
State after:
case a.mp
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map (g ∘ f) s → z ∈ Set.map g (Set.map f s)

case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map g (Set.map f s) → z ∈ Set.map (g ∘ f) s

State before:
case a.mp
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map (g ∘ f) s → z ∈ Set.map g (Set.map f s)
Tactic:
intro ⟨x, hx, hxz⟩
State after:
case a.mp
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
x : α
hx : x ∈ s
hxz : (g ∘ f) x = z
⊢ z ∈ Set.map g (Set.map f s)

State before:
case a.mp
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
x : α
hx : x ∈ s
hxz : (g ∘ f) x = z
⊢ z ∈ Set.map g (Set.map f s)
Tactic:
refine ⟨f x, ⟨x, hx, rfl⟩, hxz⟩
State after:
no goals

State before:
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
⊢ z ∈ Set.map g (Set.map f s) → z ∈ Set.map (g ∘ f) s
Tactic:
intro ⟨y, ⟨x, hx, hxy⟩, hyz⟩
State after:
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
y : β
x : α
hx : x ∈ s
hxy : f x = y
hyz : g y = z
⊢ z ∈ Set.map (g ∘ f) s

State before:
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
y : β
x : α
hx : x ∈ s
hxy : f x = y
hyz : g y = z
⊢ z ∈ Set.map (g ∘ f) s
Tactic:
refine ⟨x, hx, ?_⟩
State after:
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
y : β
x : α
hx : x ∈ s
hxy : f x = y
hyz : g y = z
⊢ (g ∘ f) x = z

State before:
case a.mpr
α : Sort u_1
β : Sort u_3
γ : Sort u_2
f : α → β
g : β → γ
s : Set α
z : γ
y : β
x : α
hx : x ∈ s
hxy : f x = y
hyz : g y = z
⊢ (g ∘ f) x = z
Tactic:
rw [←hyz, ←hxy, Function.comp_apply]
State after:
no goals