α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → β
H : l₁ ⊆ l₂
x : β
⊢ (∃ a, a ∈ l₁ ∧ f a = x) → ∃ a, a ∈ l₂ ∧ f a = x
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → β
H : l₁ ⊆ l₂
x : β
⊢ x ∈ map f l₁ → x ∈ map f l₂
simp only [mem_map]
no goals
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → β
H : l₁ ⊆ l₂
x : β
⊢ (∃ a, a ∈ l₁ ∧ f a = x) → ∃ a, a ∈ l₂ ∧ f a = x
exact .imp fun a => .imp_left (@H _)