∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (x : B) → NormedAddCommGroup (E x)] [inst_9 : (x : B) → InnerProductSpace ℝ (E x)]
  [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E],
  (∃ g,
      (ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b =>
          Bundle.TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) b (g b)) ∧
        ∀ (x : B) (v w : E x), inner ℝ v w = ((g x) v) w) →
    IsContMDiffRiemannianBundle IB n F E