no goals
α : Type u_1
β : Type u_2
γ : Type ?u.113229
ι : Sort ?u.113232
π : α → Type ?u.113237
fa : α → α
fb : β → β
f : α → β
g : β → γ
s✝ t✝ : Set α
h : Semiconj f fa fb
s t : Set β
hb : MapsTo fb s t
x : α
hx : x ∈ f ⁻¹' s
⊢ fa x ∈ f ⁻¹' t
simp only [mem_preimage, h x, hb hx]