case intro
B : Type u_2
F : Type u_1
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty F
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ↑e)
⊢ Function.Surjective (Prod.fst ∘ ↑e)
B : Type u_2
F : Type u_1
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
proj : Z → B
inst✝ : Nonempty F
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ Function.Surjective proj
obtain ⟨e, rfl⟩ := h.proj_eq
no goals
case intro
B : Type u_2
F : Type u_1
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty F
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ↑e)
⊢ Function.Surjective (Prod.fst ∘ ↑e)
exact Prod.fst_surjective.comp e.surjective