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₀
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:
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₀
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₀))

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₀)
-- 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' : ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₂ m ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))
m : M
hm : b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
h'm : b₂ m ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))
⊢ ((↑(trivializationAt F₂ E₂ (b₂ m₀)) : TotalSpace F₂ E₂ → B₂ × F₂)
        (TotalSpace.mk (E := E₂) (b₂ m) ((ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m)))).2 =
    (inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m) : (a : F₁) → F₂)
      ((↑(trivializationAt F₁ E₁ (b₁ m₀)) : TotalSpace F₁ E₁ → B₁ × F₁) (TotalSpace.mk (E := E₁) (b₁ m) (v m))).2

Tactic:
simp [inCoordinates_eq hm h'm, hm]

Premises used: ContinuousLinearMap.inCoordinates_eq
-- 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)
hϕ : ContinuousAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : ContinuousAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk (E := E₁) (b₁ m) (v m)) m₀
hb₂ : ContinuousAt b₂ m₀
rw :
  ∀
    (hϕ :
      ContinuousWithinAt (Y := F₁ →L[𝕜] F₂)
        (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) univ m₀)
    (hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk (E := E₁) (b₁ m) (v m)) univ m₀)
    (hb₂ : ContinuousWithinAt b₂ univ 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))) univ m₀
⊢ ContinuousAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk (E := E₂) (b₂ m) ((ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m))) m₀

Tactic:
rw [← continuousWithinAt_univ] at hϕ hv hb₂ ⊢

Premises used: continuousWithinAt_univ
-- 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)
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    univ m₀
hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk (E := E₁) (b₁ m) (v m)) univ m₀
hb₂ : ContinuousWithinAt b₂ univ 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))) univ m₀

Tactic:
hϕ.clm_apply_of_inCoordinates hv hb₂

Premises used: ContinuousWithinAt.clm_apply_of_inCoordinates
-- 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)
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    univ m₀
hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk (E := E₁) (b₁ m) (v m)) univ m₀
hb₂ : ContinuousWithinAt b₂ univ 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))) univ m₀

Tactic:
exact hϕ.clm_apply_of_inCoordinates hv hb₂

Premises used: ContinuousWithinAt.clm_apply_of_inCoordinates
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
M : Type u_13
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
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)
E₂ : B → Type u_15
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 M
inst_15 : FiberBundle F₁ E₁
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_15} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_8, u_15} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hϕ :
  ContinuousWithinAt (Y :=
    TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
        (F₁ →L[𝕜] F₂) (b m) (ϕ m))
    s x
hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) s x
⊢ ContinuousWithinAt.{u_13, u_9} (Y := B) (fun (x : M) ↦ b x) s x ∧
    ContinuousWithinAt (Y := F₁ →L[𝕜] F₂)
      (fun (x_1 : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b x) (b x_1) (b x) (b x_1) (ϕ x_1)) s x

Tactic:
simp only [continuousWithinAt_hom_bundle] at hϕ

Premises used: continuousWithinAt_hom_bundle
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
M : Type u_13
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
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)
E₂ : B → Type u_15
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 M
inst_15 : FiberBundle F₁ E₁
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_15} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_8, u_15} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) s x
hϕ :
  ContinuousWithinAt.{u_13, u_9} (Y := B) (fun (x : M) ↦ b x) s x ∧
    ContinuousWithinAt (Y := F₁ →L[𝕜] F₂)
      (fun (x_1 : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b x) (b x_1) (b x) (b x_1) (ϕ x_1)) s x
⊢ ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))) s x

Tactic:
hϕ.2.clm_apply_of_inCoordinates hv hϕ.1

Premises used: ContinuousWithinAt.clm_apply_of_inCoordinates, And.right, And.left
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
M : Type u_13
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
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)
E₂ : B → Type u_15
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 M
inst_15 : FiberBundle F₁ E₁
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_15} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_8, u_15} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) s x
hϕ :
  ContinuousWithinAt.{u_13, u_9} (Y := B) (fun (x : M) ↦ b x) s x ∧
    ContinuousWithinAt (Y := F₁ →L[𝕜] F₂)
      (fun (x_1 : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b x) (b x_1) (b x) (b x_1) (ϕ x_1)) s x
⊢ ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))) s x

Tactic:
exact hϕ.2.clm_apply_of_inCoordinates hv hϕ.1

Premises used: ContinuousWithinAt.clm_apply_of_inCoordinates, And.right, And.left
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
M : Type u_13
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
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)
E₂ : B → Type u_15
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 M
inst_15 : FiberBundle F₁ E₁
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
x : M
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_15} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_8, u_15} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hϕ :
  ContinuousAt (Y :=
    TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
        (F₁ →L[𝕜] F₂) (b m) (ϕ m))
    x
hv : ContinuousAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) x
simp :
  ∀
    (hϕ :
      ContinuousWithinAt (Y :=
        TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
        (fun (m : M) ↦
          TotalSpace.mk' (E := fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
            (F₁ →L[𝕜] F₂) (b m) (ϕ m))
        univ x)
    (hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ x),
    ContinuousWithinAt (Y := TotalSpace F₂ E₂)
      (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))) univ x
⊢ ContinuousAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))) x

Tactic:
simp only [← continuousWithinAt_univ] at hϕ hv ⊢

Premises used: continuousWithinAt_univ
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
M : Type u_13
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
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)
E₂ : B → Type u_15
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 M
inst_15 : FiberBundle F₁ E₁
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
x : M
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_15} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_8, u_15} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hϕ :
  ContinuousWithinAt (Y :=
    TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
        (F₁ →L[𝕜] F₂) (b m) (ϕ m))
    univ x
hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ x
⊢ ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))) univ x

Tactic:
hϕ.clm_bundle_apply hv

Premises used: ContinuousWithinAt.clm_bundle_apply
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
M : Type u_13
inst : NontriviallyNormedField 𝕜
E₁ : B → Type u_14
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)
E₂ : B → Type u_15
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 M
inst_15 : FiberBundle F₁ E₁
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
b : M → B
v : (x : M) → E₁ (b x)
x : M
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_15} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_8, u_15} 𝕜 (E₂ x)
ϕ : (x : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b x)) (E₂ (b x))
hϕ :
  ContinuousWithinAt (Y :=
    TotalSpace (F₁ →L[𝕜] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ x) (E₂ x))
        (F₁ →L[𝕜] F₂) (b m) (ϕ m))
    univ x
hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ x
⊢ ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))) univ x

Tactic:
exact hϕ.clm_bundle_apply hv

Premises used: ContinuousWithinAt.clm_bundle_apply