α : Type u_1
β : Type u_2
f : α → β
l : List α
P : β → Prop
⊢ (∀ (i : β) (x : α), x ∈ l → f x = i → P i) ↔ ∀ (j : α), j ∈ l → P (f j)
α : Type u_1
β : Type u_2
f : α → β
l : List α
P : β → Prop
⊢ (∀ (i : β), i ∈ map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)
simp
no goals
α : Type u_1
β : Type u_2
f : α → β
l : List α
P : β → Prop
⊢ (∀ (i : β) (x : α), x ∈ l → f x = i → P i) ↔ ∀ (j : α), j ∈ l → P (f j)
exact ⟨fun H j h => H _ _ h rfl, fun H i x h e => e ▸ H _ h⟩