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

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

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

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

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

State before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
⊢ z ∈ g.seq (f.seq s) → z ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s
Tactic:
intro ⟨g',hg',⟨y,⟨f',hf',⟨x,hx,hy⟩⟩,hz⟩⟩
State after:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
hz : g' y = z
⊢ z ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s

State before:
case a.mp
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
hz : g' y = z
⊢ z ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s
Tactic:
cases hz
State after:
case a.mp.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ g' y ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s

State before:
case a.mp.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ g' y ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s
Tactic:
exists (g' ∘ f')
State after:
case a.mp.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') ∈ (Set.map (fun x x_1 => x ∘ x_1) g).seq f ∧ g' y ∈ (fun f => Set.map f s) (g' ∘ f')

State before:
case a.mp.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') ∈ (Set.map (fun x x_1 => x ∘ x_1) g).seq f ∧ g' y ∈ (fun f => Set.map f s) (g' ∘ f')
Tactic:
constructor
State after:
case a.mp.refl.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') ∈ (Set.map (fun x x_1 => x ∘ x_1) g).seq f

case a.mp.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ g' y ∈ (fun f => Set.map f s) (g' ∘ f')

State before:
case a.mp.refl.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') ∈ (Set.map (fun x x_1 => x ∘ x_1) g).seq f
Tactic:
exists (g' ∘ .)
State after:
case a.mp.refl.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (fun x => g' ∘ x) ∈ Set.map (fun x x_1 => x ∘ x_1) g ∧ (g' ∘ f') ∈ (fun f_1 => Set.map f_1 f) fun x => g' ∘ x

State before:
case a.mp.refl.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (fun x => g' ∘ x) ∈ Set.map (fun x x_1 => x ∘ x_1) g ∧ (g' ∘ f') ∈ (fun f_1 => Set.map f_1 f) fun x => g' ∘ x
Tactic:
constructor
State after:
case a.mp.refl.left.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (fun x => g' ∘ x) ∈ Set.map (fun x x_1 => x ∘ x_1) g

case a.mp.refl.left.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') ∈ (fun f_1 => Set.map f_1 f) fun x => g' ∘ x

State before:
case a.mp.refl.left.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (fun x => g' ∘ x) ∈ Set.map (fun x x_1 => x ∘ x_1) g
Tactic:
exists g'
State after:
no goals

State before:
case a.mp.refl.left.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') ∈ (fun f_1 => Set.map f_1 f) fun x => g' ∘ x
Tactic:
exists f'
State after:
no goals

State before:
case a.mp.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ g' y ∈ (fun f => Set.map f s) (g' ∘ f')
Tactic:
exists x
State after:
case a.mp.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ x ∈ s ∧ (g' ∘ f') x = g' y

State before:
case a.mp.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ x ∈ s ∧ (g' ∘ f') x = g' y
Tactic:
constructor
State after:
case a.mp.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ x ∈ s

case a.mp.refl.right.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') x = g' y

State before:
case a.mp.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ x ∈ s
Tactic:
exact hx
State after:
no goals

State before:
case a.mp.refl.right.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
y : β
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hy : f' x = y
⊢ (g' ∘ f') x = g' y
Tactic:
cases hy
State after:
case a.mp.refl.right.right.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ (g' ∘ f') x = g' (f' x)

State before:
case a.mp.refl.right.right.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ (g' ∘ f') x = g' (f' x)
Tactic:
rfl
State after:
no goals

State before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
⊢ z ∈ ((Set.map (fun x x_1 => x ∘ x_1) g).seq f).seq s → z ∈ g.seq (f.seq s)
Tactic:
intro ⟨gof,⟨go,⟨g',hg',hgo⟩,⟨f',hf',hgof'⟩⟩,⟨x,hx,hz⟩⟩
State after:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
gof : α → γ
go : (α → β) → α → γ
g' : β → γ
hg' : g' ∈ g
hgo : (fun x x_1 => x ∘ x_1) g' = go
f' : α → β
hf' : f' ∈ f
hgof' : go f' = gof
x : α
hx : x ∈ s
hz : gof x = z
⊢ z ∈ g.seq (f.seq s)

State before:
case a.mpr
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
gof : α → γ
go : (α → β) → α → γ
g' : β → γ
hg' : g' ∈ g
hgo : (fun x x_1 => x ∘ x_1) g' = go
f' : α → β
hf' : f' ∈ f
hgof' : go f' = gof
x : α
hx : x ∈ s
hz : gof x = z
⊢ z ∈ g.seq (f.seq s)
Tactic:
cases hgof'
State after:
case a.mpr.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
go : (α → β) → α → γ
g' : β → γ
hg' : g' ∈ g
hgo : (fun x x_1 => x ∘ x_1) g' = go
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hz : go f' x = z
⊢ z ∈ g.seq (f.seq s)

State before:
case a.mpr.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
go : (α → β) → α → γ
g' : β → γ
hg' : g' ∈ g
hgo : (fun x x_1 => x ∘ x_1) g' = go
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hz : go f' x = z
⊢ z ∈ g.seq (f.seq s)
Tactic:
cases hgo
State after:
case a.mpr.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hz : (fun x x_1 => x ∘ x_1) g' f' x = z
⊢ z ∈ g.seq (f.seq s)

State before:
case a.mpr.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
z : γ
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
hz : (fun x x_1 => x ∘ x_1) g' f' x = z
⊢ z ∈ g.seq (f.seq s)
Tactic:
cases hz
State after:
case a.mpr.refl.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ (fun x x_1 => x ∘ x_1) g' f' x ∈ g.seq (f.seq s)

State before:
case a.mpr.refl.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ (fun x x_1 => x ∘ x_1) g' f' x ∈ g.seq (f.seq s)
Tactic:
exists g'
State after:
case a.mpr.refl.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' ∈ g ∧ (fun x x_1 => x ∘ x_1) g' f' x ∈ (fun f_1 => Set.map f_1 (f.seq s)) g'

State before:
case a.mpr.refl.refl.refl
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' ∈ g ∧ (fun x x_1 => x ∘ x_1) g' f' x ∈ (fun f_1 => Set.map f_1 (f.seq s)) g'
Tactic:
constructor
State after:
case a.mpr.refl.refl.refl.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' ∈ g

case a.mpr.refl.refl.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ (fun x x_1 => x ∘ x_1) g' f' x ∈ (fun f_1 => Set.map f_1 (f.seq s)) g'

State before:
case a.mpr.refl.refl.refl.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' ∈ g
Tactic:
exact hg'
State after:
no goals

State before:
case a.mpr.refl.refl.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ (fun x x_1 => x ∘ x_1) g' f' x ∈ (fun f_1 => Set.map f_1 (f.seq s)) g'
Tactic:
exists f' x
State after:
case a.mpr.refl.refl.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ f.seq s ∧ g' (f' x) = (fun x x_1 => x ∘ x_1) g' f' x

State before:
case a.mpr.refl.refl.refl.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ f.seq s ∧ g' (f' x) = (fun x x_1 => x ∘ x_1) g' f' x
Tactic:
constructor
State after:
case a.mpr.refl.refl.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ f.seq s

case a.mpr.refl.refl.refl.right.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' (f' x) = (fun x x_1 => x ∘ x_1) g' f' x

