no goals
α : Type u_1
β : Type u_2
γ : Type ?u.33320
δ : Type ?u.33323
e : LocalEquiv α β
e' : LocalEquiv β γ
s : Set α
x : α
hx : x ∈ e.source
⊢ x ∈ ↑e ⁻¹' (↑(LocalEquiv.symm e) ⁻¹' s) ↔ x ∈ s
simp only [mem_preimage, e.left_inv hx]