-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f f₁ : M → M'
s : Set M
h : ∀ x ∈ s, f x = f₁ x
p : TangentBundle I M
hp : p.proj (E := TangentSpace I) ∈ s
rw :
  HEq (α :=
    TangentSpace I'
      (TotalSpace.proj (F := E') (E := TangentSpace I')
        (TotalSpace.mk (E := TangentSpace I') (f (p.proj (E := TangentSpace I)))
          (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
                ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                  (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
              (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
            (p.snd (E := TangentSpace I))))))
    (TotalSpace.snd (E := TangentSpace I')
      (TotalSpace.mk (E := TangentSpace I') (f (p.proj (E := TangentSpace I)))
        (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f p.proj))
          (p.snd (E := TangentSpace I)))))
    (β := TangentSpace I' (TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f₁ s p)))
    (TotalSpace.snd (E := TangentSpace I') (tangentMapWithin I I' f₁ s p))
rw₁ :
  HEq (α :=
    TangentSpace I'
      (TotalSpace.proj (F := E') (E := TangentSpace I')
        (TotalSpace.mk (E := TangentSpace I') (f₁ (p.proj (E := TangentSpace I)))
          (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
                ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                  (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
              (a : TangentSpace I p.proj) → TangentSpace I' (f₁ p.proj))
            (p.snd (E := TangentSpace I))))))
    (TotalSpace.snd (E := TangentSpace I')
      (TotalSpace.mk (E := TangentSpace I') (f₁ (p.proj (E := TangentSpace I)))
        (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f₁ p.proj))
          (p.snd (E := TangentSpace I)))))
    (β := TangentSpace I' (TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f₁ s p)))
    (TotalSpace.snd (E := TangentSpace I') (tangentMapWithin I I' f₁ s p))
rw₂ :
  HEq.{u_5 + 1} (α :=
    TangentSpace I'
      (TotalSpace.proj (F := E') (E := TangentSpace I')
        (TotalSpace.mk (E := TangentSpace I') (f₁ (p.proj (E := TangentSpace I)))
          (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
                ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                  (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
              (a : TangentSpace I p.proj) → TangentSpace I' (f₁ p.proj))
            (p.snd (E := TangentSpace I))))))
    (TotalSpace.snd (E := TangentSpace I')
      (TotalSpace.mk (E := TangentSpace I') (f₁ (p.proj (E := TangentSpace I)))
        (((mfderivWithin I I' f s (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f₁ p.proj))
          (p.snd (E := TangentSpace I)))))
    (β :=
    TangentSpace I'
      (TotalSpace.proj (F := E') (E := TangentSpace I')
        (TotalSpace.mk (E := TangentSpace I') (f₁ (p.proj (E := TangentSpace I)))
          (((mfderivWithin I I' f₁ s (p.proj (E := TangentSpace I)) :
                ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                  (TangentSpace I' (f₁ (p.proj (E := TangentSpace I))))) :
              (a : TangentSpace I p.proj) → TangentSpace I' (f₁ p.proj))
            (p.snd (E := TangentSpace I))))))
    (TotalSpace.snd (E := TangentSpace I')
      (TotalSpace.mk (E := TangentSpace I') (f₁ (p.proj (E := TangentSpace I)))
        (((mfderivWithin I I' f₁ s (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f₁ (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f₁ p.proj))
          (p.snd (E := TangentSpace I)))))
rw₃ rw₄ :
  HEq.{u_5 + 1} (α :=
    TangentSpace I'
      (TotalSpace.proj (F := E') (E := TangentSpace I')
        (TotalSpace.mk (E := TangentSpace I') (f₁ (p.proj (E := TangentSpace I)))
          (((mfderivWithin I I' f₁ s (p.proj (E := TangentSpace I)) :
                ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                  (TangentSpace I' (f₁ (p.proj (E := TangentSpace I))))) :
              (a : TangentSpace I p.proj) → TangentSpace I' (f₁ p.proj))
            (p.snd (E := TangentSpace I))))))
    (TotalSpace.snd (E := TangentSpace I')
      (TotalSpace.mk (E := TangentSpace I') (f₁ (p.proj (E := TangentSpace I)))
        (((mfderivWithin I I' f₁ s (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f₁ (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f₁ p.proj))
          (p.snd (E := TangentSpace I)))))
    (β :=
    TangentSpace I'
      (TotalSpace.proj (F := E') (E := TangentSpace I')
        (TotalSpace.mk (E := TangentSpace I') (f₁ (p.proj (E := TangentSpace I)))
          (((mfderivWithin I I' f₁ s (p.proj (E := TangentSpace I)) :
                ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                  (TangentSpace I' (f₁ (p.proj (E := TangentSpace I))))) :
              (a : TangentSpace I p.proj) → TangentSpace I' (f₁ p.proj))
            (p.snd (E := TangentSpace I))))))
    (TotalSpace.snd (E := TangentSpace I')
      (TotalSpace.mk (E := TangentSpace I') (f₁ (p.proj (E := TangentSpace I)))
        (((mfderivWithin I I' f₁ s (p.proj (E := TangentSpace I)) :
              ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I (p.proj (E := TangentSpace I)))
                (TangentSpace I' (f₁ (p.proj (E := TangentSpace I))))) :
            (a : TangentSpace I p.proj) → TangentSpace I' (f₁ p.proj))
          (p.snd (E := TangentSpace I)))))
⊢ HEq (α := TangentSpace I' (TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f s p)))
    (TotalSpace.snd (E := TangentSpace I') (tangentMapWithin I I' f s p)) (β :=
    TangentSpace I' (TotalSpace.proj (E := TangentSpace I') (tangentMapWithin I I' f₁ s p)))
    (TotalSpace.snd (E := TangentSpace I') (tangentMapWithin I I' f₁ s p))

Tactic:
rw [tangentMapWithin, h p.1 hp, tangentMapWithin, mfderivWithin_congr h (h _ hp)]

Premises used: Bundle.TotalSpace.proj, mfderivWithin_congr, tangentMapWithin