awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_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'
rw :
  IsOpen[instTopologicalSpaceProd]
    ((Z.trivChange i j).source ∩ (↑(Z.trivChange i j).toPartialEquiv : B × F → B × F) ⁻¹' s)
⊢ IsOpen[instTopologicalSpaceProd] (f.source ∩ (↑f : B × F → B × F) ⁻¹' s)

Tactic:
rw [PartialEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsPartialEquiv_trans i j)]

Premises used: PartialEquiv.EqOnSource.source_inter_preimage_eq, FiberBundleCore.localTrivAsPartialEquiv_trans
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
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'
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.trivChange i j).source ∩ (↑(Z.trivChange i j).toPartialEquiv : B × F → B × F) ⁻¹' s)

Tactic:
(continuousOn_open_iff (Z.trivChange i j).open_source).1
        (Z.trivChange i j).continuousOn _ s_open

Premises used: OpenPartialHomeomorph.open_source, FiberBundleCore.trivChange, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.continuousOn, Iff.mp, continuousOn_open_iff
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
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'
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.trivChange i j).source ∩ (↑(Z.trivChange i j).toPartialEquiv : B × F → B × F) ⁻¹' s)

Tactic:
exact (continuousOn_open_iff (Z.trivChange i j).open_source).1
        (Z.trivChange i j).continuousOn _ s_open

Premises used: OpenPartialHomeomorph.open_source, FiberBundleCore.trivChange, OpenPartialHomeomorph.continuousOn, Iff.mp, continuousOn_open_iff
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
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'
⊢ IsOpen[instTopologicalSpaceProd] (f.source ∩ (↑f : B × F → B × F) ⁻¹' s)

Tactic:
have : IsOpen (f.source ∩ f ⁻¹' s) := by
      rw [PartialEquiv.EqOnSource.source_inter_preimage_eq (Z.localTrivAsPartialEquiv_trans i j)]
      exact (continuousOn_open_iff (Z.trivChange i j).open_source).1
        (Z.trivChange i j).continuousOn _ s_open
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
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)
⊢ IsOpen[instTopologicalSpaceProd] (f.source ∩ (↑f : B × F → B × F) ⁻¹' s)

Tactic:
this
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
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).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s) =
    f.source ∩ (↑f : B × F → B × F) ⁻¹' s
⊢ IsOpen[instTopologicalSpaceProd]
    ((Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s))

Tactic:
convert! this using 1
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
t : Set Z.TotalSpace
j : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
ts : t = (Z.localTrivAsPartialEquiv j).source ∩ (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s
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 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
⊢ (Z.localTrivAsPartialEquiv i).target ∩
      ((Z.localTrivAsPartialEquiv i).invFun ⁻¹' (Z.localTrivAsPartialEquiv j).source ∩
        (Z.localTrivAsPartialEquiv i).invFun ⁻¹' (↑(Z.localTrivAsPartialEquiv j) : Z.TotalSpace → B × F) ⁻¹' s) =
    f.source ∩ (↑f : B × F → B × F) ⁻¹' s

Tactic:
dsimp [f, PartialEquiv.trans_source]

Premises used: PartialEquiv.trans_source
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
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
h₁ 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

Tactic:
rw [← preimage_comp, inter_assoc]

Premises used: Set.preimage_comp, 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
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
simp : ((↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) p).1 = p.proj (E := Z.Fiber)
⊢ ((↑{ 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

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace F
Z : FiberBundleCore ι B F
i_1 : ι
b : B
a : F
i : ι
p : Z.TotalSpace
h : p ∈ (Z.localTrivAsPartialEquiv i).source
⊢ ((↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) p).1 = p.proj (E := Z.Fiber)

Tactic:
rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
⊢ Z.localTriv (Z.indexAt b) = Z.localTrivAt b

Tactic:
rfl

Premises used: FiberBundleCore.localTrivAt, rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
b : B
p : Bundle.TotalSpace F Z.Fiber
⊢ ((↑(Z.localTrivAt b) : Bundle.TotalSpace F Z.Fiber → B × F) p).2 =
    Z.coordChange (Z.indexAt (p.proj (E := Z.Fiber))) (Z.indexAt b) (p.proj (E := Z.Fiber)) (p.snd (E := Z.Fiber))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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)

Tactic:
continuous_iff_continuousAt.2 fun x => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
refine :
  ∀ (x : B),
    ContinuousAt (Y := Z.TotalSpace)
      (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
      this)
      x
⊢ Continuous[inst, _]
    (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
    this)

Tactic:
refine continuous_iff_continuousAt.2 fun x => ?_

Premises used: Iff.mpr, continuous_iff_continuousAt
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
v : F
h : ∀ (i j : ι), ∀ x ∈ Z.baseSet i ∩ Z.baseSet j, Z.coordChange i j x v = v
x : B
⊢ 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)
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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

Tactic:
((Z.localTrivAt x).toOpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left ?_).2 ?_

Premises used: Iff.mpr, OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left, FiberBundleCore.localTrivAt, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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
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
⊢ ContinuousAt (Y := Z.TotalSpace)
    (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 ?_

Premises used: Iff.mpr, OpenPartialHomeomorph.continuousAt_iff_continuousAt_comp_left, FiberBundleCore.localTrivAt, Bundle.Trivialization.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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
⊢ (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
      this) ⁻¹'
      (Z.localTrivAt x).source ∈
    𝓝 x

Tactic:
A

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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
⊢ (have this : B → Z.TotalSpace := fun (x : B) ↦ TotalSpace.mk (E := Z.Fiber) x v;
      this) ⁻¹'
      (Z.localTrivAt x).source ∈
    𝓝 x

Tactic:
exact A
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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_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
⊢ 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:
apply continuousAt_id.prodMk

Premises used: ContinuousAt.prodMk, continuousAt_id
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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_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
⊢ 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:
simp only [mfld_simps]
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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
⊢ 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
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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

Tactic:
(this.congr fun y hy ↦ ?_).continuousAt A

Premises used: ContinuousOn.congr, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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))
refine_2 : ∀ (y : B) (hy : y ∈ Z.baseSet (Z.indexAt x)), Z.coordChange (Z.indexAt y) (Z.indexAt x) y v = v
⊢ 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:
refine (this.congr fun y hy ↦ ?_).continuousAt A

Premises used: ContinuousOn.congr, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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))
y : B
hy : y ∈ Z.baseSet (Z.indexAt x)
⊢ Z.coordChange (Z.indexAt y) (Z.indexAt x) y v = v

