awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) e₂
p : TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
⊢ (↑(continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
        (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
      p =
    (p.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)),
      comp (σ₁₂ := σ) (M₂ := E₂ (p.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))
        (continuousLinearMapAt 𝕜₂ (E := E₂) e₂
          (p.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))
        (p.snd (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)).comp (σ₁₂ := RingHom.id 𝕜₁)
          (symmL 𝕜₁ (E := E₁) e₁
            (p.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))))

Tactic:
rfl

Premises used: Bundle.Trivialization.toFun', rfl
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
x₀ : B
⊢ Eq (α :=
    Trivialization (B := B) (F₁ →SL[σ] F₂) (Z :=
      TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (TotalSpace.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))
    (trivializationAt (F₁ →SL[σ] F₂) (fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x₀)
    (Trivialization.continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) (trivializationAt F₁ E₁ x₀) (trivializationAt F₂ E₂ x₀))

Tactic:
rfl

Premises used: Bundle.Trivialization.continuousLinearMap, Bundle.Pretrivialization.continuousLinearMap, VectorPrebundle.trivializationOfMemPretrivializationAtlas, rfl
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
x₀ : B
x : TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
⊢ (↑(trivializationAt (F₁ →SL[σ] F₂) (fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x₀) :
        (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
      x =
    (x.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)),
      inCoordinates F₁ E₁ F₂ E₂ x₀
        (x.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))) x₀
        (x.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
        (x.snd (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))

Tactic:
rfl

Premises used: Bundle.Trivialization.toFun', ContinuousLinearMap.inCoordinates, rfl
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
x₀ : B
⊢ Eq (α := Set (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
    (PartialEquiv.source
      (OpenPartialHomeomorph.toPartialEquiv
        (Trivialization.toOpenPartialHomeomorph
          (trivializationAt (F₁ →SL[σ] F₂) (fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
            x₀))))
    (TotalSpace.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) ⁻¹'
      (Trivialization.baseSet (trivializationAt F₁ E₁ x₀) ∩ Trivialization.baseSet (trivializationAt F₂ E₂ x₀)))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
x₀ : B
⊢ PartialEquiv.target (α :=
      TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (OpenPartialHomeomorph.toPartialEquiv
        (Trivialization.toOpenPartialHomeomorph
          (trivializationAt (F₁ →SL[σ] F₂) (fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
            x₀))) =
    SProd.sprod (β := Set (F₁ →SL[σ] F₂))
      (Trivialization.baseSet (trivializationAt F₁ E₁ x₀) ∩ Trivialization.baseSet (trivializationAt F₂ E₂ x₀)) univ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
x₀ : B
⊢ Trivialization.baseSet (F := F₁ →SL[σ] F₂) (Z :=
      TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
      (trivializationAt (F₁ →SL[σ] F₂) (fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) x₀) =
    Trivialization.baseSet (trivializationAt F₁ E₁ x₀) ∩ Trivialization.baseSet (trivializationAt F₂ E₂ x₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
M : Type u_8
inst_22 : TopologicalSpace M
f : M → TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
s : Set M
x₀ : M
⊢ ContinuousWithinAt f s x₀ ↔
    ContinuousWithinAt.{u_8, u_3} (Y := B)
        (fun (x : M) ↦ (f x).proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))) s x₀ ∧
      ContinuousWithinAt (Y := F₁ →SL[σ] F₂)
        (fun (x : M) ↦
          inCoordinates F₁ E₁ F₂ E₂
            ((f x₀).proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
            ((f x).proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
            ((f x₀).proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
            ((f x).proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
            ((f x).snd (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))
        s x₀

Tactic:
FiberBundle.continuousWithinAt_totalSpace ..

Premises used: ContinuousLinearMap.comp, FiberBundle.continuousWithinAt_totalSpace, ContinuousLinearMap.inCoordinates
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜₁ (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
inst_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : VectorBundle 𝕜₁ F₁ E₁
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜₂ F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_2, u_7} 𝕜₂ (E₂ x)
inst_21 : RingHomIsometric σ
M : Type u_8
inst_22 : TopologicalSpace M
f : M → TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)
x₀ : M
⊢ ContinuousAt f x₀ ↔
    ContinuousAt.{u_8, u_3} (Y := B)
        (fun (x : M) ↦ (f x).proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))) x₀ ∧
      ContinuousAt (Y := F₁ →SL[σ] F₂)
        (fun (x : M) ↦
          inCoordinates F₁ E₁ F₂ E₂
            ((f x₀).proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
            ((f x).proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
            ((f x₀).proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
            ((f x).proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)))
            ((f x).snd (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))))
        x₀

Tactic:
FiberBundle.continuousAt_totalSpace ..

Premises used: ContinuousLinearMap.comp, FiberBundle.continuousAt_totalSpace, ContinuousLinearMap.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)
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)) s
    m₀
hv : ContinuousWithinAt (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk (E := E₁) (b₁ m) (v m)) s m₀
hb₂ : ContinuousWithinAt b₂ s 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)) (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₀
⊢ ContinuousWithinAt (Y := TotalSpace F₂ E₂)
    (fun (m : M) ↦ TotalSpace.mk (E := E₂) (b₂ m) ((ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m))) s m₀

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

Premises used: continuousWithinAt_insert_self
-- 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 (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₀
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₀
⊢ 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₀

Tactic:
rw [FiberBundle.continuousWithinAt_totalSpace] at hv ⊢

Premises used: FiberBundle.continuousWithinAt_totalSpace
-- 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₀
⊢ 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:
⟨hb₂, ?_⟩

Premises used: And.intro