awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
a : F
⊢ (↑(Z.localTrivAt b) : Bundle.TotalSpace F Z.Fiber → B × F) (TotalSpace.mk (E := Z.Fiber) b a) = (b, a)

Tactic:
Z.localTrivAt_apply _

Premises used: FiberBundleCore.localTrivAt_apply
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : Z.TotalSpace
⊢ p ∈ (Z.localTriv i).source ↔ p.proj (E := Z.Fiber) ∈ (Z.localTriv i).baseSet

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
p : Z.TotalSpace
b : B
⊢ p ∈ (Z.localTrivAt b).source ↔ p.proj (E := Z.Fiber) ∈ (Z.localTrivAt b).baseSet

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : B × F
⊢ p ∈ (Z.localTriv i).target ↔ p.1 ∈ (Z.localTriv i).baseSet

Tactic:
Trivialization.mem_target _

Premises used: Bundle.Trivialization.mem_target
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
p : B × F
b : B
⊢ p ∈ (Z.localTrivAt b).target ↔ p.1 ∈ (Z.localTrivAt b).baseSet

Tactic:
Trivialization.mem_target _

Premises used: Bundle.Trivialization.mem_target
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : B × F
⊢ (↑(Z.localTriv i).symm : B × F → Z.TotalSpace) p =
    TotalSpace.mk (E := Z.Fiber) p.1 (Z.coordChange i (Z.indexAt p.1) p.1 p.2)

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
rw : b ∈ Z.baseSet (Z.indexAt b)
⊢ b ∈ (Z.localTrivAt b).baseSet

Tactic:
rw [localTrivAt, ← baseSet_at]

Premises used: FiberBundleCore.baseSet_at, FiberBundleCore.localTrivAt
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ b ∈ Z.baseSet (Z.indexAt b)

Tactic:
Z.mem_baseSet_at b

Premises used: FiberBundleCore.mem_baseSet_at
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ b ∈ Z.baseSet (Z.indexAt b)

Tactic:
exact Z.mem_baseSet_at b

Premises used: FiberBundleCore.mem_baseSet_at
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
a : F
⊢ TotalSpace.mk (E := Z.Fiber) b a ∈ (Z.localTrivAt b).source

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
rw :
  𝓝 x =
    comap
        ((↑(Z.localTrivAt b).toOpenPartialHomeomorph : Bundle.TotalSpace F Z.Fiber → B × F) ∘
          TotalSpace.mk (E := Z.Fiber) b)
        (𝓝
          ((↑(Z.localTrivAt b).toOpenPartialHomeomorph : Bundle.TotalSpace F Z.Fiber → B × F)
            (TotalSpace.mk (E := Z.Fiber) b x))) ⊓
      𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source)
⊢ 𝓝 x = comap (β := Bundle.TotalSpace F Z.Fiber) (TotalSpace.mk (E := Z.Fiber) b) (𝓝 (TotalSpace.mk (E := Z.Fiber) b x))

Tactic:
rw [(Z.localTrivAt b).nhds_eq_comap_inf_principal (mk_mem_localTrivAt_source _ _ _), comap_inf,
      comap_principal, comap_comap]

Premises used: FiberBundleCore.mk_mem_localTrivAt_source, Filter.comap_inf, Filter.comap_comap, Filter.comap_principal, OpenPartialHomeomorph.nhds_eq_comap_inf_principal, FiberBundleCore.localTrivAt, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
simp : 𝓝 x = 𝓝 x ⊓ 𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source)
⊢ 𝓝 x =
    comap
        ((↑(Z.localTrivAt b).toOpenPartialHomeomorph : Bundle.TotalSpace F Z.Fiber → B × F) ∘
          TotalSpace.mk (E := Z.Fiber) b)
        (𝓝
          ((↑(Z.localTrivAt b).toOpenPartialHomeomorph : Bundle.TotalSpace F Z.Fiber → B × F)
            (TotalSpace.mk (E := Z.Fiber) b x))) ⊓
      𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source)

Tactic:
simp only [Function.comp_def, localTrivAt_apply_mk, Trivialization.coe_coe,
      ← (isEmbedding_prodMkRight b).nhds_eq_comap]

