H : Type u
H' : Type ?u.57399
M : Type u_1
M' : Type ?u.57405
M'' : Type ?u.57408
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : LocalEquiv M H
he : e ∈ c.atlas
E : e.target ∩ ↑(LocalEquiv.symm e) ⁻¹' e.source = e.target
⊢ IsOpen e.target
H : Type u
H' : Type ?u.57399
M : Type u_1
M' : Type ?u.57405
M'' : Type ?u.57408
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : LocalEquiv M H
he : e ∈ c.atlas
⊢ IsOpen e.target
have E : e.target ∩ e.symm ⁻¹' e.source = e.target :=
  Subset.antisymm (inter_subset_left _ _) fun x hx ↦
    ⟨hx, LocalEquiv.target_subset_preimage_source _ hx⟩
no goals
H : Type u
H' : Type ?u.57399
M : Type u_1
M' : Type ?u.57405
M'' : Type ?u.57408
inst✝ : TopologicalSpace H
c : ChartedSpaceCore H M
e : LocalEquiv M H
he : e ∈ c.atlas
E : e.target ∩ ↑(LocalEquiv.symm e) ⁻¹' e.source = e.target
⊢ IsOpen e.target
simpa [LocalEquiv.trans_source, E] using c.open_source e e he he