awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
a : x ∈ Z.baseSet (Z.indexAt x)
a₁ : x ∈ Z.baseSet (Z.indexAt x) ∩ Z.baseSet i ∩ Z.baseSet (Z.indexAt x)
⊢ Eq (α := Z.TotalSpace)
    (TotalSpace.mk (E := Z.Fiber) x (Z.coordChange i (Z.indexAt x) x (Z.coordChange (Z.indexAt x) i x v)))
    (TotalSpace.mk (E := Z.Fiber) x v)

Tactic:
rw [Z.coordChange_comp, Z.coordChange_self]

Premises used: FiberBundleCore.coordChange_self, FiberBundleCore.coordChange_comp
-- 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 : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
⊢ x ∈ Z.baseSet (Z.indexAt x)

Tactic:
apply_rules [mem_baseSet_at, mem_inter]

Premises used: Set.mem_inter, FiberBundleCore.mem_baseSet_at
-- 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 : ι
x : B
v : Z.Fiber x
hx : x ∈ Z.baseSet i
⊢ x ∈ Z.baseSet (Z.indexAt x) ∩ Z.baseSet i ∩ Z.baseSet (Z.indexAt x)

Tactic:
apply_rules [mem_baseSet_at, mem_inter]

Premises used: Set.mem_inter, FiberBundleCore.mem_baseSet_at
-- 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 : ι
x : B
v : F
hx : (x, v) ∈ SProd.sprod (β := Set F) (Z.baseSet i) univ
⊢ x ∈ Z.baseSet i

Tactic:
simp only [prodMk_mem_set_prod_eq, and_true, mem_univ] at hx

Premises used: and_true, Set.prodMk_mem_set_prod_eq, Set.mem_univ
-- 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 : ι
x : B
v : F
hx : x ∈ Z.baseSet i
dsimp : (x, Z.coordChange (Z.indexAt x) i x (Z.coordChange i (Z.indexAt x) x v)) = (x, v)
⊢ (TotalSpace.proj (F := F) (E := Z.Fiber)
        (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2)),
      Z.coordChange
        (Z.indexAt
          (TotalSpace.proj (F := F) (E := Z.Fiber)
            (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2))))
        i
        (TotalSpace.proj (F := F) (E := Z.Fiber)
          (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2)))
        (TotalSpace.snd (E := Z.Fiber)
          (TotalSpace.mk (E := Z.Fiber) (x, v).1 (Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2)))) =
    (x, v)

Tactic:
dsimp only
-- 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 : ι
x : B
v : F
hx a : x ∈ Z.baseSet i
a₁ : x ∈ Z.baseSet i ∩ Z.baseSet (Z.indexAt x) ∩ Z.baseSet i
⊢ (x, Z.coordChange (Z.indexAt x) i x (Z.coordChange i (Z.indexAt x) x v)) = (x, v)

Tactic:
rw [Z.coordChange_comp, Z.coordChange_self]

Premises used: FiberBundleCore.coordChange_self, FiberBundleCore.coordChange_comp
-- 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 : ι
x : B
v : F
hx : x ∈ Z.baseSet i
⊢ x ∈ Z.baseSet i

Tactic:
hx
-- 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 : ι
x : B
v : F
hx : x ∈ Z.baseSet i
⊢ x ∈ Z.baseSet i ∩ Z.baseSet (Z.indexAt x) ∩ Z.baseSet i

Tactic:
⟨⟨hx, Z.mem_baseSet_at _⟩, hx⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, FiberBundleCore.mem_baseSet_at
-- 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 : ι
x : B
v : F
hx : x ∈ Z.baseSet i
⊢ x ∈ Z.baseSet i

Tactic:
exacts [hx, ⟨⟨hx, Z.mem_baseSet_at _⟩, hx⟩]
-- 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.localTrivAsPartialEquiv i).source ↔ p.proj (E := Z.Fiber) ∈ Z.baseSet i

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.1 ∈ Z.baseSet i ∧ Membership.mem (γ := Set F) univ p.2 ↔ p.1 ∈ Z.baseSet i

Tactic:
simp only [and_true, mem_univ]

