ι : Type ?u.62801
B : Type u_2
F : Type u_3
X : Type ?u.62810
inst✝³ : TopologicalSpace X
E : B → Type u_1
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Continuous (totalSpaceMk b)
ι : Type ?u.62801
B : Type u_2
F : Type u_3
X : Type ?u.62810
inst✝³ : TopologicalSpace X
E : B → Type u_1
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
⊢ Continuous (totalSpaceMk b)
letI := a.totalSpaceTopology
ι : Type ?u.62801
B : Type u_2
F : Type u_3
X : Type ?u.62810
inst✝³ : TopologicalSpace X
E : B → Type u_1
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
b : B
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a b ∈ a.pretrivializationAtlas)
⊢ Continuous (totalSpaceMk b)
ι : Type ?u.62801
B : Type u_2
F : Type u_3
X : Type ?u.62810
inst✝³ : TopologicalSpace X
E : B → Type u_1
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Continuous (totalSpaceMk b)
let e := a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b)
ι : Type ?u.62801
B : Type u_2
F : Type u_3
X : Type ?u.62810
inst✝³ : TopologicalSpace X
E : B → Type u_1
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
b : B
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a b ∈ a.pretrivializationAtlas)
⊢ Continuous (↑e.toLocalHomeomorph ∘ totalSpaceMk b)
ι : Type ?u.62801
B : Type u_2
F : Type u_3
X : Type ?u.62810
inst✝³ : TopologicalSpace X
E : B → Type u_1
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
b : B
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a b ∈ a.pretrivializationAtlas)
⊢ Continuous (totalSpaceMk b)
rw [e.toLocalHomeomorph.continuous_iff_continuous_comp_left
    (a.totalSpaceMk_preimage_source b)]
no goals
ι : Type ?u.62801
B : Type u_2
F : Type u_3
X : Type ?u.62810
inst✝³ : TopologicalSpace X
E : B → Type u_1
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ : Pretrivialization F TotalSpace.proj
b : B
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
e : Trivialization F TotalSpace.proj :=
  trivializationOfMemPretrivializationAtlas a (_ : pretrivializationAt a b ∈ a.pretrivializationAtlas)
⊢ Continuous (↑e.toLocalHomeomorph ∘ totalSpaceMk b)
exact continuous_iff_le_induced.mpr (le_antisymm_iff.mp (a.totalSpaceMk_inducing b).induced).1