case a
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.35703
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ (localTrivAsLocalEquiv Z i).source ∈
    ⋃ (i : ι) (s : Set (B × F)) (_ : IsOpen s),
      {(localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' s}
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.35703
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ IsOpen (localTrivAsLocalEquiv Z i).source
apply TopologicalSpace.GenerateOpen.basic
case a
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.35703
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ ∃ i_1 i_2,
    IsOpen i_2 ∧
      (localTrivAsLocalEquiv Z i).source = (localTrivAsLocalEquiv Z i_1).source ∩ ↑(localTrivAsLocalEquiv Z i_1) ⁻¹' i_2
case a
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.35703
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ (localTrivAsLocalEquiv Z i).source ∈
    ⋃ (i : ι) (s : Set (B × F)) (_ : IsOpen s),
      {(localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' s}
simp only [exists_prop, mem_iUnion, mem_singleton_iff]
case a
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.35703
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ (localTrivAsLocalEquiv Z i).source =
    (localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' baseSet Z i ×ˢ univ
case a
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.35703
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ ∃ i_1 i_2,
    IsOpen i_2 ∧
      (localTrivAsLocalEquiv Z i).source = (localTrivAsLocalEquiv Z i_1).source ∩ ↑(localTrivAsLocalEquiv Z i_1) ⁻¹' i_2
refine ⟨i, Z.baseSet i ×ˢ univ, (Z.isOpen_baseSet i).prod isOpen_univ, ?_⟩
case a.h
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.35703
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
p : TotalSpace Z
⊢ p ∈ (localTrivAsLocalEquiv Z i).source ↔
    p ∈ (localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' baseSet Z i ×ˢ univ
case a
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.35703
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
⊢ (localTrivAsLocalEquiv Z i).source =
    (localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' baseSet Z i ×ˢ univ
ext p
no goals
case a.h
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.35703
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i✝ : ι
b : B
a : F
i : ι
p : TotalSpace Z
⊢ p ∈ (localTrivAsLocalEquiv Z i).source ↔
    p ∈ (localTrivAsLocalEquiv Z i).source ∩ ↑(localTrivAsLocalEquiv Z i) ⁻¹' baseSet Z i ×ˢ univ
simp only [localTrivAsLocalEquiv_apply, prod_mk_mem_set_prod_eq, mem_inter_iff, and_self_iff,
  mem_localTrivAsLocalEquiv_source, and_true, mem_univ, mem_preimage]