case refine'_1
ι : Type ?u.56874
B : Type u_1
F : Type u_2
E : B → Type ?u.56885
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous fun x => (b, x)

case refine'_2
ι : Type ?u.56874
B : Type u_1
F : Type u_2
E : B → Type ?u.56885
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), (b, x) ∈ e₁.target

case refine'_3
ι : Type ?u.56874
B : Type u_1
F : Type u_2
E : B → Type ?u.56885
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), ↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x) ∈ e₂.source
ι : Type ?u.56874
B : Type u_1
F : Type u_2
E : B → Type ?u.56885
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous (coordChange e₁ e₂ b)
refine' continuous_snd.comp (e₂.toLocalHomeomorph.continuousOn.comp_continuous
  (e₁.toLocalHomeomorph.continuousOn_symm.comp_continuous _ _) _)
no goals
case refine'_1
ι : Type ?u.56874
B : Type u_1
F : Type u_2
E : B → Type ?u.56885
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ Continuous fun x => (b, x)
exact continuous_const.prod_mk continuous_id
no goals
case refine'_2
ι : Type ?u.56874
B : Type u_1
F : Type u_2
E : B → Type ?u.56885
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), (b, x) ∈ e₁.target
exact fun x => e₁.mem_target.2 h₁
case refine'_3
ι : Type ?u.56874
B : Type u_1
F : Type u_2
E : B → Type ?u.56885
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x✝ : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ ↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x) ∈ e₂.source
case refine'_3
ι : Type ?u.56874
B : Type u_1
F : Type u_2
E : B → Type ?u.56885
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
⊢ ∀ (x : F), ↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x) ∈ e₂.source
intro x
no goals
case refine'_3
ι : Type ?u.56874
B : Type u_1
F : Type u_2
E : B → Type ?u.56885
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace E)
e : Trivialization F proj
x✝ : Z
e' : Trivialization F TotalSpace.proj
x' : TotalSpace E
b✝ : B
y : E b✝
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ ↑(LocalHomeomorph.symm e₁.toLocalHomeomorph) (b, x) ∈ e₂.source
rwa [e₂.mem_source, e₁.proj_symm_apply' h₁]