awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
x : B
rw :
  ContinuousAt (Y := B)
      (fun (x : B) ↦
        TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
          (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 ∧
    ContinuousAt.{u_1, u_4} (Y := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
      (fun (x_1 : B) ↦
        ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                  (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                    Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                    (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)))) :
              (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
                B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
            (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
              ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2)
      x
⊢ 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

Tactic:
rw [FiberBundle.continuousAt_totalSpace]

Premises used: FiberBundle.continuousAt_totalSpace
-- 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₁
x : B
⊢ ContinuousAt (Y := B)
      (fun (x : B) ↦
        TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
          (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 ∧
    ContinuousAt.{u_1, u_4} (Y := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
      (fun (x_1 : B) ↦
        ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                  (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                    Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                    (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)))) :
              (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
                B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
            (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
              ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2)
      x

Tactic:
⟨continuousAt_id, ?_⟩

Premises used: And.intro, continuousAt_id
-- 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₁
x : B
refine :
  ContinuousAt.{u_1, u_4} (Y := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
    (fun (x_1 : B) ↦
      ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                  Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                  (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)))) :
            (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
              B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
          (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
            ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2)
    x
⊢ ContinuousAt (Y := B)
      (fun (x : B) ↦
        TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
          (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 ∧
    ContinuousAt.{u_1, u_4} (Y := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
      (fun (x_1 : B) ↦
        ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                  (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                    Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                    (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)))) :
              (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
                B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
            (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
              ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2)
      x

Tactic:
refine ⟨continuousAt_id, ?_⟩
-- 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₁
x : B
⊢ ContinuousAt.{u_1, u_4} (Y := F₁ →L⋆[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ innerSL ℝ) x

Tactic:
continuousAt_const (y := innerSL ℝ)

Premises used: continuousAt_const
-- 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₁
x : B
h :
  ∀ (x_1 : B),
    Eq.{u_4 + 1} (α := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
      ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                  Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                  (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)))) :
            (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
              B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
          (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
            ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2
      (innerSL ℝ)
⊢ ContinuousAt.{u_1, u_4} (Y := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
    (fun (x_1 : B) ↦
      ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                  Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                  (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)))) :
            (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
              B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
          (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
            ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2)
    x

Tactic:
convert! continuousAt_const (y := innerSL ℝ)

Premises used: continuousAt_const
-- 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₁
x x_1 : B
h :
  ∀ (v w : F₁),
    Eq (α := ℝ)
      ((((((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                            (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                              Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                              (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)))) :
                        (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
                          B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
                      (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                        (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
                        ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2 :
                  (a : F₁) → F₁ →L[ℝ] ℝ)
                v :
              F₁ →L[ℝ] ℝ) :
            (a : F₁) → ℝ)
          w :
        ℝ)
      ((((innerSL ℝ : (a : F₁) → F₁ →L[ℝ] ℝ) v : F₁ →L[ℝ] ℝ) : (a : F₁) → ℝ) w : ℝ)
⊢ Eq.{u_4 + 1} (α := F₁ →L[ℝ] F₁ →L[ℝ] ℝ)
    ((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
              (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                (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)))) :
          (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
            B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
        (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
          ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2
    (innerSL ℝ)

Tactic:
ext v w
-- 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₁
x x_1 : B
v w : F₁
⊢ Eq (α := ℝ)
    ((((((↑(trivializationAt (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                          (TotalSpace.proj (F := F₁ →L[ℝ] F₁ →L[ℝ] ℝ) (E := fun (x : B) ↦
                            Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                            (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)))) :
                      (TotalSpace (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ) →
                        B × (F₁ →L[ℝ] F₁ →L[ℝ] ℝ))
                    (TotalSpace.mk' (E := fun (x : B) ↦ Trivial B F₁ x →L[ℝ] Trivial B F₁ x →L[ℝ] ℝ)
                      (F₁ →L[ℝ] F₁ →L[ℝ] ℝ) x_1
                      ((fun (x : B) ↦ (innerSL ℝ : Trivial B F₁ x →L⋆[ℝ] Trivial B F₁ x →L[ℝ] ℝ)) x_1))).2 :
                (a : F₁) → F₁ →L[ℝ] ℝ)
              v :
            F₁ →L[ℝ] ℝ) :
          (a : F₁) → ℝ)
        w :
      ℝ)
    ((((innerSL ℝ : (a : F₁) → F₁ →L[ℝ] ℝ) v : F₁ →L[ℝ] ℝ) : (a : F₁) → ℝ) w : ℝ)

Tactic:
simp [hom_trivializationAt_apply, inCoordinates]

Premises used: ContinuousLinearMap.inCoordinates, hom_trivializationAt_apply
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
rcases :
  ∀ (g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ)
    (g_cont :
      Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ]
        fun (x : B) ↦ TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x))
    (hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w),
    ContinuousWithinAt (Y := ℝ) (fun (m : M) ↦ ⟪v m, w m⟫) s x
⊢ ContinuousWithinAt (Y := ℝ) (fun (m : M) ↦ ⟪v m, w m⟫) s x

Tactic:
rcases h.exists_continuous with ⟨g, g_cont, hg⟩

Premises used: IsContinuousRiemannianBundle.exists_continuous
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
⊢ ContinuousWithinAt.{u_4, u_1} (Y := B) (fun (x : M) ↦ b x) s x ∧
    ContinuousWithinAt.{u_4, u_2} (Y := F)
      (fun (x_1 : M) ↦
        ((↑(trivializationAt F E (b x)) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) (b x_1) (v x_1))).2)
      s x

Tactic:
simp only [FiberBundle.continuousWithinAt_totalSpace] at hv

Premises used: FiberBundle.continuousWithinAt_totalSpace
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
hv :
  ContinuousWithinAt.{u_4, u_1} (Y := B) (fun (x : M) ↦ b x) s x ∧
    ContinuousWithinAt.{u_4, u_2} (Y := F)
      (fun (x_1 : M) ↦
        ((↑(trivializationAt F E (b x)) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) (b x_1) (v x_1))).2)
      s x
⊢ ContinuousWithinAt b s x

Tactic:
hv.1

Premises used: And.left
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
hv :
  ContinuousWithinAt.{u_4, u_1} (Y := B) (fun (x : M) ↦ b x) s x ∧
    ContinuousWithinAt.{u_4, u_2} (Y := F)
      (fun (x_1 : M) ↦
        ((↑(trivializationAt F E (b x)) : TotalSpace F E → B × F) (TotalSpace.mk (E := E) (b x_1) (v x_1))).2)
      s x
⊢ ContinuousWithinAt b s x

Tactic:
exact hv.1

Premises used: And.left
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
⊢ ContinuousWithinAt b s x

Tactic:
have hf : ContinuousWithinAt b s x := by
    simp only [FiberBundle.continuousWithinAt_totalSpace] at hv
    exact hv.1
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
hf : ContinuousWithinAt b s x
simp :
  ContinuousWithinAt (Y := ℝ)
    (fun (m : M) ↦ (((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)) s
    x
⊢ ContinuousWithinAt (Y := ℝ) (fun (m : M) ↦ ⟪v m, w m⟫) s x

Tactic:
simp only [hg]
-- 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
M : Type u_4
inst_8 : TopologicalSpace M
h : IsContinuousRiemannianBundle F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (v m)) s x
hw : ContinuousWithinAt (Y := TotalSpace F E) (fun (m : M) ↦ TotalSpace.mk (E := E) (b m) (w m)) s x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun (x : B) ↦ E x →L[ℝ] ℝ] fun (x : B) ↦
    TotalSpace.mk' (E := fun (x : B) ↦ E x →L[ℝ] E x →L[ℝ] ℝ) (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = (((g x : (a : E x) → E x →L[ℝ] ℝ) v : E x →L[ℝ] ℝ) : (a : E x) → ℝ) w
hf : ContinuousWithinAt b s x
⊢ ContinuousWithinAt.{u_4, u_1} (Y := TotalSpace ℝ (Trivial B ℝ))
    (fun (m : M) ↦
      TotalSpace.mk' (E := Trivial B ℝ) ℝ (b m)
        ((((g (b m) : (a : E (b m)) → E (b m) →L[ℝ] ℝ) (v m) : E (b m) →L[ℝ] ℝ) : (a : E (b m)) → ℝ) (w m)))
    s x

Tactic:
have : ContinuousWithinAt
      (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) (g (b m) (v m) (w m))) s x :=
    (g_cont.continuousAt.comp_continuousWithinAt hf).clm_bundle_apply₂ (F₁ := F) (F₂ := F) hv hw