awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
b : B
h :
  IsInducing
    ((a.pretrivializationAt (E := E) b).source.restrict («π» := fun (a : TotalSpace F E) ↦ B × F)
        (↑(a.pretrivializationAt (E := E) b) : TotalSpace F E → B × F) ∘
      codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source ⋯)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
refine :
  Continuous[inst_2 b, instTopologicalSpaceSubtype]
    (codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source ⋯)
⊢ IsInducing (codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source ⋯)

Tactic:
refine h.of_comp ?_ (continuousOn_iff_continuous_restrict.mp
    (a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b)).continuousOn)

Premises used: FiberPrebundle.trivializationOfMemPretrivializationAtlas, continuousOn_iff_continuous_restrict, Bundle.Trivialization.continuousOn, Iff.mp, Topology.IsInducing.of_comp, FiberPrebundle.pretrivialization_mem_atlas
-- 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
b : B
h :
  IsInducing
    ((a.pretrivializationAt (E := E) b).source.restrict («π» := fun (a : TotalSpace F E) ↦ B × F)
        (↑(a.pretrivializationAt (E := E) b) : TotalSpace F E → B × F) ∘
      codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source ⋯)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
⊢ Continuous[inst_2 b, instTopologicalSpaceSubtype]
    (codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source ⋯)

Tactic:
(a.continuous_totalSpaceMk b).codRestrict (a.mem_pretrivializationAt_source b)

Premises used: FiberPrebundle.mem_pretrivializationAt_source, FiberPrebundle.continuous_totalSpaceMk, Continuous.codRestrict
-- 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
b : B
h :
  IsInducing
    ((a.pretrivializationAt (E := E) b).source.restrict («π» := fun (a : TotalSpace F E) ↦ B × F)
        (↑(a.pretrivializationAt (E := E) b) : TotalSpace F E → B × F) ∘
      codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source ⋯)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
⊢ Continuous[inst_2 b, instTopologicalSpaceSubtype]
    (codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source ⋯)

Tactic:
exact (a.continuous_totalSpaceMk b).codRestrict (a.mem_pretrivializationAt_source b)

Premises used: FiberPrebundle.mem_pretrivializationAt_source, FiberPrebundle.continuous_totalSpaceMk, Continuous.codRestrict
-- 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
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
⊢ Continuous[a.totalSpaceTopology, inst] (TotalSpace.proj (E := E))

Tactic:
FiberBundle.continuous_proj F E

Premises used: FiberBundle.continuous_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
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
⊢ Continuous[a.totalSpaceTopology, inst] (TotalSpace.proj (E := E))

Tactic:
exact FiberBundle.continuous_proj F E

Premises used: FiberBundle.continuous_proj
-- 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 e₀ : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he₀ : e₀ ∈ a.pretrivializationAtlas (E := E)
⊢ MemTrivializationAtlas (E := E) (a.trivializationOfMemPretrivializationAtlas (E := E) he₀)

Tactic:
letI := a.totalSpaceTopology; letI := a.toFiberBundle; ⟨e₀, he₀, rfl⟩

Premises used: Exists.intro, MemTrivializationAtlas.mk, rfl
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
⊢ ContinuousWithinAt f (TotalSpace.proj (E := E) ⁻¹' s) z

Tactic:
(e.continuousAt_of_comp_right ?_
    ((hf z.proj hz).continuousAt (IsOpen.mem_nhds ?_ ?_))).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, Bundle.Trivialization.continuousAt_of_comp_right, Bundle.TotalSpace.proj, IsOpen.mem_nhds, ContinuousOn.continuousAt
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
refine_1 : z.proj (E := E) ∈ e.baseSet
refine_2 :
  IsOpen[instTopologicalSpaceProd]
    (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet) univ)
refine_3 :
  (↑e : TotalSpace F E → B × F) z ∈
    SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet) univ
