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
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
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
this : IsOpen[instTopologicalSpaceProd] (f.source ∩ (↑f : B × F → B × F) ⁻¹' s)
⊢ (Z.localTrivAsPartialEquiv i).target ∩
      ((↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹'
          (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s) =
    e.target ∩ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' e'.source ∩
      (↑e' : Z.TotalSpace → B × F) ∘ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' s
have h : (Z.localTrivAsPartialEquiv i).target ∩
    ((↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
      (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ∘
          (↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹'
        s) =
  e.target ∩ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' e'.source ∩
    (↑e' : Z.TotalSpace → B × F) ∘ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' s
Tactic: rw [← preimage_comp, inter_assoc]
-- 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
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
e : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv i
e' : PartialEquiv Z.TotalSpace (B × F) := Z.localTrivAsPartialEquiv j
f : PartialEquiv (B × F) (B × F) := e.symm.trans e'
this : IsOpen[instTopologicalSpaceProd] (f.source ∩ (↑f : B × F → B × F) ⁻¹' s)
h :
  (Z.localTrivAsPartialEquiv i).target ∩
      ((↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ∘
            (↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹'
          s) =
    e.target ∩ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' e'.source ∩
      (↑e' : Z.TotalSpace → B × F) ∘ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' s
⊢ (Z.localTrivAsPartialEquiv i).target ∩
      ((↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹'
          (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s) =
    e.target ∩ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' e'.source ∩
      (↑e' : Z.TotalSpace → B × F) ∘ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' s
have h₁ : (Z.localTrivAsPartialEquiv i).target ∩
    ((↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
      (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ∘
          (↑(Z.localTrivAsPartialEquiv i).symm : B × F → Z.TotalSpace) ⁻¹'
        s) =
  e.target ∩
    ((↑e.symm : B × F → Z.TotalSpace) ⁻¹' e'.source ∩
      (↑e' : Z.TotalSpace → B × F) ∘ (↑e.symm : B × F → Z.TotalSpace) ⁻¹' s)
Tactic: rw [← preimage_comp, inter_assoc]
-- 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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
p : Z.TotalSpace
h : p ∈ (Z.localTrivAsPartialEquiv i).source
⊢ ((↑{ toPartialEquiv := Z.localTrivAsPartialEquiv i, open_source := ⋯, open_target := ⋯, continuousOn_toFun := ⋯,
              continuousOn_invFun := ⋯ : OpenPartialHomeomorph Z.TotalSpace (B × F) } :
          Z.TotalSpace → B × F)
        p).1 =
    Z.proj p
have simp : ((↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) p).1 = p.proj (E := Z.Fiber)
Tactic: simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
⊢ Continuous[inst, _]
    (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
    this)
have refine : ∀ (x : B),
  ContinuousAt (Y := Z.TotalSpace)
    (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
    this)
    x
Tactic: refine continuous_iff_continuousAt.2 fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
⊢ ContinuousAt (Y := Z.TotalSpace)
    (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
    this)
    x
have A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
Tactic: have A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x :=
    IsOpen.mem_nhds (Z.isOpen_baseSet (Z.indexAt x)) (Z.mem_baseSet_at x)
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt (Y := Z.TotalSpace)
    (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
    this)
    x
have refine_1 : (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
    this) ⁻¹'
    (Z.localTrivAt x).source ∈
  𝓝 x
Tactic: refine ((Z.localTrivAt x).toOpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left ?_).2 ?_
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
refine_1 :
  (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
      this) ⁻¹'
      (Z.localTrivAt x).source ∈
    𝓝 x
⊢ ContinuousAt (Y := Z.TotalSpace)
    (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
    this)
    x
have refine_2 : ContinuousAt
  ((↑(Z.localTrivAt x).toOpenPartialHomeomorph : Bundle.TotalSpace F Z.Fiber → B × F) ∘
    have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
    this)
  x
Tactic: refine ((Z.localTrivAt x).toOpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left ?_).2 ?_
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt
    ((↑(Z.localTrivAt x).toOpenPartialHomeomorph : Bundle.TotalSpace F Z.Fiber → B × F) ∘
      have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
      this)
    x
have refine_2 : ContinuousAt.{u_2, u_3} (Y := F)
  (fun (x_1 : B) ↦
    Z.coordChange
      (Z.indexAt
        (TotalSpace.proj (F := F) (E := Z.Fiber)
          ((have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
            this)
            x_1)))
      (Z.indexAt x)
      (TotalSpace.proj (F := F) (E := Z.Fiber)
        ((have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
          this)
          x_1))
      (TotalSpace.snd (E := Z.Fiber)
        ((have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
          this)
          x_1)))
  x
Tactic: apply continuousAt_id.prodMk
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt.{u_2, u_3} (Y := F)
    (fun (x_1 : B) ↦
      Z.coordChange
        (Z.indexAt
          (TotalSpace.proj (F := F) (E := Z.Fiber)
            ((have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
              this)
              x_1)))
        (Z.indexAt x)
        (TotalSpace.proj (F := F) (E := Z.Fiber)
          ((have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
            this)
            x_1))
        (TotalSpace.snd (E := Z.Fiber)
          ((have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
            this)
            x_1)))
    x
have refine_2 : ContinuousAt.{u_2, u_3} (Y := F) (fun (x_1 : B) ↦ Z.coordChange (Z.indexAt x_1) (Z.indexAt x) x_1 v) x
Tactic: simp only [mfld_simps]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (hypothesis)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
⊢ ContinuousAt.{u_2, u_3} (Y := F) (fun (x_1 : B) ↦ Z.coordChange (Z.indexAt x_1) (Z.indexAt x) x_1 v) x
have this : ContinuousOn.{u_2, u_3} (Y := F) (fun (x : B) ↦ v) (Z.baseSet (Z.indexAt x))
Tactic: have : ContinuousOn (fun _ : B => v) (Z.baseSet (Z.indexAt x)) := continuousOn_const
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
A : Z.baseSet (Z.indexAt x) ∈ 𝓝 x
this : ContinuousOn.{u_2, u_3} (Y := F) (fun (x : B) ↦ v) (Z.baseSet (Z.indexAt x))
⊢ ContinuousAt.{u_2, u_3} (Y := F) (fun (x_1 : B) ↦ Z.coordChange (Z.indexAt x_1) (Z.indexAt x) x_1 v) x
have refine_2 : ∀ (y : B) (hy : y ∈ Z.baseSet (Z.indexAt x)), Z.coordChange (Z.indexAt y) (Z.indexAt x) y v = v
Tactic: refine (this.congr fun y hy ↦ ?_).continuousAt A
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
p : Z.TotalSpace
⊢ (↑(Z.localTrivAt (p.proj (E := Z.Fiber))) : Bundle.TotalSpace F Z.Fiber → B × F) p =
    (p.proj (E := Z.Fiber), p.snd (E := Z.Fiber))
have a : p.proj (E := Z.Fiber) ∈ Z.baseSet (Z.indexAt (p.proj (E := Z.Fiber)))
Tactic: rw [localTrivAt, localTriv_apply, coordChange_self]
-- Lean 4 proof step from Mathlib.Topology.FiberBundle.Basic (goal)
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ b ∈ (Z.localTrivAt b).baseSet
have rw : b ∈ Z.baseSet (Z.indexAt b)
Tactic: rw [localTrivAt, ← baseSet_at]
-- 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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x = comap (β := Bundle.TotalSpace F Z.Fiber) (TotalSpace.mk (E := Z.Fiber) b) (𝓝 (TotalSpace.mk (E := Z.Fiber) b x))
have rw : 𝓝 x =
  comap
      ((↑(Z.localTrivAt b).toOpenPartialHomeomorph : Bundle.TotalSpace F Z.Fiber → B × F) ∘
        TotalSpace.mk (E := Z.Fiber) b)
      (𝓝
        ((↑(Z.localTrivAt b).toOpenPartialHomeomorph : Bundle.TotalSpace F Z.Fiber → B × F)
          (TotalSpace.mk (E := Z.Fiber) b x))) ⊓
    𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source)
Tactic: rw [(Z.localTrivAt b).nhds_eq_comap_inf_principal (mk_mem_localTrivAt_source _ _ _), comap_inf,
      comap_principal, comap_comap]
-- 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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x =
    comap
        ((↑(Z.localTrivAt b).toOpenPartialHomeomorph : Bundle.TotalSpace F Z.Fiber → B × F) ∘
          TotalSpace.mk (E := Z.Fiber) b)
        (𝓝
          ((↑(Z.localTrivAt b).toOpenPartialHomeomorph : Bundle.TotalSpace F Z.Fiber → B × F)
            (TotalSpace.mk (E := Z.Fiber) b x))) ⊓
      𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source)
have simp : 𝓝 x = 𝓝 x ⊓ 𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source)
Tactic: simp only [Function.comp_def, localTrivAt_apply_mk, Trivialization.coe_coe,
      ← (isEmbedding_prodMkRight b).nhds_eq_comap]
-- 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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x = 𝓝 x ⊓ 𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source)
have h : 𝓝 x ⊓ 𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source) = 𝓝 x ⊓ 𝓟 univ
Tactic: convert_to 𝓝 x = 𝓝 x ⊓ 𝓟 univ
-- 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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
h : 𝓝 x ⊓ 𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source) = 𝓝 x ⊓ 𝓟 univ
⊢ 𝓝 x = 𝓝 x ⊓ 𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source)
have convert_to : 𝓝 x = 𝓝 x ⊓ 𝓟 univ
Tactic: convert_to 𝓝 x = 𝓝 x ⊓ 𝓟 univ
-- 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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x ⊓ 𝓟 (TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source) = 𝓝 x ⊓ 𝓟 univ
have h : TotalSpace.mk (E := Z.Fiber) b ⁻¹' (Z.localTrivAt b).source = univ
Tactic: congr
-- 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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
⊢ 𝓝 x = 𝓝 x ⊓ 𝓟 univ
have rw : 𝓝 x = 𝓝 x ⊓ ⊤
Tactic: rw [principal_univ, inf_top_eq]
-- 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
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b_1 : B
a : F
b : B
x : Z.Fiber b
rw : 𝓝 x = 𝓝 x ⊓ ⊤
⊢ 𝓝 x = 𝓝 x ⊓ 𝓟 univ
have rw₁ : 𝓝 x = 𝓝 x
Tactic: rw [principal_univ, inf_top_eq]
-- 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
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.pretrivializationAtlas (E := E)
⊢ ContinuousOn (↑e.symm : B × F → TotalSpace F E) e.target
have refine : ∀ (z : B × F) (H : z ∈ e.target) (U : Set (TotalSpace F E)) (h : U ∈ 𝓝 ((↑e.symm : B × F → TotalSpace F E) z)),
  coinduced (fun (x : (↑e.target : Type (max u_2 u_3))) ↦ (↑e.symm : B × F → TotalSpace F E) (↑x : B × F))
      inferInstance ≤
    a.totalSpaceTopology (E := E)
Tactic: refine fun z H U h => preimage_nhdsWithin_coinduced' H (le_def.1 (nhds_mono ?_) U h)
-- 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
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
⊢ IsOpen[a.totalSpaceTopology] e.source
have refine : ∀ e' ∈ a.pretrivializationAtlas (E := E), IsOpen[coinduced e'.setSymm instTopologicalSpaceSubtype] e.source
Tactic: refine isOpen_iSup_iff.mpr fun e' => isOpen_iSup_iff.mpr fun _ => ?_
-- 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
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
h : e' ∈ a.pretrivializationAtlas (E := E)
⊢ IsOpen[coinduced e'.setSymm instTopologicalSpaceSubtype] e.source
have refine : Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹' e.target = e'.setSymm ⁻¹' e.source
Tactic: refine isOpen_coinduced.mpr (isOpen_induced_iff.mpr ⟨e.target, e.open_target, ?_⟩)
-- 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
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
h : e' ∈ a.pretrivializationAtlas (E := E)
⊢ Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹' e.target = e'.setSymm ⁻¹' e.source
have h : ∀ (x : B × F) (hx : x ∈ e'.target),
  Membership.mem (γ := Set (↑e'.target : Type (max u_2 u_3)))
      (Subtype.val (p := fun (x : B × F) ↦ x ∈ e'.target) ⁻¹' e.target)
      (Subtype.mk (p := fun (x : B × F) ↦ x ∈ e'.target) x hx) ↔
    Subtype.mk (p := fun (x : B × F) ↦ x ∈ e'.target) x hx ∈ e'.setSymm ⁻¹' e.source
Tactic: ext ⟨x, hx⟩
-- 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
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
⊢ IsOpen[instTopologicalSpaceProd] (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
have obtain : ∀ (u : Set (B × F)) (hu1 : IsOpen[instTopologicalSpaceProd] u)
  (hu2 : (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source ∩ e'.target = u ∩ e'.target),
  IsOpen[instTopologicalSpaceProd] (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
Tactic: obtain ⟨u, hu1, hu2⟩ := continuousOn_iff'.mp (a.continuous_symm_of_mem_pretrivializationAtlas he')
    e.source (a.isOpen_source e)
-- 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
e e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.pretrivializationAtlas (E := E)
this : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
u : Set (B × F)
hu1 : IsOpen[instTopologicalSpaceProd] u
hu2 : (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source ∩ e'.target = u ∩ e'.target
⊢ IsOpen[instTopologicalSpaceProd] (e'.target ∩ (↑e'.symm : B × F → TotalSpace F E) ⁻¹' e.source)
have rw : IsOpen[instTopologicalSpaceProd] (u ∩ e'.target)
Tactic: rw [inter_comm, hu2]
-- 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.toPartialEquiv : TotalSpace F E → B × F) ⁻¹' s ∩ e.source =
    (↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source ∩ e.source
have rw : (↑e.toPartialEquiv : TotalSpace F E → B × F) ⁻¹' s ∩ e.source = (↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source
Tactic: rw [inter_assoc, inter_self]
-- 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)
⊢ ContinuousOn (↑e.toPartialEquiv : TotalSpace F E → B × F) e.source
have refine : ∀ (s : Set (B × F)) (hs : IsOpen[instTopologicalSpaceProd] s)
  (e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))),
  IsOpen[⨆ (_ : e' ∈ a.pretrivializationAtlas), coinduced e'.setSymm instTopologicalSpaceSubtype]
    ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)
Tactic: refine continuousOn_iff'.mpr fun s hs => ⟨e ⁻¹' s ∩ e.source,
        isOpen_iSup_iff.mpr fun e' => ?_, by rw [inter_assoc, inter_self]; rfl⟩
-- 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))
⊢ IsOpen[⨆ (_ : e' ∈ a.pretrivializationAtlas), coinduced e'.setSymm instTopologicalSpaceSubtype]
    ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)
have refine : ∀ (he' : e' ∈ a.pretrivializationAtlas (E := E)),
  IsOpen[coinduced e'.setSymm instTopologicalSpaceSubtype] ((↑e : TotalSpace F E → B × F) ⁻¹' s ∩ e.source)
Tactic: refine isOpen_iSup_iff.mpr fun he' => ?_