∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {H : Type uH} [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (↑⊤) M] [inst_7 : T2Space M] [inst_8 : Fintype ι] {s : Set M}
  (f : SmoothBumpCovering ι I M s) (x : M) (hx : x ∈ s),
  ((ContinuousLinearMap.fst ℝ E ℝ).comp (ContinuousLinearMap.proj (f.ind x hx))).comp
      (mfderiv I (modelWithCornersSelf ℝ (ι → E × ℝ)) (⇑f.embeddingPiTangent) x) =
    mfderiv I I (↑(chartAt H (f.c (f.ind x hx)))) x