ι : Type ?u.50161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.50175
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
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this :
  ∀ (z : B × F),
    z ∈ e.baseSet ×ˢ univ →
      totalSpaceMk z.fst (Trivialization.symm e z.fst z.snd) = ↑(LocalHomeomorph.symm e.toLocalHomeomorph) z
⊢ ContinuousOn (fun z => totalSpaceMk z.fst (Trivialization.symm e z.fst z.snd)) (e.baseSet ×ˢ univ)
ι : Type ?u.50161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.50175
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
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
⊢ ContinuousOn (fun z => totalSpaceMk z.fst (Trivialization.symm e z.fst z.snd)) (e.baseSet ×ˢ univ)
have : ∀ z ∈ e.baseSet ×ˢ (univ : Set F),
    totalSpaceMk z.1 (e.symm z.1 z.2) = e.toLocalHomeomorph.symm z := by
  rintro x ⟨hx : x.1 ∈ e.baseSet, _⟩
  rw [e.mk_symm hx]
ι : Type ?u.50161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.50175
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
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this :
  ∀ (z : B × F),
    z ∈ e.baseSet ×ˢ univ →
      totalSpaceMk z.fst (Trivialization.symm e z.fst z.snd) = ↑(LocalHomeomorph.symm e.toLocalHomeomorph) z
⊢ ContinuousOn (fun x => ↑(LocalHomeomorph.symm e.toLocalHomeomorph) x) (e.baseSet ×ˢ univ)
ι : Type ?u.50161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.50175
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
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this :
  ∀ (z : B × F),
    z ∈ e.baseSet ×ˢ univ →
      totalSpaceMk z.fst (Trivialization.symm e z.fst z.snd) = ↑(LocalHomeomorph.symm e.toLocalHomeomorph) z
⊢ ContinuousOn (fun z => totalSpaceMk z.fst (Trivialization.symm e z.fst z.snd)) (e.baseSet ×ˢ univ)
refine' ContinuousOn.congr _ this
ι : Type ?u.50161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.50175
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
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this :
  ∀ (z : B × F),
    z ∈ e.baseSet ×ˢ univ →
      totalSpaceMk z.fst (Trivialization.symm e z.fst z.snd) = ↑(LocalHomeomorph.symm e.toLocalHomeomorph) z
⊢ ContinuousOn (fun x => ↑(LocalHomeomorph.symm e.toLocalHomeomorph) x) e.target
ι : Type ?u.50161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.50175
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
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this :
  ∀ (z : B × F),
    z ∈ e.baseSet ×ˢ univ →
      totalSpaceMk z.fst (Trivialization.symm e z.fst z.snd) = ↑(LocalHomeomorph.symm e.toLocalHomeomorph) z
⊢ ContinuousOn (fun x => ↑(LocalHomeomorph.symm e.toLocalHomeomorph) x) (e.baseSet ×ˢ univ)
rw [← e.target_eq]
no goals
ι : Type ?u.50161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.50175
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
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this :
  ∀ (z : B × F),
    z ∈ e.baseSet ×ˢ univ →
      totalSpaceMk z.fst (Trivialization.symm e z.fst z.snd) = ↑(LocalHomeomorph.symm e.toLocalHomeomorph) z
⊢ ContinuousOn (fun x => ↑(LocalHomeomorph.symm e.toLocalHomeomorph) x) e.target
exact e.toLocalHomeomorph.continuousOn_symm
case intro
ι : Type ?u.50161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.50175
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
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
x : B × F
hx : x.fst ∈ e.baseSet
right✝ : x.snd ∈ univ
⊢ totalSpaceMk x.fst (Trivialization.symm e x.fst x.snd) = ↑(LocalHomeomorph.symm e.toLocalHomeomorph) x
ι : Type ?u.50161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.50175
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
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
⊢ ∀ (z : B × F),
    z ∈ e.baseSet ×ˢ univ →
      totalSpaceMk z.fst (Trivialization.symm e z.fst z.snd) = ↑(LocalHomeomorph.symm e.toLocalHomeomorph) z
rintro x ⟨hx : x.1 ∈ e.baseSet, _⟩
no goals
case intro
ι : Type ?u.50161
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type ?u.50175
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
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
x : B × F
hx : x.fst ∈ e.baseSet
right✝ : x.snd ∈ univ
⊢ totalSpaceMk x.fst (Trivialization.symm e x.fst x.snd) = ↑(LocalHomeomorph.symm e.toLocalHomeomorph) x
rw [e.mk_symm hx]