ι : Type ?u.63469
B : Type u_2
F : Type u_3
X : Type ?u.63478
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
h : Inducing (↑(pretrivializationAt a b) ∘ totalSpaceMk b)
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Inducing (totalSpaceMk b)
ι : Type ?u.63469
B : Type u_2
F : Type u_3
X : Type ?u.63478
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
h : Inducing (↑(pretrivializationAt a b) ∘ totalSpaceMk b)
⊢ Inducing (totalSpaceMk b)
letI := a.totalSpaceTopology
ι : Type ?u.63469
B : Type u_2
F : Type u_3
X : Type ?u.63478
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
h :
  Inducing
    (restrict (pretrivializationAt a b).source ↑(pretrivializationAt a b) ∘
      codRestrict (fun x => totalSpaceMk b x) (pretrivializationAt a b).source
        (_ : ∀ (x : E b), totalSpaceMk b x ∈ (pretrivializationAt a b).source))
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Inducing (totalSpaceMk b)
ι : Type ?u.63469
B : Type u_2
F : Type u_3
X : Type ?u.63478
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
h : Inducing (↑(pretrivializationAt a b) ∘ totalSpaceMk b)
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Inducing (totalSpaceMk b)
rw [← restrict_comp_codRestrict (a.mem_pretrivializationAt_source b)] at h
ι : Type ?u.63469
B : Type u_2
F : Type u_3
X : Type ?u.63478
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
h :
  Inducing
    (restrict (pretrivializationAt a b).source ↑(pretrivializationAt a b) ∘
      codRestrict (fun x => totalSpaceMk b x) (pretrivializationAt a b).source
        (_ : ∀ (x : E b), totalSpaceMk b x ∈ (pretrivializationAt a b).source))
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Inducing
    (codRestrict (fun a => totalSpaceMk b a) (pretrivializationAt a b).source
      (_ : ∀ (x : E b), totalSpaceMk b x ∈ (pretrivializationAt a b).source))
ι : Type ?u.63469
B : Type u_2
F : Type u_3
X : Type ?u.63478
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
h :
  Inducing
    (restrict (pretrivializationAt a b).source ↑(pretrivializationAt a b) ∘
      codRestrict (fun x => totalSpaceMk b x) (pretrivializationAt a b).source
        (_ : ∀ (x : E b), totalSpaceMk b x ∈ (pretrivializationAt a b).source))
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Inducing (totalSpaceMk b)
apply Inducing.of_codRestrict (a.mem_pretrivializationAt_source b)
ι : Type ?u.63469
B : Type u_2
F : Type u_3
X : Type ?u.63478
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
h :
  Inducing
    (restrict (pretrivializationAt a b).source ↑(pretrivializationAt a b) ∘
      codRestrict (fun x => totalSpaceMk b x) (pretrivializationAt a b).source
        (_ : ∀ (x : E b), totalSpaceMk b x ∈ (pretrivializationAt a b).source))
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Continuous
    (codRestrict (fun a => totalSpaceMk b a) (pretrivializationAt a b).source
      (_ : ∀ (x : E b), totalSpaceMk b x ∈ (pretrivializationAt a b).source))
ι : Type ?u.63469
B : Type u_2
F : Type u_3
X : Type ?u.63478
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
h :
  Inducing
    (restrict (pretrivializationAt a b).source ↑(pretrivializationAt a b) ∘
      codRestrict (fun x => totalSpaceMk b x) (pretrivializationAt a b).source
        (_ : ∀ (x : E b), totalSpaceMk b x ∈ (pretrivializationAt a b).source))
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Inducing
    (codRestrict (fun a => totalSpaceMk b a) (pretrivializationAt a b).source
      (_ : ∀ (x : E b), totalSpaceMk b x ∈ (pretrivializationAt a b).source))
refine inducing_of_inducing_compose ?_ (continuousOn_iff_continuous_restrict.mp
  (a.trivializationOfMemPretrivializationAtlas
    (a.pretrivialization_mem_atlas b)).continuous_toFun) h
no goals
ι : Type ?u.63469
B : Type u_2
F : Type u_3
X : Type ?u.63478
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
h :
  Inducing
    (restrict (pretrivializationAt a b).source ↑(pretrivializationAt a b) ∘
      codRestrict (fun x => totalSpaceMk b x) (pretrivializationAt a b).source
        (_ : ∀ (x : E b), totalSpaceMk b x ∈ (pretrivializationAt a b).source))
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Continuous
    (codRestrict (fun a => totalSpaceMk b a) (pretrivializationAt a b).source
      (_ : ∀ (x : E b), totalSpaceMk b x ∈ (pretrivializationAt a b).source))
exact (a.continuous_totalSpaceMk b).codRestrict (a.mem_pretrivializationAt_source b)