awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
refine :
  ContinuousWithinAt.{u_13, u_10} (Y := F₂)
    (fun (x : M) ↦
      ((↑(trivializationAt F₂ E₂
                (TotalSpace.proj.{u_12, u_10, u_15} (F := F₂) (E := E₂)
                  (TotalSpace.mk (E := E₂) (b₂ m₀) ((ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀))))) :
            TotalSpace F₂ E₂ → B₂ × F₂)
          (TotalSpace.mk (E := E₂) (b₂ x) ((ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)))).2)
    (insert m₀ s) m₀
⊢ ContinuousWithinAt.{u_13, u_12} (Y := B₂)
      (fun (x : M) ↦
        TotalSpace.proj.{u_12, u_10, u_15} (F := F₂) (E := E₂)
          (TotalSpace.mk (E := E₂) (b₂ x) ((ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x))))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_10} (Y := F₂)
      (fun (x : M) ↦
        ((↑(trivializationAt F₂ E₂
                  (TotalSpace.proj.{u_12, u_10, u_15} (F := F₂) (E := E₂)
                    (TotalSpace.mk (E := E₂) (b₂ m₀) ((ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀))))) :
              TotalSpace F₂ E₂ → B₂ × F₂)
            (TotalSpace.mk (E := E₂) (b₂ x) ((ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)))).2)
      (insert m₀ s) m₀

Tactic:
refine ⟨hb₂, ?_⟩
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
apply :
  Filter.EventuallyEq.{u_13, u_10} (β := F₂) (𝓝[insert m₀ s] m₀)
    (fun (x : M) ↦
      ((↑(trivializationAt F₂ E₂
                (TotalSpace.proj.{u_12, u_10, u_15} (F := F₂) (E := E₂)
                  (TotalSpace.mk (E := E₂) (b₂ m₀) ((ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀))))) :
            TotalSpace F₂ E₂ → B₂ × F₂)
          (TotalSpace.mk (E := E₂) (b₂ x) ((ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)))).2)
    fun (x : M) ↦
    (inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ x) (b₂ m₀) (b₂ x) (ϕ x) : (a : F₁) → F₂)
      ((↑(trivializationAt F₁ E₁
                (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
            TotalSpace F₁ E₁ → B₁ × F₁)
          (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2
⊢ ContinuousWithinAt.{u_13, u_10} (Y := F₂)
    (fun (x : M) ↦
      ((↑(trivializationAt F₂ E₂
                (TotalSpace.proj.{u_12, u_10, u_15} (F := F₂) (E := E₂)
                  (TotalSpace.mk (E := E₂) (b₂ m₀) ((ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀))))) :
            TotalSpace F₂ E₂ → B₂ × F₂)
          (TotalSpace.mk (E := E₂) (b₂ x) ((ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)))).2)
    (insert m₀ s) m₀

Tactic:
apply (ContinuousWithinAt.clm_apply hϕ hv.2).congr_of_eventuallyEq_of_mem ?_ (mem_insert m₀ s)

Premises used: ContinuousWithinAt.clm_apply, And.right, Set.mem_insert, ContinuousWithinAt.congr_of_eventuallyEq_of_mem
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
a :
  Membership.mem (γ := Filter B₁)
    (𝓝
      ((fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x))) m₀))
    (Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀)))
⊢ ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))

Tactic:
apply hv.1

Premises used: And.left
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
a :
  (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x))) m₀ ∈
    Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
⊢ Membership.mem (γ := Filter B₁)
    (𝓝
      ((fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x))) m₀))
    (Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀)))

Tactic:
apply (trivializationAt F₁ E₁ (b₁ m₀)).open_baseSet.mem_nhds

Premises used: Bundle.Trivialization.open_baseSet, FiberBundle.trivializationAt, IsOpen.mem_nhds
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
⊢ (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x))) m₀ ∈
    Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))

Tactic:
FiberBundle.mem_baseSet_trivializationAt' (b₁ m₀)

Premises used: FiberBundle.mem_baseSet_trivializationAt', Set.Mem
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
⊢ (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x))) m₀ ∈
    Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))

Tactic:
exact FiberBundle.mem_baseSet_trivializationAt' (b₁ m₀)

Premises used: FiberBundle.mem_baseSet_trivializationAt'
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
⊢ ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))

Tactic:
have A : ∀ᶠ m in 𝓝[insert m₀ s] m₀, b₁ m ∈ (trivializationAt F₁ E₁ (b₁ m₀)).baseSet := by
    apply hv.1
    apply (trivializationAt F₁ E₁ (b₁ m₀)).open_baseSet.mem_nhds
    exact FiberBundle.mem_baseSet_trivializationAt' (b₁ m₀)
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
A : ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
a : Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀)) ∈ 𝓝 (b₂ m₀)
⊢ ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₂ m ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))

Tactic:
apply hb₂
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
A : ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
a : b₂ m₀ ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))
⊢ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀)) ∈ 𝓝 (b₂ m₀)

Tactic:
apply (trivializationAt F₂ E₂ (b₂ m₀)).open_baseSet.mem_nhds

Premises used: Bundle.Trivialization.open_baseSet, FiberBundle.trivializationAt, IsOpen.mem_nhds
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
A : ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
⊢ b₂ m₀ ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))

Tactic:
FiberBundle.mem_baseSet_trivializationAt' (b₂ m₀)

Premises used: FiberBundle.mem_baseSet_trivializationAt', Set.Mem