no goals
α : Type u_1
β : Type u_2
γ : Type ?u.57966
δ : Type ?u.57969
e✝ : LocalEquiv α β
e'✝ : LocalEquiv β γ
e e' : LocalEquiv α β
he : e ≈ e'
s : Set β
⊢ e.source ∩ ↑e ⁻¹' s = e'.source ∩ ↑e' ⁻¹' s
rw [he.eqOn.inter_preimage_eq, source_eq he]