Premises used: Topology.IsInducing.nhds_eq_comap, Function.comp_def, Bundle.Trivialization.coe_coe, Topology.IsEmbedding.toIsInducing, FiberBundleCore.localTrivAt_apply_mk, isEmbedding_prodMkRight
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
h : 𝓝 x ⊓ 𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source) = 𝓝 x ⊓ 𝓟 univ
convert_to : 𝓝 x = 𝓝 x ⊓ 𝓟 univ
⊢ 𝓝 x = 𝓝 x ⊓ 𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source)

Tactic:
convert_to 𝓝 x = 𝓝 x ⊓ 𝓟 univ

Premises used: Set.univ, nhds, Filter.principal
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
h : TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source = univ
⊢ 𝓝 x ⊓ 𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source) = 𝓝 x ⊓ 𝓟 univ

Tactic:
congr
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
⊢ TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source = univ

Tactic:
eq_univ_of_forall (mk_mem_localTrivAt_source Z _)

Premises used: FiberBundleCore.mk_mem_localTrivAt_source, Set.eq_univ_of_forall
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
⊢ TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source = univ

Tactic:
exact eq_univ_of_forall (mk_mem_localTrivAt_source Z _)

Premises used: FiberBundleCore.mk_mem_localTrivAt_source, Set.eq_univ_of_forall
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
rw : 𝓝 x = 𝓝 x ⊓ ⊤
rw₁ rw₂ : 𝓝 x = 𝓝 x
⊢ 𝓝 x = 𝓝 x ⊓ 𝓟 univ

Tactic:
rw [principal_univ, inf_top_eq]

Premises used: inf_top_eq, Filter.principal_univ
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ Continuous (X := Z.Fiber b) (Y := Bundle.TotalSpace F Z.Fiber) (TotalSpace.mk (E := Z.Fiber) b)

Tactic:
FiberBundle.continuous_totalSpaceMk F Z.Fiber b

Premises used: FiberBundleCore.Fiber, FiberBundle.continuous_totalSpaceMk
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
⊢ Continuous[_, inst] Z.proj

Tactic:
FiberBundle.continuous_proj F Z.Fiber

Premises used: FiberBundleCore.Fiber, FiberBundle.continuous_proj
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
⊢ IsOpenMap Z.proj

Tactic:
FiberBundle.isOpenMap_proj F Z.Fiber

Premises used: FiberBundleCore.Fiber, FiberBundle.isOpenMap_proj
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
⊢ ContinuousOn (↑e.symm : B × F → TotalSpace F E) e.target

Tactic:
fun z H U h => preimage_nhdsWithin_coinduced' H (le_def.1 (nhds_mono ?_) U h)

Premises used: ContinuousWithinAt, Set.Mem, setOf, Set.preimage, Filter.Tendsto, nhds_mono, Iff.mp, ContinuousOn, preimage_nhdsWithin_coinduced', Filter.le_def
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
refine :
  ∀ (z : B × F) (H : z ∈ e.target) (U : Set (TotalSpace F E)) (h : U ∈ 𝓝 ((↑e.symm : B × F → TotalSpace F E) z)),
    coinduced (fun (x : (↑e.target : Type (max u_2 u_3))) ↦ (↑e.symm : B × F → TotalSpace F E) (↑x : B × F))
        inferInstance ≤
      a.totalSpaceTopology (E := E)
⊢ ContinuousOn (↑e.symm : B × F → TotalSpace F E) e.target

Tactic:
refine fun z H U h => preimage_nhdsWithin_coinduced' H (le_def.1 (nhds_mono ?_) U h)

Premises used: nhds_mono, Iff.mp, preimage_nhdsWithin_coinduced', Filter.le_def
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
z : B × F
H : z ∈ e.target
U : Set (TotalSpace F E)
h : U ∈ 𝓝 ((↑e.symm : B × F → TotalSpace F E) z)
⊢ coinduced (fun (x : (↑e.target : Type (max u_2 u_3))) ↦ (↑e.symm : B × F → TotalSpace F E) (↑x : B × F))
      inferInstance ≤
    a.totalSpaceTopology (E := E)