Tactic:
h _ _ _ ⟨mem_baseSet_at _ _, hy⟩

Premises used: And.intro, FiberBundleCore.mem_baseSet_at
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
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))
y : B
hy : y ∈ Z.baseSet (Z.indexAt x)
⊢ Z.coordChange (Z.indexAt y) (Z.indexAt x) y v = v

Tactic:
exact h _ _ _ ⟨mem_baseSet_at _ _, hy⟩

Premises used: And.intro, FiberBundleCore.mem_baseSet_at
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ (↑(Z.localTrivAsPartialEquiv i) : Z.TotalSpace → B × F) = (↑(Z.localTriv i) : Z.TotalSpace → B × F)

Tactic:
rfl

Premises used: Bundle.Trivialization.toFun', rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ (Z.localTrivAsPartialEquiv i).source = (Z.localTriv i).source

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ (Z.localTrivAsPartialEquiv i).target = (Z.localTriv i).target

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ (Z.localTrivAsPartialEquiv i).symm = (Z.localTriv i).symm

Tactic:
rfl

Premises used: FiberBundleCore.localTrivAsPartialEquiv, rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ Z.baseSet i = (Z.localTriv i).baseSet

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : Z.TotalSpace
⊢ (↑(Z.localTriv i) : Z.TotalSpace → B × F) p =
    (p.proj (E := Z.Fiber),
      Z.coordChange (Z.indexAt (p.proj (E := Z.Fiber))) i (p.proj (E := Z.Fiber)) (p.snd (E := Z.Fiber)))

Tactic:
rfl

Premises used: Bundle.Trivialization.toFun', rfl
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
p : Z.TotalSpace
a : p.proj (E := Z.Fiber) ∈ Z.baseSet (Z.indexAt (p.proj (E := Z.Fiber)))
⊢ (↑(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))

Tactic:
rw [localTrivAt, localTriv_apply, coordChange_self]

Premises used: FiberBundleCore.coordChange_self, FiberBundleCore.localTriv_apply, FiberBundleCore.localTrivAt
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
p : Z.TotalSpace
⊢ p.proj (E := Z.Fiber) ∈ Z.baseSet (Z.indexAt (p.proj (E := Z.Fiber)))

Tactic:
Z.mem_baseSet_at p.1

Premises used: Bundle.TotalSpace.proj, FiberBundleCore.mem_baseSet_at
-- Module: Mathlib.Topology.FiberBundle.Basic
Goal:
ι : Type u_1
B : Type u_2
F : Type u_3
inst : TopologicalSpace B
inst_1 : TopologicalSpace F
Z : FiberBundleCore ι B F
p : Z.TotalSpace
⊢ p.proj (E := Z.Fiber) ∈ Z.baseSet (Z.indexAt (p.proj (E := Z.Fiber)))

Tactic:
exact Z.mem_baseSet_at p.1

Premises used: Bundle.TotalSpace.proj, FiberBundleCore.mem_baseSet_at