α : Type u_2
β : Type u_3
γ : Type ?u.193360
ι : Sort u_1
ι' : Sort ?u.193366
ι₂ : Sort ?u.193369
κ : ι → Sort ?u.193374
κ₁ : ι → Sort ?u.193379
κ₂ : ι → Sort ?u.193384
κ' : ι' → Sort ?u.193389
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
y : β
hy : y ∈ t
⊢ y ∈ f '' ⋂ (i : ι), s i
α : Type u_2
β : Type u_3
γ : Type ?u.193360
ι : Sort u_1
ι' : Sort ?u.193366
ι₂ : Sort ?u.193369
κ : ι → Sort ?u.193374
κ₁ : ι → Sort ?u.193379
κ₂ : ι → Sort ?u.193384
κ' : ι' → Sort ?u.193389
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
⊢ SurjOn f (⋂ (i : ι), s i) t
intro y hy
α : Type u_2
β : Type u_3
γ : Type ?u.193360
ι : Sort u_1
ι' : Sort ?u.193366
ι₂ : Sort ?u.193369
κ : ι → Sort ?u.193374
κ₁ : ι → Sort ?u.193379
κ₂ : ι → Sort ?u.193384
κ' : ι' → Sort ?u.193389
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
y : β
hy : y ∈ t
⊢ ∀ (i : ι), y ∈ f '' s i
α : Type u_2
β : Type u_3
γ : Type ?u.193360
ι : Sort u_1
ι' : Sort ?u.193366
ι₂ : Sort ?u.193369
κ : ι → Sort ?u.193374
κ₁ : ι → Sort ?u.193379
κ₂ : ι → Sort ?u.193384
κ' : ι' → Sort ?u.193389
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
y : β
hy : y ∈ t
⊢ y ∈ f '' ⋂ (i : ι), s i
rw [Hinj.image_iInter_eq, mem_iInter]
no goals
α : Type u_2
β : Type u_3
γ : Type ?u.193360
ι : Sort u_1
ι' : Sort ?u.193366
ι₂ : Sort ?u.193369
κ : ι → Sort ?u.193374
κ₁ : ι → Sort ?u.193379
κ₂ : ι → Sort ?u.193384
κ' : ι' → Sort ?u.193389
inst✝ : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
y : β
hy : y ∈ t
⊢ ∀ (i : ι), y ∈ f '' s i
exact fun i => H i hy