-- Mathlib/Topology/FiberBundle/Constructions.lean
theorem Prod.continuous_inv_fun :
    ContinuousOn (Prod.invFun' e₁ e₂) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)

Proof state:
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ 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 => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)

Tactic:
have H₁ : Continuous fun p : B × F₁ × F₂ ↦ ((p.1, p.2.1), (p.1, p.2.2)) := by fun_prop

Result:
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ 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.1, p.2.1), p.1, p.2.2)
⊢ ContinuousOn ((fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)

Proof state:
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝¹ : (x : B) → Zero (E₁ x)
inst✝ : (x : B) → Zero (E₂ x)
⊢ Continuous fun p => ((p.1, p.2.1), p.1, p.2.2)

Tactic:
fun_prop

Result:
no goals

Proof state:
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ 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.1, p.2.1), p.1, p.2.2)
⊢ ContinuousOn ((fun p => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)

Tactic:
refine (e₁.continuousOn_symm.prod_map e₂.continuousOn_symm).comp H₁.continuousOn ?_

Result:
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ 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.1, p.2.1), p.1, p.2.2)
⊢ MapsTo (fun p => ((p.1, p.2.1), p.1, p.2.2)) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
    ((e₁.baseSet ×ˢ univ) ×ˢ e₂.baseSet ×ˢ univ)

Proof state:
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ 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.1, p.2.1), p.1, p.2.2)
⊢ MapsTo (fun p => ((p.1, p.2.1), p.1, p.2.2)) ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)
    ((e₁.baseSet ×ˢ univ) ×ˢ e₂.baseSet ×ˢ univ)

Tactic:
exact fun x h ↦ ⟨⟨h.1.1, mem_univ _⟩, ⟨h.1.2, mem_univ _⟩⟩

Result:
no goals

Proof state:
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ 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)

Tactic:
rw [(Prod.isInducing_diag F₁ E₁ F₂ E₂).continuousOn_iff]

Result:
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_2
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
inst✝² : TopologicalSpace (TotalSpace F₂ 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 => ({ proj := p.proj, snd := p.snd.1 }, { proj := p.proj, snd := p.snd.2 })) ∘ invFun' e₁ e₂)
    ((e₁.baseSet ∩ e₂.baseSet) ×ˢ univ)