awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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 (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk (E := E₁) (b₁ m) (v m)) (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
⊢ ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk (E := E₂) (b₂ m) ((ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m))) (insert m₀ s) m₀
have rw : ∀
  (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₀),
  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: rw [FiberBundle.continuousWithinAt_totalSpace] at hv ⊢
Cleared hypotheses: hv, hb₂
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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₀
⊢ 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₀
have 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₀
Tactic: refine ⟨hb₂, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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₀
⊢ 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₀
have 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
Tactic: apply (ContinuousWithinAt.clm_apply hϕ hv.2).congr_of_eventuallyEq_of_mem ?_ (mem_insert m₀ s)
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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₀))
have 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₀)))
Tactic: apply hv.1
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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₀
⊢ 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₀)))
have 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₀))
Tactic: apply (trivializationAt F₁ E₁ (b₁ m₀)).open_baseSet.mem_nhds
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (hypothesis)
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₀
⊢ 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
have A : ∀ᶠ (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₀)
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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₀))
⊢ ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₂ m ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))
have a : Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀)) ∈ 𝓝 (b₂ m₀)
Tactic: apply hb₂
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
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₀))
⊢ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀)) ∈ 𝓝 (b₂ m₀)
have a : b₂ m₀ ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))
Tactic: apply (trivializationAt F₂ E₂ (b₂ m₀)).open_baseSet.mem_nhds
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (hypothesis)
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₀))
⊢ 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
have A' : ∀ᶠ (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 hb₂
    apply (trivializationAt F₂ E₂ (b₂ m₀)).open_baseSet.mem_nhds
    exact FiberBundle.mem_baseSet_trivializationAt' (b₂ m₀)