ι : Type ?u.42663
B : Type u_2
F : Type u_3
E : B → Type ?u.42674
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑(LocalEquiv.symm e.toLocalEquiv)) (↑e z)
hez : z ∈ (LocalEquiv.symm e.toLocalEquiv).target
⊢ ContinuousAt f z
ι : Type ?u.42663
B : Type u_2
F : Type u_3
E : B → Type ?u.42674
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑(LocalEquiv.symm e.toLocalEquiv)) (↑e z)
⊢ ContinuousAt f z
have hez : z ∈ e.toLocalEquiv.symm.target := by
  rw [LocalEquiv.symm_target, e.mem_source]
  exact he
no goals
ι : Type ?u.42663
B : Type u_2
F : Type u_3
E : B → Type ?u.42674
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑(LocalEquiv.symm e.toLocalEquiv)) (↑e z)
hez : z ∈ (LocalEquiv.symm e.toLocalEquiv).target
⊢ ContinuousAt f z
rwa [e.toLocalHomeomorph.symm.continuousAt_iff_continuousAt_comp_right hez,
  LocalHomeomorph.symm_symm]
ι : Type ?u.42663
B : Type u_2
F : Type u_3
E : B → Type ?u.42674
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑(LocalEquiv.symm e.toLocalEquiv)) (↑e z)
⊢ proj z ∈ e.baseSet
ι : Type ?u.42663
B : Type u_2
F : Type u_3
E : B → Type ?u.42674
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑(LocalEquiv.symm e.toLocalEquiv)) (↑e z)
⊢ z ∈ (LocalEquiv.symm e.toLocalEquiv).target
rw [LocalEquiv.symm_target, e.mem_source]
no goals
ι : Type ?u.42663
B : Type u_2
F : Type u_3
E : B → Type ?u.42674
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : Z → X
z : Z
e : Trivialization F proj
he : proj z ∈ e.baseSet
hf : ContinuousAt (f ∘ ↑(LocalEquiv.symm e.toLocalEquiv)) (↑e z)
⊢ proj z ∈ e.baseSet
exact he