α : Type u_1
β : Type ?u.63927
γ : Type ?u.63930
ι : Sort u_2
ι' : Sort ?u.63936
f : ι → α
s t : Set α
p : ↑(range f) → Prop
H : ∀ (i : ι), p { val := f i, property := (_ : f i ∈ range f) }
x✝ : ↑(range f)
i : ι
⊢ p { val := f i, property := (_ : ∃ y, f y = f i) }
α : Type u_1
β : Type ?u.63927
γ : Type ?u.63930
ι : Sort u_2
ι' : Sort ?u.63936
f : ι → α
s t : Set α
p : ↑(range f) → Prop
H : ∀ (i : ι), p { val := f i, property := (_ : f i ∈ range f) }
x✝ : ↑(range f)
y : α
i : ι
hi : f i = y
⊢ p { val := y, property := (_ : ∃ y_1, f y_1 = y) }
subst hi
no goals
α : Type u_1
β : Type ?u.63927
γ : Type ?u.63930
ι : Sort u_2
ι' : Sort ?u.63936
f : ι → α
s t : Set α
p : ↑(range f) → Prop
H : ∀ (i : ι), p { val := f i, property := (_ : f i ∈ range f) }
x✝ : ↑(range f)
i : ι
⊢ p { val := f i, property := (_ : ∃ y, f y = f i) }
apply H