⊢ ContinuousWithinAt f (TotalSpace.proj (E := E) ⁻¹' s) z

Tactic:
refine (e.continuousAt_of_comp_right ?_
    ((hf z.proj hz).continuousAt (IsOpen.mem_nhds ?_ ?_))).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, Bundle.Trivialization.continuousAt_of_comp_right, Bundle.TotalSpace.proj, IsOpen.mem_nhds, ContinuousOn.continuousAt
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
⊢ z.proj (E := E) ∈ e.baseSet

Tactic:
a.mem_base_pretrivializationAt z.proj

Premises used: Set.Mem, Bundle.TotalSpace.proj, FiberPrebundle.mem_base_pretrivializationAt
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
⊢ z.proj (E := E) ∈ e.baseSet

Tactic:
exact a.mem_base_pretrivializationAt z.proj

Premises used: Bundle.TotalSpace.proj, FiberPrebundle.mem_base_pretrivializationAt
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
⊢ IsOpen[instTopologicalSpaceProd]
    (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet) univ)

Tactic:
(hs.inter (a.pretrivializationAt z.proj).open_baseSet).prod isOpen_univ

Premises used: isOpen_univ, FiberPrebundle.pretrivializationAt, Bundle.TotalSpace.proj, Bundle.Pretrivialization.open_baseSet, IsOpen.inter, IsOpen.prod
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
⊢ IsOpen[instTopologicalSpaceProd]
    (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet) univ)

Tactic:
exact (hs.inter (a.pretrivializationAt z.proj).open_baseSet).prod isOpen_univ

Premises used: isOpen_univ, FiberPrebundle.pretrivializationAt, Bundle.TotalSpace.proj, Bundle.Pretrivialization.open_baseSet, IsOpen.inter, IsOpen.prod
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
⊢ (↑e : TotalSpace F E → B × F) z ∈
    SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet) univ

Tactic:
⟨?_, mem_univ _⟩

Premises used: Set.Mem, setOf, Set.prod, And.intro, Set.mem_univ
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
refine_3 : ((↑e : TotalSpace F E → B × F) z).1 ∈ s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet
⊢ (↑e : TotalSpace F E → B × F) z ∈
    SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet) univ

Tactic:
refine ⟨?_, mem_univ _⟩
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
refine_3 : z.proj (E := E) ∈ s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet
refine_3₁ : z ∈ e.source
⊢ ((↑e : TotalSpace F E → B × F) z).1 ∈ s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet

Tactic:
rw [e.coe_fst]

Premises used: Bundle.Trivialization.coe_fst
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
⊢ z.proj (E := E) ∈ s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet

Tactic:
⟨hz, a.mem_base_pretrivializationAt z.proj⟩

Premises used: Set.Mem, setOf, Set.inter, Bundle.TotalSpace.proj, And.intro, FiberPrebundle.mem_base_pretrivializationAt
-- 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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
⊢ z.proj (E := E) ∈ s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet

Tactic:
exact ⟨hz, a.mem_base_pretrivializationAt z.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
X : Type u_6
inst_3 : TopologicalSpace X
f : TotalSpace F E → X
s : Set B
hs : IsOpen[inst] s
hf :
  ∀ b ∈ s,
    ContinuousOn (f ∘ (↑(a.pretrivializationAt (E := E) b).symm : B × F → TotalSpace F E))
      (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) b).baseSet) univ)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
z : TotalSpace F E
hz : Membership.mem (γ := Set (TotalSpace F E)) (TotalSpace.proj (E := E) ⁻¹' s) z
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) (e := a.pretrivializationAt (E := E) (z.proj (E := E))) ⋯
refine_3 : z.proj (E := E) ∈ e.baseSet
⊢ z ∈ e.source

Tactic:
rw [e.mem_source]

Premises used: Bundle.Trivialization.mem_source
-- 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)
inst_3 : (x : B) → Zero (E x)
inst_4 : TopologicalSpace (TotalSpace F E)
inst_5 : FiberBundle F E
x : B
v : E x
⊢ extend F (E := E) v x = v

