-- Mathlib/Topology/FiberBundle/Basic.lean
theorem isOpen_target_of_mem_pretrivializationAtlas_inter (e e' : Pretrivialization F (π F E))
    (he' : e' ∈ a.pretrivializationAtlas) :
    IsOpen (e'.toPartialEquiv.target ∩ e'.toPartialEquiv.symm ⁻¹' e.source)

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ IsOpen (e'.target ∩ ↑e'.symm ⁻¹' e.source)

Tactic:
letI := a.totalSpaceTopology

Result:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ IsOpen (e'.target ∩ ↑e'.symm ⁻¹' e.source)

Proof state:
case intro.intro
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
u : Set (B × F)
hu1 : IsOpen u
hu2 : ↑e'.symm ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen (e'.target ∩ ↑e'.symm ⁻¹' e.source)

Tactic:
rw [inter_comm, hu2]

Result:
case intro.intro
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
u : Set (B × F)
hu1 : IsOpen u
hu2 : ↑e'.symm ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen (u ∩ e'.target)

Proof state:
case intro.intro
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
u : Set (B × F)
hu1 : IsOpen u
hu2 : ↑e'.symm ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen (u ∩ e'.target)

Tactic:
exact hu1.inter e'.open_target

Result:
no goals

Proof state:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
⊢ IsOpen (e'.target ∩ ↑e'.symm ⁻¹' e.source)

Tactic:
obtain ⟨u, hu1, hu2⟩ := continuousOn_iff'.mp (a.continuous_symm_of_mem_pretrivializationAtlas he')
  e.source (a.isOpen_source e)

Result:
case intro.intro
B : Type u_2
F : Type u_3
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
u : Set (B × F)
hu1 : IsOpen u
hu2 : ↑e'.symm ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen (e'.target ∩ ↑e'.symm ⁻¹' e.source)