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₁_1 e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂_1 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 σ
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
he₁ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
e₂ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) he₁
⊢ Pretrivialization.IsLinear 𝕜₂ (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
    ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ he₁)

Tactic:
infer_instance
-- 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₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := 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 σ
b : B
L₁ : ContinuousLinearEquiv.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁ :=
  Trivialization.continuousLinearEquivAt 𝕜₁ (E := E₁) (trivializationAt F₁ E₁ b) b ⋯
L₂ : ContinuousLinearEquiv.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
φ : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
⊢ IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
    (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)

Tactic:
have : IsInducing fun x ↦ (b, φ x) := isInducing_const_prod.mpr φ.toHomeomorph.isInducing
-- 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₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := 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 σ
b : B
L₁ : ContinuousLinearEquiv.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁ :=
  Trivialization.continuousLinearEquivAt 𝕜₁ (E := E₁) (trivializationAt F₁ E₁ b) b ⋯
L₂ : ContinuousLinearEquiv.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
φ : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
this :
  IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
    (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
⊢ IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
    (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)

Tactic:
this
-- 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₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := 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 σ
b : B
L₁ : ContinuousLinearEquiv.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁ :=
  Trivialization.continuousLinearEquivAt 𝕜₁ (E := E₁) (trivializationAt F₁ E₁ b) b ⋯
L₂ : ContinuousLinearEquiv.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
φ : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
this :
  IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
    (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
h :
  ∀ (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)),
    Eq (α := F₁ →SL[σ] F₂)
      (Function.comp (β :=
          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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
            (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
          (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
            ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) b)
          x).2
      ((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
⊢ IsInducing (X := ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) (Y := B × (F₁ →SL[σ] F₂))
    (Function.comp (β :=
      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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
        (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
      (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
        b))

Tactic:
convert! this
-- 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₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := 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 σ
b : B
L₁ : ContinuousLinearEquiv.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁ :=
  Trivialization.continuousLinearEquivAt 𝕜₁ (E := E₁) (trivializationAt F₁ E₁ b) b ⋯
L₂ : ContinuousLinearEquiv.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
φ : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
this :
  IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
    (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)
h :
  ∀ (f : F₁),
    Eq.{u_6 + 1} (α := F₂)
      (((Function.comp (β :=
                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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
                  (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
                (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                  ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) b)
                x).2 :
            (a : F₁) → F₂)
          f :
        F₂)
      ((((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x : F₁ →SL[σ] F₂) : (a : F₁) → F₂) f : F₂)
⊢ Eq (α := F₁ →SL[σ] F₂)
    (Function.comp (β :=
        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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
          (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
        (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x))
          b)
        x).2
    ((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)

Tactic:
ext f
-- 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₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := 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 σ
b : B
L₁ : ContinuousLinearEquiv.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁ :=
  Trivialization.continuousLinearEquivAt 𝕜₁ (E := E₁) (trivializationAt F₁ E₁ b) b ⋯
L₂ : ContinuousLinearEquiv.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
φ : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
this :
  IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
    (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)
f : F₁
h :
  Eq.{u_6 + 1} (α := F₂)
    (((Trivialization.linearMapAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b :
            LinearMap.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂) :
          (a : E₂ b) → F₂)
        ((x : (a : E₁ b) → E₂ b) (Trivialization.symm (E := E₁) (trivializationAt F₁ E₁ b) b f) : E₂ b) :
      F₂)
    ((((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x : F₁ →SL[σ] F₂) : (a : F₁) → F₂) f : F₂)
⊢ Eq.{u_6 + 1} (α := F₂)
    (((Function.comp (β :=
              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₂) (trivializationAt F₁ E₁ b) (trivializationAt F₂ E₂ b)) :
                (TotalSpace (F₁ →SL[σ] F₂) fun (x : B) ↦ E₁ x →SL[σ] E₂ x) → B × (F₁ →SL[σ] F₂))
              (TotalSpace.mk (F := F₁ →SL[σ] F₂) (E := fun (x : B) ↦
                ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)) b)
              x).2 :
          (a : F₁) → F₂)
        f :
      F₂)
    ((((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x : F₁ →SL[σ] F₂) : (a : F₁) → F₂) f : F₂)

Tactic:
dsimp [Pretrivialization.continuousLinearMap_apply]

Premises used: Bundle.Pretrivialization.continuousLinearMap_apply
-- 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₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := 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 σ
b : B
L₁ : ContinuousLinearEquiv.{u_1, u_1, u_5, u_4} (RingHom.id 𝕜₁) (E₁ b) F₁ :=
  Trivialization.continuousLinearEquivAt 𝕜₁ (E := E₁) (trivializationAt F₁ E₁ b) b ⋯
L₂ : ContinuousLinearEquiv.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂ :=
  Trivialization.continuousLinearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯
φ : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b) ≃L[𝕜₂] F₁ →SL[σ] F₂ := L₁.arrowCongrSL L₂
this :
  IsInducing (Y := B × (F₁ →SL[σ] F₂)) fun (x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)) ↦
    (b, (φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x)
x : ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ b) (E₂ b)
f : F₁
⊢ Eq.{u_6 + 1} (α := F₂)
    ((((↑(Trivialization.linearEquivAt 𝕜₂ (E := E₂) (trivializationAt F₂ E₂ b) b ⋯) :
              LinearMap.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂) :
            LinearMap.{u_2, u_2, u_7, u_6} (RingHom.id 𝕜₂) (E₂ b) F₂) :
          (a : E₂ b) → F₂)
        ((x : (a : E₁ b) → E₂ b) (Trivialization.symm (E := E₁) (trivializationAt F₁ E₁ b) b f) : E₂ b) :
      F₂)
    ((((φ : (a : E₁ b →SL[σ] E₂ b) → F₁ →SL[σ] F₂) x : F₁ →SL[σ] F₂) : (a : F₁) → F₂) f : F₂)

Tactic:
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
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := 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 σ
⊢ VectorBundle 𝕜₂ (F₁ →SL[σ] F₂) fun (x : B) ↦ ContinuousLinearMap.{u_1, u_2, u_5, u_7} σ (E₁ x) (E₂ x)

Tactic:
(Bundle.ContinuousLinearMap.vectorPrebundle σ F₁ E₁ F₂ E₂).toVectorBundle

Premises used: VectorPrebundle.toVectorBundle, Bundle.ContinuousLinearMap.vectorPrebundle
-- 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₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := 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₂
⊢ MemTrivializationAtlas (E := E₁) e₁

Tactic:
infer_instance
-- 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₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := 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₂
⊢ MemTrivializationAtlas (E := E₂) e₂

Tactic:
infer_instance
-- 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₂
⊢ 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))
      (continuousLinearMap σ (E₁ := E₁) (E₂ := E₂) e₁ e₂) =
    e₁.baseSet ∩ e₂.baseSet

Tactic:
rfl

Premises used: rfl