Tactic:
simp [extend, FiberBundle.mem_baseSet_trivializationAt' x]

Premises used: FiberBundle.mem_baseSet_trivializationAt', FiberBundle.extend
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
F : Type u_2
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
simp :
  topologicalSpace B F =
    induced
        (Function.comp (β := B × F) Prod.fst (⇑(TotalSpace.toProd B F) : (a : TotalSpace F fun (x : B) ↦ F) → B × F))
        inst ⊓
      induced
        (Function.comp (β := B × F) Prod.snd (⇑(TotalSpace.toProd B F) : (a : TotalSpace F fun (x : B) ↦ F) → B × F))
        inst_1
⊢ topologicalSpace B F =
    induced (Y := B × F) (⇑(TotalSpace.toProd B F) : (a : TotalSpace F fun (x : B) ↦ F) → B × F)
      instTopologicalSpaceProd

Tactic:
simp only [instTopologicalSpaceProd, induced_inf, induced_compose]

Premises used: induced_inf, instTopologicalSpaceProd, induced_compose
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
F : Type u_2
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
⊢ topologicalSpace B F =
    induced
        (Function.comp (β := B × F) Prod.fst (⇑(TotalSpace.toProd B F) : (a : TotalSpace F fun (x : B) ↦ F) → B × F))
        inst ⊓
      induced
        (Function.comp (β := B × F) Prod.snd (⇑(TotalSpace.toProd B F) : (a : TotalSpace F fun (x : B) ↦ F) → B × F))
        inst_1

Tactic:
rfl
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
F : Type u_2
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
inst_2 : Zero F
b : B
f : F
⊢ Trivialization.symm (E := Trivial B F) (trivialization B F) b f = f

Tactic:
simp [trivialization, homeomorphProd, TotalSpace.toProd, Trivialization.symm,
    Pretrivialization.symm, Trivialization.toPretrivialization]

Premises used: Bundle.Trivialization.symm, Bundle.TotalSpace.toProd, Bundle.Trivial.trivialization, Bundle.Pretrivialization.symm, Bundle.Trivial.homeomorphProd, Bundle.Trivialization.toPretrivialization
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
F : Type u_2
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
v : B × F
⊢ (↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivialization B F))) :
        B × F → TotalSpace F (Trivial B F))
      v =
    TotalSpace.mk (E := Trivial B F) v.1 v.2

Tactic:
rfl

Premises used: OpenPartialHomeomorph.toFun', rfl
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
F : Type u_2
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
e : Trivialization (B := B) F (Z := TotalSpace F (Trivial B F)) (TotalSpace.proj (E := Trivial B F))
i : MemTrivializationAtlas (E := Trivial B F) e
⊢ e = trivialization B F

Tactic:
i.out

Premises used: Set.Mem, MemTrivializationAtlas.out, setOf, Set.singleton
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
F₁ : Type u_2
E₁ : B → Type u_3
F₂ : Type u_4
E₂ : B → Type u_5
inst : TopologicalSpace (TotalSpace F₁ E₁)
inst_1 : TopologicalSpace (TotalSpace F₂ E₂)
⊢ IsInducing (Y := TotalSpace F₁ E₁ × TotalSpace F₂ E₂)
    fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
    (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
        p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
      TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
        p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)

Tactic:
⟨rfl⟩

Premises used: Topology.IsInducing.mk, rfl
-- Module: Mathlib.Topology.FiberBundle.Constructions
Goal:
B : Type u_1
inst : TopologicalSpace B
F₁ : Type u_2
inst_1 : TopologicalSpace F₁
E₁ : B → Type u_3
inst_2 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_4
inst_3 : TopologicalSpace F₂
E₂ : B → Type u_5
inst_4 : TopologicalSpace (TotalSpace F₂ E₂)
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
f₁ : (TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) → TotalSpace F₁ E₁ × TotalSpace F₂ E₂ :=
  fun (p : TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)) ↦
    (TotalSpace.mk (E := E₁) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
        p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).1,
      TotalSpace.mk (E := E₂) (p.proj (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)))
        p.snd (E := fun (x : B) ↦ Prod.{u_3, u_5} (E₁ x) (E₂ x)).2)
f₂ : TotalSpace F₁ E₁ × TotalSpace F₂ E₂ → (B × F₁) × B × F₂ :=
  fun (p : TotalSpace F₁ E₁ × TotalSpace F₂ E₂) ↦
    ((↑e₁ : TotalSpace F₁ E₁ → B × F₁) p.1, (↑e₂ : TotalSpace F₂ E₂ → B × F₂) p.2)
f₃ : (B × F₁) × B × F₂ → B × F₁ × F₂ := fun (p : (B × F₁) × B × F₂) ↦ (p.1.1, p.1.2, p.2.2)
⊢ Continuous[Prod.topologicalSpace F₁ E₁ F₂ E₂, instTopologicalSpaceProd] f₁

Tactic:
have hf₁ : Continuous f₁ := (Prod.isInducing_diag F₁ E₁ F₂ E₂).continuous