case mk.mk
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_4
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_2
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
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)
x : B
w₁ : F₁
w₂ : F₂
h : (x, w₁, w₂) ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_4
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_2
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
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)
x : B × F₁ × F₂
h : x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ x) = x
obtain ⟨x, w₁, w₂⟩ := x
case mk.mk.intro.intro
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_4
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_2
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
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)
x : B
w₁ : F₁
w₂ : F₂
h₁ : x ∈ e₁.baseSet
h₂ : x ∈ e₂.baseSet
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
case mk.mk
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_4
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_2
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
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)
x : B
w₁ : F₁
w₂ : F₂
h : (x, w₁, w₂) ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
obtain ⟨⟨h₁ : x ∈ e₁.baseSet, h₂ : x ∈ e₂.baseSet⟩, -⟩ := h
no goals
case mk.mk.intro.intro
B : Type u_1
inst✝⁶ : TopologicalSpace B
F₁ : Type u_3
inst✝⁵ : TopologicalSpace F₁
E₁ : B → Type u_4
inst✝⁴ : TopologicalSpace (TotalSpace E₁)
F₂ : Type u_2
inst✝³ : TopologicalSpace F₂
E₂ : B → Type u_5
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)
x : B
w₁ : F₁
w₂ : F₂
h₁ : x ∈ e₁.baseSet
h₂ : x ∈ e₂.baseSet
⊢ toFun' e₁ e₂ (invFun' e₁ e₂ (x, w₁, w₂)) = (x, w₁, w₂)
simp only [Prod.toFun', Prod.invFun', apply_mk_symm, h₁, h₂]