∀ {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 : (b : B) → TopologicalSpace (E b)] [inst_9 : (b : B) → AddCommGroup (E b)]
  [inst_10 : (b : B) → Module ℝ (E b)] [inst_11 : FiberBundle F E] [inst_12 : VectorBundle ℝ F 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)
  (isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1})
  (contMDiff :
    ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b =>
      Bundle.TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) b (inner b))
  (inner_1 : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) (symm_1 : ∀ (b : B) (v w : E b), ((inner_1 b) v) w = ((inner_1 b) w) v)
  (pos_1 : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner_1 b) v) v)
  (isVonNBounded_1 : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner_1 b) v) v < 1})
  (contMDiff_1 :
    ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b =>
      Bundle.TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) b (inner_1 b)),
  ({ inner := inner, symm := symm, pos := pos, isVonNBounded := isVonNBounded, contMDiff := contMDiff } =
      { inner := inner_1, symm := symm_1, pos := pos_1, isVonNBounded := isVonNBounded_1, contMDiff := contMDiff_1 }) =
    (inner = inner_1)