awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨u, hu1, hu2⟩ := continuousOn_iff'.mp (a.continuous_trivChange _ he _ he') s hs
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
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)
⊢ ∃ (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)
have 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)))
Tactic: have hu3 := congr_arg (fun s => (fun x : e'.target => (x : B × F)) ⁻¹' s) hu2
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
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)))
⊢ ∃ (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)
have 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)
Tactic: simp only [Subtype.coe_preimage_self, preimage_inter, univ_inter] at hu3
Cleared hypotheses: hu3
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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)
⊢ 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)
have 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
Tactic: simp only [preimage_inter, inter_univ, Subtype.coe_preimage_self, hu3.symm]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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)
⊢ ∃ (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)
have refine : IsOpen[instTopologicalSpaceProd] (u ∩ e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' 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⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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)
have rw : IsOpen[instTopologicalSpaceProd] (u ∩ (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source))
Tactic: rw [inter_assoc]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ TotalSpace.mk (E := E) b x ∈ (a.pretrivializationAt (E := E) b).source
have simp : b ∈ (a.pretrivializationAt (E := E) b).baseSet
Tactic: simp only [(a.pretrivializationAt b).source_eq, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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, a.totalSpaceTopology] (TotalSpace.mk (E := E) b)
have rw : Continuous[inst_2 b, instTopologicalSpaceProd]
  ((↑e.toOpenPartialHomeomorph : TotalSpace F E → B × F) ∘ TotalSpace.mk (E := E) b)
Tactic: rw [e.toOpenPartialHomeomorph.continuous_iff_continuous_comp_left
      (a.totalSpaceMk_preimage_source b)]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
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 (X := E b) (Y := TotalSpace F E) (TotalSpace.mk (E := E) b)
have 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 sorry)
Tactic: rw [← restrict_comp_codRestrict (a.mem_pretrivializationAt_source b)] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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 (X := E b) (Y := TotalSpace F E) (TotalSpace.mk (E := E) b)
have apply : IsInducing (codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source sorry)
Tactic: apply IsInducing.of_codRestrict (a.mem_pretrivializationAt_source b)
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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 ⋯)
have refine : Continuous[inst_2 b, instTopologicalSpaceSubtype]
  (codRestrict (TotalSpace.mk (E := E) b) (a.pretrivializationAt (E := E) b).source sorry)
Tactic: refine h.of_comp ?_ (continuousOn_iff_continuous_restrict.mp
    (a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b)).continuousOn)
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
have refine_1 : z.proj (E := E) ∈ e.baseSet
Tactic: refine (e.continuousAt_of_comp_right ?_
    ((hf z.proj hz).continuousAt (IsOpen.mem_nhds ?_ ?_))).continuousWithinAt
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ContinuousWithinAt f (TotalSpace.proj (E := E) ⁻¹' s) z
have refine_2 : IsOpen[instTopologicalSpaceProd]
  (SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet) univ)
Tactic: refine (e.continuousAt_of_comp_right ?_
    ((hf z.proj hz).continuousAt (IsOpen.mem_nhds ?_ ?_))).continuousWithinAt
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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)
⊢ ContinuousWithinAt f (TotalSpace.proj (E := E) ⁻¹' s) z
have refine_3 : (↑e : TotalSpace F E → B × F) z ∈
  SProd.sprod (β := Set F) (s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet) univ
Tactic: refine (e.continuousAt_of_comp_right ?_
    ((hf z.proj hz).continuousAt (IsOpen.mem_nhds ?_ ?_))).continuousWithinAt
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
have refine_3 : ((↑e : TotalSpace F E → B × F) z).1 ∈ s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet
Tactic: refine ⟨?_, mem_univ _⟩
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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).1 ∈ s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet
have refine_3 : z.proj (E := E) ∈ s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet
Tactic: rw [e.coe_fst]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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
⊢ ((↑e : TotalSpace F E → B × F) z).1 ∈ s ∩ (a.pretrivializationAt (E := E) (z.proj (E := E))).baseSet
have refine_3₁ : z ∈ e.source
Tactic: rw [e.coe_fst]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
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 ∈ e.source
have refine_3 : z.proj (E := E) ∈ e.baseSet
Tactic: rw [e.mem_source]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Constructions (goal)
Goal:
B : Type u_1
F : Type u_2
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
⊢ topologicalSpace B F =
    induced (Y := B × F) (⇑(TotalSpace.toProd B F) : (a : TotalSpace F fun (x : B) ↦ F) → B × F)
      instTopologicalSpaceProd
have 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
Tactic: simp only [instTopologicalSpaceProd, induced_inf, induced_compose]