{B : Type u_4} →
  {E : B → Type u_6} →
    [inst : (b : B) → TopologicalSpace (E b)] →
      [inst_1 : (b : B) → AddCommGroup (E b)] →
        [inst_2 : (b : B) → Module ℝ (E b)] →
          {motive : Bundle.RiemannianMetric E → Sort u} →
            (t : Bundle.RiemannianMetric E) →
              ((inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) →
                  (symm : ∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v) →
                    (pos : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v) →
                      (continuousAt : ∀ (b : B), ContinuousAt (fun v => ((inner b) v) v) 0) →
                        (isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1}) →
                          motive
                            { inner := inner, symm := symm, pos := pos, continuousAt := continuousAt,
                              isVonNBounded := isVonNBounded }) →
                motive t