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