no goals
ι : Type ?u.62554
B : Type u_1
F : Type u_2
E : B → Type ?u.62565
Z : Type u_3
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b : B
y : E b
B' : Type ?u.62653
inst✝ : TopologicalSpace B'
e : Trivialization F proj
s : Set B
⊢ e.source ∩ frontier (proj ⁻¹' s) = proj ⁻¹' (e.baseSet ∩ frontier s)
rw [← (e.isImage_preimage_prod s).frontier.preimage_eq, frontier_prod_univ_eq,
  (e.isImage_preimage_prod _).preimage_eq, e.source_eq, preimage_inter]