Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: case refine_1
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
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ z.proj ∈ e.baseSet

pp: case refine_2
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
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ IsOpen[instTopologicalSpaceProd] ((s ∩ (a.pretrivializationAt z.proj).baseSet) ×ˢ univ)

pp: case refine_3
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
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ ↑e z ∈ (s ∩ (a.pretrivializationAt z.proj).baseSet) ×ˢ univ

Tactic:
· exact a.mem_base_pretrivializationAt z.proj

Goal state after:
case refine_2
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
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ IsOpen[instTopologicalSpaceProd] ((s ∩ (a.pretrivializationAt z.proj).baseSet) ×ˢ univ)

case refine_3
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
X : Type u_6
inst✝ : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst✝³] s
hf : ∀ b ∈ s, ContinuousOn (f ∘ ↑(a.pretrivializationAt b).symm) ((s ∩ (a.pretrivializationAt b).baseSet) ×ˢ univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
z : TotalSpace F E
hz : z ∈ TotalSpace.proj ⁻¹' s
e : Trivialization F TotalSpace.proj := a.trivializationOfMemPretrivializationAtlas ⋯
⊢ ↑e z ∈ (s ∩ (a.pretrivializationAt z.proj).baseSet) ×ˢ univ