Premises used: and_true, Set.mem_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
i : ι
p : Z.TotalSpace
⊢ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) p =
    (p.proj (E := Z.Fiber),
      Z.coordChange (Z.indexAt (p.proj (E := Z.Fiber))) i (p.proj (E := Z.Fiber)) (p.snd (E := Z.Fiber)))

Tactic:
rfl

Premises used: 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
i j : ι
left : ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source = (Z.trivChange i j).source
right :
  EqOn (↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)) : B × F → B × F)
    (↑(Z.trivChange i j).toPartialEquiv : B × F → B × F)
    ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source
⊢ (Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j) ≈ (Z.trivChange i j).toPartialEquiv

Tactic:
constructor
-- 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 j : ι
left :
  ∀ (x : B × F),
    x ∈ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source ↔ x ∈ (Z.trivChange i j).source
⊢ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source = (Z.trivChange i j).source

Tactic:
ext x
-- 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 j : ι
x : B × F
left :
  x.1 ∈ Z.baseSet i ∧
      (↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) x ∈ (Z.localTrivAsPartialEquiv j).source ↔
    x.1 ∈ Z.baseSet i ∧ x.1 ∈ Z.baseSet j
⊢ x ∈ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source ↔ x ∈ (Z.trivChange i j).source

Tactic:
simp only [mem_localTrivAsPartialEquiv_target, mfld_simps]

Premises used: FiberBundleCore.mem_localTrivAsPartialEquiv_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 j : ι
x : B × F
⊢ x.1 ∈ Z.baseSet i ∧
      (↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) x ∈ (Z.localTrivAsPartialEquiv j).source ↔
    x.1 ∈ Z.baseSet i ∧ x.1 ∈ Z.baseSet j

Tactic:
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
i j : ι
x : B
v : F
hx : (x, v) ∈ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source
right :
  ∀ (hx : (x ∈ Z.baseSet i ∧ True) ∧ x ∈ Z.baseSet j),
    True ∧ Z.coordChange (Z.indexAt x) j x (Z.coordChange i (Z.indexAt x) x v) = Z.coordChange i j x v
⊢ (↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)) : B × F → B × F) (x, v) =
    (↑(Z.trivChange i j).toPartialEquiv : B × F → B × F) (x, v)

Tactic:
simp only [trivChange, localTrivAsPartialEquiv, PartialEquiv.symm,
      Prod.mk_inj, prodMk_mem_set_prod_eq, PartialEquiv.trans_source, mem_inter_iff,
      mem_preimage, proj, mem_univ, (· ∘ ·),
      PartialEquiv.coe_trans] at hx ⊢

Premises used: PartialEquiv.trans_source, Set.mem_inter_iff, FiberBundleCore.trivChange, Prod.mk_inj, Function.comp, PartialEquiv.symm, Set.prodMk_mem_set_prod_eq, FiberBundleCore.proj, FiberBundleCore.localTrivAsPartialEquiv, PartialEquiv.coe_trans, Set.mem_univ, Set.mem_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 j : ι
x : B
v : F
hx : (x ∈ Z.baseSet i ∧ True) ∧ x ∈ Z.baseSet j
⊢ True ∧ Z.coordChange (Z.indexAt x) j x (Z.coordChange i (Z.indexAt x) x v) = Z.coordChange i j x v

Tactic:
simp only [Z.coordChange_comp, hx, mem_inter_iff, and_self_iff, mem_baseSet_at]

