-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem continuousOn_symm (e : Trivialization F (π F E)) :
    ContinuousOn (fun z : B × F => TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ univ)

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
⊢ ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z

Tactic:
rintro x ⟨hx : x.1 ∈ e.baseSet, _⟩

Result:
case intro
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
x : B × F
hx : x.1 ∈ e.baseSet
right✝ : x.2 ∈ univ
⊢ { proj := x.1, snd := e.symm x.1 x.2 } = ↑e.symm x

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z
⊢ ContinuousOn (fun z => TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ univ)

Tactic:
refine ContinuousOn.congr ?_ this

Result:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z
⊢ ContinuousOn (↑e.symm) (e.baseSet ×ˢ univ)

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z
⊢ ContinuousOn (↑e.symm) e.target

Tactic:
exact e.toPartialHomeomorph.continuousOn_symm

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
⊢ ContinuousOn (fun z => TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ univ)

Tactic:
have : ∀ z ∈ e.baseSet ×ˢ (univ : Set F),
    TotalSpace.mk z.1 (e.symm z.1 z.2) = e.toPartialHomeomorph.symm z := by
  rintro x ⟨hx : x.1 ∈ e.baseSet, _⟩
  rw [e.mk_symm hx]

Result:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z
⊢ ContinuousOn (fun z => TotalSpace.mk' F z.1 (e.symm z.1 z.2)) (e.baseSet ×ˢ univ)

Proof state:
case intro
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
x : B × F
hx : x.1 ∈ e.baseSet
right✝ : x.2 ∈ univ
⊢ { proj := x.1, snd := e.symm x.1 x.2 } = ↑e.symm x

Tactic:
rw [e.mk_symm hx]

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z
⊢ ContinuousOn (↑e.symm) (e.baseSet ×ˢ univ)

Tactic:
rw [← e.target_eq]

Result:
B : Type u_1
F : Type u_2
E : B → Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace (TotalSpace F E)
inst✝ : (x : B) → Zero (E x)
e : Trivialization F TotalSpace.proj
this : ∀ z ∈ e.baseSet ×ˢ univ, { proj := z.1, snd := e.symm z.1 z.2 } = ↑e.symm z
⊢ ContinuousOn (↑e.symm) e.target