-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Basic (goal)
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 : M → M'
x : M
s t : Set M
ht : t ∈ 𝓝 x
rw :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (if MDifferentiableWithinAt I I' f (s ∩ t) x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
    else 0)
    (mfderivWithin I I' f s x)
rw₁ :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (if MDifferentiableWithinAt I I' f (s ∩ t) x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ t) ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
    else 0)
    (if MDifferentiableWithinAt I I' f s x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
    else 0)
rw₂ :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (if MDifferentiableWithinAt I I' f (s ∩ t) x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f)
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' t)
        ((↑(extChartAt I x) : M → E) x)
    else 0)
    (if MDifferentiableWithinAt I I' f s x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
    else 0)
rw₃ :
  Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (if MDifferentiableWithinAt I I' f s x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f)
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' t)
        ((↑(extChartAt I x) : M → E) x)
    else 0)
    (if MDifferentiableWithinAt I I' f s x then
      fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
        ((↑(extChartAt I x) : M → E) x)
    else 0)
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
    (mfderivWithin I I' f (s ∩ t) x) (mfderivWithin I I' f s x)
have rw₄ : Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id 𝕜) (TangentSpace I x) (TangentSpace I' (f x)))
  (if MDifferentiableWithinAt I I' f s x then
    fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
  else 0)
  (if MDifferentiableWithinAt I I' f s x then
    fderivWithin 𝕜 (writtenInExtChartAt I I' x f) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
  else 0)
Tactic: rw [mfderivWithin, mfderivWithin, extChartAt_preimage_inter_eq, mdifferentiableWithinAt_inter ht,
    fderivWithin_inter (extChartAt_preimage_mem_nhds ht)]