State before:
case a.mpr.refl.refl.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ f.seq s
Tactic:
exists f'
State after:
case a.mpr.refl.refl.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' ∈ f ∧ f' x ∈ (fun f => Set.map f s) f'

State before:
case a.mpr.refl.refl.refl.right.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' ∈ f ∧ f' x ∈ (fun f => Set.map f s) f'
Tactic:
constructor
State after:
case a.mpr.refl.refl.refl.right.left.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' ∈ f

case a.mpr.refl.refl.refl.right.left.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ (fun f => Set.map f s) f'

State before:
case a.mpr.refl.refl.refl.right.left.left
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' ∈ f
Tactic:
exact hf'
State after:
no goals

State before:
case a.mpr.refl.refl.refl.right.left.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ f' x ∈ (fun f => Set.map f s) f'
Tactic:
exists x
State after:
no goals

State before:
case a.mpr.refl.refl.refl.right.right
α : Sort u_1
β : Sort u_2
γ : Sort u_3
s : Set α
f : Set (α → β)
g : Set (β → γ)
g' : β → γ
hg' : g' ∈ g
f' : α → β
hf' : f' ∈ f
x : α
hx : x ∈ s
⊢ g' (f' x) = (fun x x_1 => x ∘ x_1) g' f' x
Tactic:
rfl
State after:
no goals