-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
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 : ModelWithCorners 𝕜 E H
H' : Type u_5
inst_6 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
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'
F : Type u_8
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : IsManifold I 1 M
inst_14 : IsManifold I' 1 M'
this : IsManifold I (HAdd.hAdd (α := ℕ∞ω) 0 1) M
i j k : (↑(atlas H M) : Type (max u_4 u_6))
x : M
hxk : x ∈ (↑k : OpenPartialHomeomorph M H).source
hxi : x ∈ (↑i : OpenPartialHomeomorph M H).source
hxj : x ∈ (↑j : OpenPartialHomeomorph M H).source
v : E
hs :
  ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
        (↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M)) ∘
      (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
        (↑((↑i : OpenPartialHomeomorph M H).extend I).symm :
          E → M) =ᶠ[𝓝[range (↑I : H → E)] (↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x]
    (↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M)
hx :
  (((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M)) ∘
        (↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
          (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x) =
    ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
        (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
      ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)
hg :
  DifferentiableWithinAt 𝕜
    ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
      (↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M))
    (range (↑I : H → E)) ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x)
hf :
  DifferentiableWithinAt 𝕜
    ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
      (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
    (range (↑I : H → E)) ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x)
⊢ Eq (α := E)
    ((fderivWithin 𝕜
            ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
              (↑((↑j : OpenPartialHomeomorph M H).extend I).symm : E → M))
            (range (↑I : H → E)) ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) x) :
          (a : E) → E)
        ((fderivWithin 𝕜
                ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘
                  (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
                (range (↑I : H → E)) ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x) :
              (a : E) → E)
            v :
          E) :
      E)
    ((fderivWithin 𝕜
            ((↑((↑k : OpenPartialHomeomorph M H).extend I) : M → E) ∘
              (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
            (range (↑I : H → E)) ((↑((↑i : OpenPartialHomeomorph M H).extend I) : M → E) x) :
          (a : E) → E)
        v :
      E)
have h : MapsTo
  ((↑((↑j : OpenPartialHomeomorph M H).extend I) : M → E) ∘ (↑((↑i : OpenPartialHomeomorph M H).extend I).symm : E → M))
  (range (↑I : H → E)) (range (↑I : H → E))
Tactic: rw [fderivWithin_fderivWithin, Filter.EventuallyEq.fderivWithin_eq]