case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.111397
ι : Sort ?u.111400
π : α → Type ?u.111405
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxt : x ∈ t
⊢ f x ∈ fb '' (f '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.111397
ι : Sort ?u.111400
π : α → Type ?u.111405
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
⊢ SurjOn fb (f '' s) (f '' t)
rintro y ⟨x, hxt, rfl⟩
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.111397
ι : Sort ?u.111400
π : α → Type ?u.111405
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ f (fa x) ∈ fb '' (f '' s)
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.111397
ι : Sort ?u.111400
π : α → Type ?u.111405
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxt : x ∈ t
⊢ f x ∈ fb '' (f '' s)
rcases ha hxt with ⟨x, hxs, rfl⟩
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.111397
ι : Sort ?u.111400
π : α → Type ?u.111405
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' (f '' s)
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.111397
ι : Sort ?u.111400
π : α → Type ?u.111405
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ f (fa x) ∈ fb '' (f '' s)
rw [h x]
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.111397
ι : Sort ?u.111400
π : α → Type ?u.111405
fa : α → α
fb : β → β
f : α → β
g : β → γ
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' (f '' s)
exact mem_image_of_mem _ (mem_image_of_mem _ hxs)