Tactic:
le_iSup₂ (α := TopologicalSpace (TotalSpace F E)) e he

Premises used: le_iSup₂, Bundle.Pretrivialization.setSymm, Set.restrict
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
z : B × F
H : z ∈ e.target
U : Set (TotalSpace F E)
h : U ∈ 𝓝 ((↑e.symm : B × F → TotalSpace F E) z)
⊢ coinduced (fun (x : (↑e.target : Type (max u_2 u_3))) ↦ (↑e.symm : B × F → TotalSpace F E) (↑x : B × F))
      inferInstance ≤
    a.totalSpaceTopology (E := E)

Tactic:
exact le_iSup₂ (α := TopologicalSpace (TotalSpace F E)) e he

Premises used: le_iSup₂
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
⊢ IsOpen[a.totalSpaceTopology] e.source

Tactic:
isOpen_iSup_iff.mpr fun e' => isOpen_iSup_iff.mpr fun _ => ?_

Premises used: Iff.mpr, isOpen_iSup_iff
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
refine : ∀ e' ∈ a.pretrivializationAtlas (E := E), IsOpen[coinduced e'.setSymm instTopologicalSpaceSubtype] e.source
⊢ IsOpen[a.totalSpaceTopology] e.source

Tactic:
refine isOpen_iSup_iff.mpr fun e' => isOpen_iSup_iff.mpr fun _ => ?_

