awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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ϕ :
  ContinuousOn (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
hv : ContinuousOn (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) s
⊢ ContinuousOn (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

Tactic:
fun x hx ↦ (hϕ x hx).clm_bundle_apply (hv x hx)

Premises used: ContinuousOn, 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)
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ϕ :
  Continuous[inst_14, ContinuousLinearMap.topologicalSpaceTotalSpace (RingHom.id 𝕜) F₁ E₁ F₂ E₂] 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)
hv : Continuous[inst_14, inst_5] fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)
simp :
  ∀
    (hϕ :
      ContinuousOn (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)
    (hv : ContinuousOn (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ),
    ContinuousOn (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
⊢ Continuous[inst_14, inst_11] fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) ((ϕ m : (a : E₁ (b m)) → E₂ (b m)) (v m))

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

Premises used: continuousOn_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)
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ϕ :
  ContinuousOn (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
hv : ContinuousOn (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ
⊢ ContinuousOn (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

Tactic:
hϕ.clm_bundle_apply hv

Premises used: ContinuousOn.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)
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ϕ :
  ContinuousOn (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
hv : ContinuousOn (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ
⊢ ContinuousOn (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

Tactic:
exact hϕ.clm_bundle_apply hv

Premises used: ContinuousOn.clm_bundle_apply
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
F₃ : Type u_12
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)
E₃ : B → Type u_16
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_8, u_16} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
inst_19 : TopologicalSpace B
inst_20 : TopologicalSpace M
inst_21 : FiberBundle F₁ E₁
inst_22 : VectorBundle 𝕜 F₁ E₁
inst_23 : FiberBundle F₂ E₂
inst_24 : VectorBundle 𝕜 F₂ E₂
inst_25 : FiberBundle F₃ E₃
inst_26 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
x : M
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_16} (E₃ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_8, u_16} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ :
  ContinuousWithinAt (Y :=
    TotalSpace (F₁ →L[𝕜] F₂ →L[𝕜] F₃) fun (x : B) ↦
      E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦
        E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) (F₁ →L[𝕜] 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
hw : ContinuousWithinAt (Y := TotalSpace F₂ E₂) (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) (w m)) 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) →L[𝕜] E₃ (b m)) (v m) :
              ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
            (a : E₂ (b m)) → E₃ (b m))
          (w m)))
    s x

Tactic:
(hψ.clm_bundle_apply hv).clm_bundle_apply hw

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
F₃ : Type u_12
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)
E₃ : B → Type u_16
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_8, u_16} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
inst_19 : TopologicalSpace B
inst_20 : TopologicalSpace M
inst_21 : FiberBundle F₁ E₁
inst_22 : VectorBundle 𝕜 F₁ E₁
inst_23 : FiberBundle F₂ E₂
inst_24 : VectorBundle 𝕜 F₂ E₂
inst_25 : FiberBundle F₃ E₃
inst_26 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
x : M
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_16} (E₃ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_8, u_16} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ :
  ContinuousAt (Y :=
    TotalSpace (F₁ →L[𝕜] F₂ →L[𝕜] F₃) fun (x : B) ↦
      E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦
        E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) (F₁ →L[𝕜] 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
hw : ContinuousAt (Y := TotalSpace F₂ E₂) (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) (w m)) x
⊢ ContinuousAt (Y := TotalSpace F₃ E₃)
    (fun (m : M) ↦
      TotalSpace.mk' (E := E₃) F₃ (b m)
        ((((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
              ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
            (a : E₂ (b m)) → E₃ (b m))
          (w m)))
    x

Tactic:
(hψ.clm_bundle_apply hv).clm_bundle_apply hw

Premises used: ContinuousAt.clm_bundle_apply
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
F₃ : Type u_12
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)
E₃ : B → Type u_16
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_8, u_16} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
inst_19 : TopologicalSpace B
inst_20 : TopologicalSpace M
inst_21 : FiberBundle F₁ E₁
inst_22 : VectorBundle 𝕜 F₁ E₁
inst_23 : FiberBundle F₂ E₂
inst_24 : VectorBundle 𝕜 F₂ E₂
inst_25 : FiberBundle F₃ E₃
inst_26 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
s : Set M
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_16} (E₃ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_8, u_16} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ :
  ContinuousOn (Y :=
    TotalSpace (F₁ →L[𝕜] F₂ →L[𝕜] F₃) fun (x : B) ↦
      E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦
        E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m)
        (ψ m))
    s
