B : Type u_3
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_1
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_4
inst✝² : TopologicalSpace (TotalSpace E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ ContinuousOn ((fun p => ({ fst := p.fst, snd := p.snd.fst }, { fst := p.fst, snd := p.snd.snd })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
B : Type u_3
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_1
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_4
inst✝² : TopologicalSpace (TotalSpace E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ ContinuousOn (invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
rw [(Prod.inducing_diag E₁ E₂).continuousOn_iff]
B : Type u_3
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_1
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_4
inst✝² : TopologicalSpace (TotalSpace E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
H₁ : Continuous fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)
⊢ ContinuousOn ((fun p => ({ fst := p.fst, snd := p.snd.fst }, { fst := p.fst, snd := p.snd.snd })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
B : Type u_3
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_1
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_4
inst✝² : TopologicalSpace (TotalSpace E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ ContinuousOn ((fun p => ({ fst := p.fst, snd := p.snd.fst }, { fst := p.fst, snd := p.snd.snd })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
have H₁ : Continuous fun p : B × F₁ × F₂ ↦ ((p.1, p.2.1), (p.1, p.2.2)) :=
  (continuous_id.prod_map continuous_fst).prod_mk (continuous_id.prod_map continuous_snd)
B : Type u_3
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_1
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_4
inst✝² : TopologicalSpace (TotalSpace E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
H₁ : Continuous fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)
⊢ MapsTo (fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
    ((e₁.baseSet ×ˢ univ) ×ˢ e₂.baseSet ×ˢ univ)
B : Type u_3
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_1
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_4
inst✝² : TopologicalSpace (TotalSpace E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
H₁ : Continuous fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)
⊢ ContinuousOn ((fun p => ({ fst := p.fst, snd := p.snd.fst }, { fst := p.fst, snd := p.snd.snd })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
refine' (e₁.continuousOn_symm.prod_map e₂.continuousOn_symm).comp H₁.continuousOn _
no goals
B : Type u_3
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_5
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_1
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_4
inst✝² : TopologicalSpace (TotalSpace E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
H₁ : Continuous fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)
⊢ MapsTo (fun p => ((p.fst, p.snd.fst), p.fst, p.snd.snd)) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
    ((e₁.baseSet ×ˢ univ) ×ˢ e₂.baseSet ×ˢ univ)
exact fun x h ↦ ⟨⟨h.1.1, mem_univ _⟩, ⟨h.1.2, mem_univ _⟩⟩