α : Type u_1
β : Type ?u.66669
γ : Type ?u.66672
ι : Sort u_2
ι' : Sort ?u.66678
f : ι → α
s t : Set α
p : ↑(range f) → Prop
x✝ : ∃ a, p a
i : ι
ha : p { val := f i, property := (_ : ∃ y, f y = f i) }
⊢ ∃ i, p { val := f i, property := (_ : f i ∈ range f) }
α : Type u_1
β : Type ?u.66669
γ : Type ?u.66672
ι : Sort u_2
ι' : Sort ?u.66678
f : ι → α
s t : Set α
p : ↑(range f) → Prop
x✝ : ∃ a, p a
a : α
i : ι
hi : f i = a
ha : p { val := a, property := (_ : ∃ y, f y = a) }
⊢ ∃ i, p { val := f i, property := (_ : f i ∈ range f) }
subst a
no goals
α : Type u_1
β : Type ?u.66669
γ : Type ?u.66672
ι : Sort u_2
ι' : Sort ?u.66678
f : ι → α
s t : Set α
p : ↑(range f) → Prop
x✝ : ∃ a, p a
i : ι
ha : p { val := f i, property := (_ : ∃ y, f y = f i) }
⊢ ∃ i, p { val := f i, property := (_ : f i ∈ range f) }
exact ⟨i, ha⟩