Premises used: Iff.mpr, isOpen_iSup_iff
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
h : e' ∈ a.pretrivializationAtlas (E := E)
⊢ IsOpen[coinduced e'.setSymm instTopologicalSpaceSubtype] e.source

Tactic:
isOpen_coinduced.mpr (isOpen_induced_iff.mpr ⟨e.target, e.open_target, ?_⟩)

Premises used: Iff.mpr, PartialEquiv.target, Bundle.Pretrivialization.open_target, isOpen_coinduced, Bundle.Pretrivialization.toPartialEquiv, And.intro, Exists.intro, isOpen_induced_iff
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
h : e' ∈ a.pretrivializationAtlas (E := E)
refine : Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹' e.target = e'.setSymm ⁻¹' e.source
⊢ IsOpen[coinduced e'.setSymm instTopologicalSpaceSubtype] e.source

Tactic:
refine isOpen_coinduced.mpr (isOpen_induced_iff.mpr ⟨e.target, e.open_target, ?_⟩)

Premises used: Iff.mpr, PartialEquiv.target, Bundle.Pretrivialization.open_target, isOpen_coinduced, Bundle.Pretrivialization.toPartialEquiv, And.intro, Exists.intro, isOpen_induced_iff
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
h_1 : e' ∈ a.pretrivializationAtlas (E := E)
h :
  ∀ (x : B × F) (hx : x ∈ e'.target),
    Membership.mem (γ := Set (↑e'.target : Type (max u_2 u_3)))
        (Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹' e.target)
        (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e'.target) x hx) ↔
      Subtype.mk (p := fun (x : B × F) ↦ x ∈ e'.target) x hx ∈ e'.setSymm ⁻¹' e.source
⊢ Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹' e.target = e'.setSymm ⁻¹' e.source

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
h : e' ∈ a.pretrivializationAtlas (E := E)
x : B × F
hx : x ∈ e'.target
⊢ Membership.mem (γ := Set (↑e'.target : Type (max u_2 u_3)))
      (Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹' e.target)
      (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e'.target) x hx) ↔
    Subtype.mk (p := fun (x : B × F) ↦ x ∈ e'.target) x hx ∈ e'.setSymm ⁻¹' e.source

Tactic:
simp only [mem_preimage, Pretrivialization.setSymm, restrict, e.mem_target, e.mem_source,
    e'.proj_symm_apply hx]

Premises used: Bundle.Pretrivialization.mem_source, Bundle.Pretrivialization.mem_target, Bundle.Pretrivialization.proj_symm_apply, Bundle.Pretrivialization.setSymm, Set.restrict, Set.mem_preimage
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
obtain :
  ∀ (u : Set (B × F)) (hu1 : IsOpen[instTopologicalSpaceProd] u)
    (hu2 : (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source ∩ e'.target = u ∩ e'.target),
    IsOpen[instTopologicalSpaceProd] (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
⊢ IsOpen[instTopologicalSpaceProd] (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)

Tactic:
obtain ⟨u, hu1, hu2⟩ := continuousOn_iff'.mp (a.continuous_symm_of_mem_pretrivializationAtlas he')
    e.source (a.isOpen_source e)

Premises used: FiberPrebundle.continuous_symm_of_mem_pretrivializationAtlas, FiberPrebundle.isOpen_source, Bundle.Pretrivialization.toPartialEquiv, Iff.mp, PartialEquiv.source, continuousOn_iff'
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 : (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source ∩ e'.target = u ∩ e'.target
rw : IsOpen[instTopologicalSpaceProd] (u ∩ e'.target)
⊢ IsOpen[instTopologicalSpaceProd] (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)

Tactic:
rw [inter_comm, hu2]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 : (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen[instTopologicalSpaceProd] (u ∩ e'.target)

Tactic:
hu1.inter e'.open_target

Premises used: Bundle.Pretrivialization.open_target, IsOpen.inter
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_5
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 : (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen[instTopologicalSpaceProd] (u ∩ e'.target)

Tactic:
exact hu1.inter e'.open_target

Premises used: Bundle.Pretrivialization.open_target, IsOpen.inter
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
E : B → Type u_5
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
inst_3 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
x : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
rw : (↑e.toPartialEquiv : TotalSpace F E → B × F) ⁻¹' s ∩ e.source = (↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source
⊢ (↑e.toPartialEquiv : TotalSpace F E → B × F) ⁻¹' s ∩ e.source =
    (↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source ∩ e.source

Tactic:
rw [inter_assoc, inter_self]

Premises used: Set.inter_self, Set.inter_assoc
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
E : B → Type u_5
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
inst_3 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
x : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
⊢ (↑e.toPartialEquiv : TotalSpace F E → B × F) ⁻¹' s ∩ e.source = (↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source

Tactic:
rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
E : B → Type u_5
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
inst_3 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
x : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
refine :
  ∀ (s : Set (B × F)) (hs : IsOpen[instTopologicalSpaceProd] s)
    (e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))),
    IsOpen[⨆ (_ : e' ∈ a.pretrivializationAtlas), coinduced e'.setSymm instTopologicalSpaceSubtype]
      ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)
⊢ ContinuousOn (↑e.toPartialEquiv : TotalSpace F E → B × F) e.source

Tactic:
refine continuousOn_iff'.mpr fun s hs => ⟨e ⁻¹' s ∩ e.source,
        isOpen_iSup_iff.mpr fun e' => ?_, by rw [inter_assoc, inter_self]; rfl⟩

Premises used: Iff.mpr, Bundle.Pretrivialization.toFun', isOpen_iSup_iff, Inter.inter, Set.preimage, Bundle.Pretrivialization.toPartialEquiv, And.intro, Exists.intro, PartialEquiv.source, continuousOn_iff'
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
E : B → Type u_5
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
inst_3 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
x : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
⊢ IsOpen[⨆ (_ : e' ∈ a.pretrivializationAtlas), coinduced e'.setSymm instTopologicalSpaceSubtype]
    ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)

Tactic:
isOpen_iSup_iff.mpr fun he' => ?_

Premises used: Iff.mpr, isOpen_iSup_iff
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
E : B → Type u_5
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
inst_3 : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
x : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
refine :
  ∀ (he' : e' ∈ a.pretrivializationAtlas (E := E)),
    IsOpen[coinduced e'.setSymm instTopologicalSpaceSubtype] ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)
⊢ IsOpen[⨆ (_ : e' ∈ a.pretrivializationAtlas), coinduced e'.setSymm instTopologicalSpaceSubtype]
    ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)

Tactic:
refine isOpen_iSup_iff.mpr fun he' => ?_

Premises used: Iff.mpr, isOpen_iSup_iff