∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] (I I_1 : ModelWithCorners 𝕜 E H) (e_I : I = I_1) {H' : Type u_5}
  [inst_6 : TopologicalSpace H'] (I' I'_1 : ModelWithCorners 𝕜 E' H') (e_I' : I' = I'_1) {M : Type u_6}
  [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {M' : Type u_7} [inst_9 : TopologicalSpace M']
  [inst_10 : ChartedSpace H' M'] [inst_11 : IsManifold I 1 M] [inst_12 : IsManifold I' 1 M'] {N : Type u_9}
  (f f_1 : N → M),
  f = f_1 →
    ∀ (g g_1 : N → M'),
      g = g_1 →
        ∀ (ϕ ϕ_1 : N → E →L[𝕜] E'),
          ϕ = ϕ_1 →
            ∀ (a a_1 : N),
              a = a_1 →
                ∀ (a_2 a_3 : N),
                  a_2 = a_3 → inTangentCoordinates I I' f g ϕ a a_2 = inTangentCoordinates I_1 I'_1 f_1 g_1 ϕ_1 a_1 a_3