no goals
α : Type u_1
β : Type u_3
γ : Type u_2
δ : Type ?u.49747
e : LocalEquiv α β
e'✝ : LocalEquiv β γ
e' : LocalEquiv α γ
x : α
he : x ∈ e.source
he' : x ∈ e'.source
⊢ ↑e x ∈ ↑(LocalEquiv.symm (LocalEquiv.symm (LocalEquiv.symm e))) ⁻¹' e'.source
rwa [mem_preimage, LocalEquiv.symm_symm, e.left_inv he]