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
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))
he' : e' ∈ a.pretrivializationAtlas (E := E)
obtain :
  ∀ (u : Set (B × F)) (hu1 : IsOpen[instTopologicalSpaceProd] u)
    (hu2 :
      (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
          (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source) =
        u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)),
    ∃ (t : Set (B × F)),
      IsOpen[instTopologicalSpaceProd] t ∧
        Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹' t =
          e'.setSymm ⁻¹' ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)
⊢ ∃ (t : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] t ∧
      Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹' t =
        e'.setSymm ⁻¹' ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)

Tactic:
obtain ⟨u, hu1, hu2⟩ := continuousOn_iff'.mp (a.continuous_trivChange _ he _ he') s hs

Premises used: FiberPrebundle.continuous_trivChange, Iff.mp, 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))
he' : e' ∈ a.pretrivializationAtlas (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 :
  (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source) =
    u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
⊢ Eq (α := Set (↑e'.target : Type (max u_2 u_3)))
    ((fun (s : Set (B × F)) ↦
        ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' s : Set (↑e'.target : Type (max u_2 u_3))))
      ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
        (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)))
    ((fun (s : Set (B × F)) ↦
        ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' s : Set (↑e'.target : Type (max u_2 u_3))))
      (u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)))

Tactic:
have hu3 := congr_arg (fun s => (fun x : e'.target => (x : B × F)) ⁻¹' s) hu2
-- 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))
he' : e' ∈ a.pretrivializationAtlas (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 :
  (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source) =
    u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
hu3 :
  Eq (α := Set (↑e'.target : Type (max u_2 u_3)))
    ((fun (s : Set (B × F)) ↦
        ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' s : Set (↑e'.target : Type (max u_2 u_3))))
      ((↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
        (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)))
    ((fun (s : Set (B × F)) ↦
        ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' s : Set (↑e'.target : Type (max u_2 u_3))))
      (u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)))