Premises used: Set.mem_inter_iff, and_self_iff, FiberBundleCore.mem_baseSet_at, FiberBundleCore.coordChange_comp
-- 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 : ι
a :
  Membership.mem (γ := Set (Set (Bundle.TotalSpace F Z.Fiber)))
    (⋃ (i : ι),
      ⋃ (s : Set (B × F)),
        ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
          {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
    (Z.localTrivAsPartialEquiv i).source
⊢ IsOpen (Z.localTrivAsPartialEquiv i).source

Tactic:
apply TopologicalSpace.GenerateOpen.basic

Premises used: TopologicalSpace.GenerateOpen.basic
-- 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 : ι
a :
  ∃ (i_1 : ι) (i_2 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_2 ∧
      (Z.localTrivAsPartialEquiv i).source =
        (Z.localTrivAsPartialEquiv i_1).source ∩ (↑(Z.localTrivAsPartialEquiv i_1) : Z.TotalSpace → B × F) ⁻¹' i_2
⊢ Membership.mem (γ := Set (Set (Bundle.TotalSpace F Z.Fiber)))
    (⋃ (i : ι),
      ⋃ (s : Set (B × F)),
        ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
          {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
    (Z.localTrivAsPartialEquiv i).source

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff]

Premises used: Set.mem_iUnion, exists_prop, Set.mem_singleton_iff
-- 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 : ι
⊢ ∃ (i_1 : ι) (i_2 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_2 ∧
      (Z.localTrivAsPartialEquiv i).source =
        (Z.localTrivAsPartialEquiv i_1).source ∩ (↑(Z.localTrivAsPartialEquiv i_1) : Z.TotalSpace → B × F) ⁻¹' i_2

Tactic:
⟨i, Z.baseSet i ×ˢ univ, (Z.isOpen_baseSet i).prod isOpen_univ, ?_⟩

Premises used: SProd.sprod, Set.univ, FiberBundleCore.isOpen_baseSet, isOpen_univ, FiberBundleCore.baseSet, And.intro, Exists.intro, IsOpen.prod
-- 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 : ι
a :
  (Z.localTrivAsPartialEquiv i).source =
    (Z.localTrivAsPartialEquiv i).source ∩
      (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' SProd.sprod (β := Set F) (Z.baseSet i) univ
⊢ ∃ (i_1 : ι) (i_2 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_2 ∧
      (Z.localTrivAsPartialEquiv i).source =
        (Z.localTrivAsPartialEquiv i_1).source ∩ (↑(Z.localTrivAsPartialEquiv i_1) : Z.TotalSpace → B × F) ⁻¹' i_2

Tactic:
refine ⟨i, Z.baseSet i ×ˢ univ, (Z.isOpen_baseSet i).prod isOpen_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
i : ι
a :
  ∀ (p : Z.TotalSpace),
    p ∈ (Z.localTrivAsPartialEquiv i).source ↔
      p ∈
        (Z.localTrivAsPartialEquiv i).source ∩
          (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' SProd.sprod (β := Set F) (Z.baseSet i) univ
⊢ (Z.localTrivAsPartialEquiv i).source =
    (Z.localTrivAsPartialEquiv i).source ∩
      (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' SProd.sprod (β := Set F) (Z.baseSet i) univ

Tactic:
ext p
-- 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.localTrivAsPartialEquiv i).source ↔
    p ∈
      (Z.localTrivAsPartialEquiv i).source ∩
        (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' SProd.sprod (β := Set F) (Z.baseSet i) univ

Tactic:
simp only [localTrivAsPartialEquiv_apply, prodMk_mem_set_prod_eq, mem_inter_iff, and_self_iff,
    mem_localTrivAsPartialEquiv_source, and_true, mem_univ, mem_preimage]

Premises used: and_true, Set.mem_inter_iff, FiberBundleCore.mem_localTrivAsPartialEquiv_source, Set.prodMk_mem_set_prod_eq, FiberBundleCore.localTrivAsPartialEquiv_apply, Set.mem_univ, and_self_iff, Set.mem_preimage
-- 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_1 : ι
b : B
a : F
i : ι
rw :
  ∀ (t : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] t →
      IsOpen ((Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' t)
⊢ ContinuousOn (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) (Z.localTrivAsPartialEquiv i).source

Tactic:
rw [continuousOn_open_iff (Z.open_source' i)]

Premises used: continuousOn_open_iff, FiberBundleCore.open_source'
-- 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_1 : ι
b : B
a : F
i : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
a₁ :
  Membership.mem (γ := Set (Set (Bundle.TotalSpace F Z.Fiber)))
    (⋃ (i : ι),
      ⋃ (s : Set (B × F)),
        ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
          {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
    ((Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s)
⊢ IsOpen ((Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s)

Tactic:
apply TopologicalSpace.GenerateOpen.basic

Premises used: TopologicalSpace.GenerateOpen.basic
-- 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_1 : ι
b : B
a : F
i : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
a₁ :
  ∃ (i_2 : ι) (i_3 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_3 ∧
      (Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s =
        (Z.localTrivAsPartialEquiv i_2).source ∩ (↑(Z.localTrivAsPartialEquiv i_2) : Z.TotalSpace → B × F) ⁻¹' i_3
⊢ Membership.mem (γ := Set (Set (Bundle.TotalSpace F Z.Fiber)))
    (⋃ (i : ι),
      ⋃ (s : Set (B × F)),
        ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
          {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
    ((Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s)

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff]

Premises used: Set.mem_iUnion, exists_prop, Set.mem_singleton_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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
⊢ ∃ (i_2 : ι) (i_3 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_3 ∧
      (Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s =
        (Z.localTrivAsPartialEquiv i_2).source ∩ (↑(Z.localTrivAsPartialEquiv i_2) : Z.TotalSpace → B × F) ⁻¹' i_3

Tactic:
⟨i, s, s_open, rfl⟩

Premises used: And.intro, Exists.intro, 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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
⊢ ∃ (i_2 : ι) (i_3 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_3 ∧
      (Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s =
        (Z.localTrivAsPartialEquiv i_2).source ∩ (↑(Z.localTrivAsPartialEquiv i_2) : Z.TotalSpace → B × F) ⁻¹' i_3

Tactic:
exact ⟨i, s, s_open, 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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
⊢ ContinuousOn (Z.localTrivAsPartialEquiv i).invFun (Z.localTrivAsPartialEquiv i).target

Tactic:
continuousOn_isOpen_of_generateFrom fun t ht ↦ ?_

Premises used: continuousOn_isOpen_of_generateFrom
-- 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_1 : ι
b : B
a : F
i : ι
refine :
  ∀ (t : Set Z.TotalSpace)
    (ht :
      Membership.mem (γ := Set (Set Z.TotalSpace))
        (⋃ (i : ι),
          ⋃ (s : Set (B × F)),
            ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
              {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
        t),
    IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)
⊢ ContinuousOn (Z.localTrivAsPartialEquiv i).invFun (Z.localTrivAsPartialEquiv i).target

Tactic:
refine continuousOn_isOpen_of_generateFrom fun t ht ↦ ?_

Premises used: continuousOn_isOpen_of_generateFrom
-- 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_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
ht :
  Membership.mem (γ := Set (Set Z.TotalSpace))
    (⋃ (i : ι),
      ⋃ (s : Set (B × F)),
        ⋃ (_ : IsOpen[instTopologicalSpaceProd] s),
          {(Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' s})
    t
⊢ ∃ (i : ι) (i_2 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_2 ∧
      t = (Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' i_2

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff] at ht

Premises used: Set.mem_iUnion, exists_prop, Set.mem_singleton_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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
ht :
  ∃ (i : ι) (i_2 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_2 ∧
      t = (Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' i_2
⊢ ∃ (j : ι) (s : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] s ∧
      t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s

Tactic:
ht
-- 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_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
ht :
  ∃ (i : ι) (i_2 : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] i_2 ∧
      t = (Z.localTrivAsPartialEquiv i).source ∩ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) ⁻¹' i_2
obtain :
  ∀ (j : ι) (s : Set (B × F)) (s_open : IsOpen[instTopologicalSpaceProd] s)
    (ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s),
    IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)
⊢ IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)

Tactic:
obtain ⟨j, s, s_open, ts⟩ : ∃ j s, IsOpen s ∧
      t = (localTrivAsPartialEquiv Z j).source ∩ localTrivAsPartialEquiv Z j ⁻¹' s := ht
-- 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_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
rw :
  IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      (Z.localTrivAsPartialEquiv i).invFun ⁻¹'
        ((Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s))
⊢ IsOpen[instTopologicalSpaceProd] ((Z.localTrivAsPartialEquiv i).target ∩ (Z.localTrivAsPartialEquiv i).invFun ⁻¹' t)

Tactic:
rw [ts]
-- 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_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
simp :
  IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s))
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      (Z.localTrivAsPartialEquiv i).invFun ⁻¹'
        ((Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s))

Tactic:
simp only [preimage_inter]

Premises used: Set.preimage_inter