hv : ContinuousOn (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) s
hw : ContinuousOn (Y := TotalSpace F₂ E₂) (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) (w m)) s
⊢ ContinuousOn (Y := TotalSpace F₃ E₃)
    (fun (m : M) ↦
      TotalSpace.mk' (E := E₃) F₃ (b m)
        ((((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
              ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
            (a : E₂ (b m)) → E₃ (b m))
          (w m)))
    s

Tactic:
fun x hx ↦ (hψ x hx).clm_bundle_apply₂ (hv x hx) (hw x hx)

Premises used: ContinuousWithinAt.clm_bundle_apply₂, ContinuousOn
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
F₃ : Type u_12
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)
E₃ : B → Type u_16
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_8, u_16} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
inst_19 : TopologicalSpace B
inst_20 : TopologicalSpace M
inst_21 : FiberBundle F₁ E₁
inst_22 : VectorBundle 𝕜 F₁ E₁
inst_23 : FiberBundle F₂ E₂
inst_24 : VectorBundle 𝕜 F₂ E₂
inst_25 : FiberBundle F₃ E₃
inst_26 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_16} (E₃ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_8, u_16} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ :
  ContinuousOn (Y :=
    TotalSpace (F₁ →L[𝕜] F₂ →L[𝕜] F₃) fun (x : B) ↦
      E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦
        E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m)
        (ψ m))
    univ
hv : ContinuousOn (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ
hw : ContinuousOn (Y := TotalSpace F₂ E₂) (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) (w m)) univ
⊢ ContinuousOn (Y := TotalSpace F₃ E₃)
    (fun (m : M) ↦
      TotalSpace.mk' (E := E₃) F₃ (b m)
        ((((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
              ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
            (a : E₂ (b m)) → E₃ (b m))
          (w m)))
    univ

Tactic:
hψ.clm_bundle_apply₂ hv hw

Premises used: ContinuousOn.clm_bundle_apply₂
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
F₃ : Type u_12
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)
E₃ : B → Type u_16
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_8, u_16} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
inst_19 : TopologicalSpace B
inst_20 : TopologicalSpace M
inst_21 : FiberBundle F₁ E₁
inst_22 : VectorBundle 𝕜 F₁ E₁
inst_23 : FiberBundle F₂ E₂
inst_24 : VectorBundle 𝕜 F₂ E₂
inst_25 : FiberBundle F₃ E₃
inst_26 : VectorBundle 𝕜 F₃ E₃
b : M → B
v : (x : M) → E₁ (b x)
inst_27 : ∀ (x : B), IsTopologicalAddGroup.{u_16} (E₃ x)
inst_28 : ∀ (x : B), ContinuousSMul.{u_8, u_16} 𝕜 (E₃ x)
ψ : (x : M) → E₁ (b x) →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b x)) (E₃ (b x))
w : (x : M) → E₂ (b x)
hψ :
  ContinuousOn (Y :=
    TotalSpace (F₁ →L[𝕜] F₂ →L[𝕜] F₃) fun (x : B) ↦
      E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x))
    (fun (m : M) ↦
      TotalSpace.mk' (E := fun (x : B) ↦
        E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) (F₁ →L[𝕜] F₂ →L[𝕜] F₃) (b m)
        (ψ m))
    univ
