ι : Type ?u.57301
B : Type u_1
F : Type u_2
X : Type ?u.57310
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ IsOpen e.source
ι : Type ?u.57301
B : Type u_1
F : Type u_2
X : Type ?u.57310
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e : Pretrivialization F TotalSpace.proj
⊢ IsOpen e.source
refine isOpen_iSup_iff.mpr fun e' => isOpen_iSup_iff.mpr fun _ => ?_
ι : Type ?u.57301
B : Type u_1
F : Type u_2
X : Type ?u.57310
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ Subtype.val ⁻¹' e.target = Pretrivialization.setSymm e' ⁻¹' e.source
ι : Type ?u.57301
B : Type u_1
F : Type u_2
X : Type ?u.57310
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ IsOpen e.source
refine' isOpen_coinduced.mpr (isOpen_induced_iff.mpr ⟨e.target, e.open_target, _⟩)
case h.mk
ι : Type ?u.57301
B : Type u_1
F : Type u_2
X : Type ?u.57310
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
x : B × F
hx : x ∈ e'.target
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' e.target ↔
    { val := x, property := hx } ∈ Pretrivialization.setSymm e' ⁻¹' e.source
ι : Type ?u.57301
B : Type u_1
F : Type u_2
X : Type ?u.57310
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
⊢ Subtype.val ⁻¹' e.target = Pretrivialization.setSymm e' ⁻¹' e.source
ext ⟨x, hx⟩
no goals
case h.mk
ι : Type ?u.57301
B : Type u_1
F : Type u_2
X : Type ?u.57310
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e✝ e e' : Pretrivialization F TotalSpace.proj
x✝ : e' ∈ a.pretrivializationAtlas
x : B × F
hx : x ∈ e'.target
⊢ { val := x, property := hx } ∈ Subtype.val ⁻¹' e.target ↔
    { val := x, property := hx } ∈ Pretrivialization.setSymm e' ⁻¹' e.source
simp only [mem_preimage, Pretrivialization.setSymm, restrict, e.mem_target, e.mem_source,
  e'.proj_symm_apply hx]