⊢ Eq (α := Set (↑e'.target : Type (max u_2 u_3)))
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' u ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)

Tactic:
simp only [Subtype.coe_preimage_self, preimage_inter, univ_inter] at hu3

Premises used: Set.preimage_inter, Subtype.coe_preimage_self, Set.univ_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
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 :
  (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source) =
    u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
hu3 :
  Eq (α := Set (↑e'.target : Type (max u_2 u_3)))
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' u ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
simp :
  (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source =
    e'.setSymm ⁻¹' (↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e'.setSymm ⁻¹' e.source
⊢ Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹'
      (u ∩ e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source) =
    e'.setSymm ⁻¹' ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)

Tactic:
simp only [preimage_inter, inter_univ, Subtype.coe_preimage_self, hu3.symm]

Premises used: Set.preimage_inter, Subtype.coe_preimage_self, Set.inter_univ, Eq.symm
-- 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))
he' : e' ∈ a.pretrivializationAtlas (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 :
  (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source) =
    u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
hu3 :
  Eq (α := Set (↑e'.target : Type (max u_2 u_3)))
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' u ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
⊢ (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source =
    e'.setSymm ⁻¹' (↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e'.setSymm ⁻¹' 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)
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 :
  (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source) =
    u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
hu3 :
  Eq (α := Set (↑e'.target : Type (max u_2 u_3)))
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' u ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
refine : IsOpen[instTopologicalSpaceProd] (u ∩ e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
⊢ ∃ (t : Set (B × F)),
    IsOpen[instTopologicalSpaceProd] t ∧
      Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹' t =
        e'.setSymm ⁻¹' ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)

Tactic:
refine ⟨u ∩ e'.toPartialEquiv.target ∩ e'.toPartialEquiv.symm ⁻¹' e.source, ?_, by
        simp only [preimage_inter, inter_univ, Subtype.coe_preimage_self, hu3.symm]; 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)
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 :
  (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source) =
    u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
hu3 :
  Eq (α := Set (↑e'.target : Type (max u_2 u_3)))
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' u ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
rw : IsOpen[instTopologicalSpaceProd] (u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source))
⊢ IsOpen[instTopologicalSpaceProd] (u ∩ e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)

Tactic:
rw [inter_assoc]

Premises used: 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' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 :
  (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source) =
    u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
hu3 :
  Eq (α := Set (↑e'.target : Type (max u_2 u_3)))
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' u ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
⊢ IsOpen[instTopologicalSpaceProd] (u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source))

Tactic:
hu1.inter (a.isOpen_target_of_mem_pretrivializationAtlas_inter e e' he')

Premises used: FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter, 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
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 :
  (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source) =
    u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
hu3 :
  Eq (α := Set (↑e'.target : Type (max u_2 u_3)))
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹'
        (↑e : TotalSpace F E → B × F) ∘ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' s ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
    ((fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' u ∩
      (fun (x : (↑e'.target : Type (max u_2 u_3))) ↦ (↑x : B × F)) ⁻¹' (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
⊢ IsOpen[instTopologicalSpaceProd] (u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source))

Tactic:
exact hu1.inter (a.isOpen_target_of_mem_pretrivializationAtlas_inter e e' he')

Premises used: FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter, 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
b : B
x : E b
simp : b ∈ (a.pretrivializationAt (E := E) b).baseSet
⊢ TotalSpace.mk (E := E) b x ∈ (a.pretrivializationAt (E := E) b).source

Tactic:
simp only [(a.pretrivializationAt b).source_eq, mem_preimage]

Premises used: Bundle.Pretrivialization.source_eq, FiberPrebundle.pretrivializationAt, 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
b : B
x : E b
⊢ b ∈ (a.pretrivializationAt (E := E) b).baseSet

Tactic:
a.mem_base_pretrivializationAt b

Premises used: 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
b : B
x : E b
⊢ b ∈ (a.pretrivializationAt (E := E) b).baseSet

Tactic:
exact a.mem_base_pretrivializationAt b

Premises used: 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
b : B
⊢ TotalSpace.mk (E := E) b ⁻¹' (a.pretrivializationAt (E := E) b).source = univ

Tactic:
eq_univ_of_forall (a.mem_pretrivializationAt_source b)

Premises used: FiberPrebundle.mem_pretrivializationAt_source, Set.eq_univ_of_forall
-- 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
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) ⋯
rw :
  Continuous[inst_2 b, instTopologicalSpaceProd]
    ((↑e.toOpenPartialHomeomorph : TotalSpace F E → B × F) ∘ TotalSpace.mk (E := E) b)
⊢ Continuous[inst_2 b, a.totalSpaceTopology] (TotalSpace.mk (E := E) b)

Tactic:
rw [e.toOpenPartialHomeomorph.continuous_iff_continuous_comp_left
      (a.totalSpaceMk_preimage_source b)]

Premises used: OpenPartialHomeomorph.continuous_iff_continuous_comp_left, FiberPrebundle.totalSpaceMk_preimage_source, Bundle.Trivialization.toOpenPartialHomeomorph
-- 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
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) ⋯
⊢ Continuous[inst_2 b, instTopologicalSpaceProd]
    ((↑e.toOpenPartialHomeomorph : TotalSpace F E → B × F) ∘ TotalSpace.mk (E := E) b)

Tactic:
continuous_iff_le_induced.2 (a.totalSpaceMk_isInducing b).eq_induced.le

Premises used: Iff.mpr, FiberPrebundle.totalSpaceMk_isInducing, Eq.le, continuous_iff_le_induced, Topology.IsInducing.eq_induced
-- 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
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) :=
  a.trivializationOfMemPretrivializationAtlas (E := E) ⋯
⊢ Continuous[inst_2 b, instTopologicalSpaceProd]
    ((↑e.toOpenPartialHomeomorph : TotalSpace F E → B × F) ∘ TotalSpace.mk (E := E) b)

Tactic:
exact continuous_iff_le_induced.2 (a.totalSpaceMk_isInducing b).eq_induced.le

Premises used: Iff.mpr, FiberPrebundle.totalSpaceMk_isInducing, Eq.le, continuous_iff_le_induced, Topology.IsInducing.eq_induced
-- 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) : TotalSpace F E → B × F) ∘ TotalSpace.mk (E := E) b)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
⊢ 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 ⋯)

Tactic:
rw [← restrict_comp_codRestrict (a.mem_pretrivializationAt_source b)] at h

Premises used: FiberPrebundle.mem_pretrivializationAt_source, Set.restrict_comp_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)
apply : IsInducing (codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source ⋯)
⊢ IsInducing (X := E b) (Y := TotalSpace F E) (TotalSpace.mk (E := E) b)

Tactic:
apply IsInducing.of_codRestrict (a.mem_pretrivializationAt_source b)

Premises used: FiberPrebundle.mem_pretrivializationAt_source, Topology.IsInducing.of_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)
⊢ IsInducing (codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source ⋯)

Tactic:
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