case a
α : Type u_1
β : Type u_2
γ : Type ?u.70019
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
a✝ : β
⊢ a✝ ∈ filter (fun y => y ∈ image f s) t ↔ a✝ ∈ image f s
α : Type u_1
β : Type u_2
γ : Type ?u.70019
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
⊢ filter (fun y => y ∈ image f s) t = image f s
ext
case a
α : Type u_1
β : Type u_2
γ : Type ?u.70019
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
a✝ : β
⊢ ∀ (x : α), x ∈ s → f x = a✝ → a✝ ∈ t
case a
α : Type u_1
β : Type u_2
γ : Type ?u.70019
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
a✝ : β
⊢ a✝ ∈ filter (fun y => y ∈ image f s) t ↔ a✝ ∈ image f s
simp only [mem_filter, mem_image, decide_eq_true_eq, and_iff_right_iff_imp, forall_exists_index,
  and_imp]
case a
α : Type u_1
β : Type u_2
γ : Type ?u.70019
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
x : α
xel : x ∈ s
⊢ f x ∈ t
case a
α : Type u_1
β : Type u_2
γ : Type ?u.70019
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
a✝ : β
⊢ ∀ (x : α), x ∈ s → f x = a✝ → a✝ ∈ t
rintro x xel rfl
no goals
case a
α : Type u_1
β : Type u_2
γ : Type ?u.70019
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
f : α → β
s : Finset α
t : Finset β
h : ∀ (x : α), x ∈ s → f x ∈ t
x : α
xel : x ∈ s
⊢ f x ∈ t
exact h _ xel