hv : ContinuousOn (Y := TotalSpace F₁ E₁) (fun (m : M) ↦ TotalSpace.mk' (E := E₁) F₁ (b m) (v m)) univ
hw : ContinuousOn (Y := TotalSpace F₂ E₂) (fun (m : M) ↦ TotalSpace.mk' (E := E₂) F₂ (b m) (w m)) univ
⊢ ContinuousOn (Y := TotalSpace F₃ E₃)
    (fun (m : M) ↦
      TotalSpace.mk' (E := E₃) F₃ (b m)
        ((((ψ m : (a : E₁ (b m)) → E₂ (b m) →L[𝕜] E₃ (b m)) (v m) :
              ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ (b m)) (E₃ (b m))) :
            (a : E₂ (b m)) → E₃ (b m))
          (w m)))
    univ

Tactic:
exact hψ.clm_bundle_apply₂ hv hw

Premises used: ContinuousOn.clm_bundle_apply₂
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜 : Type u_8
B : Type u_9
F₁ : Type u_10
F₂ : Type u_11
F₃ : Type u_12
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)
E₃ : B → Type u_16
inst_13 : (x : B) → AddCommGroup (E₃ x)
inst_14 : (x : B) → Module.{u_8, u_16} 𝕜 (E₃ x)
inst_15 : NormedAddCommGroup F₃
inst_16 : NormedSpace 𝕜 F₃
inst_17 : TopologicalSpace (TotalSpace F₃ E₃)
inst_18 : (x : B) → TopologicalSpace (E₃ x)
inst_19 : TopologicalSpace B
inst_20 : FiberBundle F₁ E₁
inst_21 : VectorBundle 𝕜 F₁ E₁
inst_22 : FiberBundle F₂ E₂
inst_23 : VectorBundle 𝕜 F₂ E₂
inst_24 : FiberBundle F₃ E₃
inst_25 : VectorBundle 𝕜 F₃ E₃
inst_26 : ∀ (x : B), IsTopologicalAddGroup.{u_16} (E₃ x)
inst_27 : ∀ (x : B), ContinuousSMul.{u_8, u_16} 𝕜 (E₃ x)
x₀ x : B
ϕ : E₁ x →L[𝕜] ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)
v : F₁
w : F₂
h₁x : x ∈ Trivialization.baseSet (trivializationAt F₁ E₁ x₀)
h₂x : x ∈ Trivialization.baseSet (trivializationAt F₂ E₂ x₀)
h₃x : x ∈ Trivialization.baseSet (trivializationAt F₃ E₃ x₀)
⊢ x ∈
    Trivialization.baseSet (F := F₂ →L[𝕜] F₃) (Z :=
      TotalSpace (F₂ →L[𝕜] F₃) fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x))
      (trivializationAt (F₂ →L[𝕜] F₃)
        (fun (x : B) ↦ ContinuousLinearMap.{u_8, u_8, u_15, u_16} (RingHom.id 𝕜) (E₂ x) (E₃ x)) x₀)

Tactic:
simp [h₂x, h₃x]
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
F₁ : Type u_4
inst_8 : NormedAddCommGroup F₁
inst_9 : InnerProductSpace ℝ F₁
⊢ IsContinuousRiemannianBundle F₁ (Trivial B F₁)

Tactic:
⟨fun x ↦ innerSL ℝ, ?_, fun x v w ↦ rfl⟩

Premises used: Real, innerSL, IsContinuousRiemannianBundle.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
F₁ : Type u_4
inst_8 : NormedAddCommGroup F₁
inst_9 : InnerProductSpace ℝ F₁
refine :
  Continuous[inst,
      topologicalSpaceTotalSpace (RingHom.id ℝ) F₁ (Trivial B F₁) (F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] ℝ]
    fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
      ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x)
⊢ IsContinuousRiemannianBundle F₁ (Trivial B F₁)

Tactic:
refine ⟨fun x ↦ innerSL ℝ, ?_, fun x v w ↦ rfl⟩
-- Module: Mathlib.Topology.VectorBundle.Riemannian
Goal:
B : Type u_1
inst : TopologicalSpace B
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
E : B → Type u_3
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → NormedAddCommGroup (E x)
inst_5 : (x : B) → InnerProductSpace ℝ (E x)
inst_6 : FiberBundle F E
inst_7 : VectorBundle ℝ F E
F₁ : Type u_4
inst_8 : NormedAddCommGroup F₁
inst_9 : InnerProductSpace ℝ F₁
rw :
  ∀ (x : B),
    ContinuousAt (Y :=
      TotalSpace.{u_1, u_4, u_4} (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
      (fun (x : B) ↦
        TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
          ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x))
      x
⊢ Continuous[inst,
      topologicalSpaceTotalSpace (RingHom.id ℝ) F₁ (Trivial B F₁) (F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] ℝ]
    fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x
      ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x)

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt