-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
EM : Type u_10
inst_8 : NormedAddCommGroup EM
inst_9 : NormedSpace 𝕜 EM
HM : Type u_11
inst_10 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_11 : TopologicalSpace M
inst_12 : ChartedSpace HM M
inst_13 : TopologicalSpace B
inst_14 : ChartedSpace HB B
inst_15 : FiberBundle F E
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : ContinuousWithinAt f s x₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
refine_1 :
  ∀ (x : M)
    (hx :
      Membership.mem (γ := Set M)
        ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))))
        x),
    Eq.{u_7 + 1} (α := EB) ((fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) x)
      (Function.comp (β := EB × F) Prod.fst
        (fun (x : M) ↦
          ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
              ((↑(OpenPartialHomeomorph.toPartialEquiv
                        (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                    TotalSpace F E → B × F)
                  (f x)).1,
            ((↑(OpenPartialHomeomorph.toPartialEquiv
                      (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).2))
        x)
refine_2 :
  (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x₀).proj (E := E)) =
    Function.comp (β := EB × F) Prod.fst
      (fun (x : M) ↦
        ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
            ((↑(OpenPartialHomeomorph.toPartialEquiv
                      (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).1,
          ((↑(OpenPartialHomeomorph.toPartialEquiv
                    (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                TotalSpace F E → B × F)
              (f x)).2))
      x₀
⊢ MDiffAt[s]
        (Function.comp (β := EB × F) Prod.fst fun (x : M) ↦
          ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
              ((↑(OpenPartialHomeomorph.toPartialEquiv
                        (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                    TotalSpace F E → B × F)
                  (f x)).1,
            ((↑(OpenPartialHomeomorph.toPartialEquiv
                      (Trivialization.toOpenPartialHomeomorph (trivializationAt F E ((f x₀).proj (E := E))))) :
                  TotalSpace F E → B × F)
                (f x)).2))
      x₀ ↔
    (MDiffAt[s] fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) x₀

Tactic:
refine EventuallyEq.mdifferentiableWithinAt_iff (eventually_of_mem h1 fun x hx => ?_) ?_

Premises used: Filter.eventually_of_mem, Filter.EventuallyEq.mdifferentiableWithinAt_iff