-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
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
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → AddCommGroup (V x)
inst_10 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_11 : (x : M) → TopologicalSpace (V x)
inst_12 : FiberBundle F V
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle 1 F V I
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_15 : MemTrivializationAtlas (E := V) e
ι : Type u_7
b : Basis ι 𝕜 F
s : (x : M) → V x
x : M
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
hxe : x ∈ e.baseSet
hs : MDiffAt (T% s) x
i : ι
step step₁ step₂ :
  MDiffAt
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (Trivialization.localFrame_coeff I (V := V) e b i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        s)
    x
step₃ :
  let aux : (x : M) → 𝕜 := fun (x : M) ↦
    (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2 : ι →₀ 𝕜) :
        (a : ι) → 𝕜)
      i;
  MDiffAt aux x
step₄ :
  (MDiffAt fun (x : M) ↦
      (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2 : ι →₀ 𝕜) : (a : ι) → 𝕜) i)
    x
step₅ step₆ :
  ∀ (h₁ : (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2) x),
    (MDiffAt fun (x : M) ↦
        (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2 : ι →₀ 𝕜) : (a : ι) → 𝕜) i)
      x
step₇ :
  let aux : (x : M) → 𝕜 := fun (x : M) ↦
    (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2 : ι →₀ 𝕜) :
        (a : ι) → 𝕜)
      i;
  ∀ (h₁ : (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2) x),
    let breprl : F →ₗ[𝕜] 𝕜 :=
      { toFun := fun (v : F) ↦ (((b.repr : (a : F) → ι →₀ 𝕜) v : ι →₀ 𝕜) : (a : ι) → 𝕜) i, map_add' := ⋯,
        map_smul' := ⋯ };
    ∀
      (this :
        MDiffAt
            (⇑(((LinearMap.toContinuousLinearMap.{u_1, u_5, u_1} (𝕜 := 𝕜) (E := F) (F' := 𝕜) :
                        (F →ₗ[𝕜] 𝕜) ≃ₗ[𝕜] F →L[𝕜] 𝕜) :
                      (a : F →ₗ[𝕜] 𝕜) → F →L[𝕜] 𝕜)
                    breprl :
                  F →L[𝕜] 𝕜) :
              (a : F) → 𝕜)
          ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2),
      (MDiffAt fun (x : M) ↦
          (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2 : ι →₀ 𝕜) : (a : ι) → 𝕜) i)
        x
⊢ MDiffAt
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (Trivialization.localFrame_coeff I (V := V) e b i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        s)
    x

Tactic:
classical
  -- step 1: on `e.baseSet`, we know the coefficient very well
  let aux := fun x ↦ b.repr (e ((T% s) x)).2 i
  -- Since `e.baseSet` is open, this is sufficient.
  suffices MDiffAt aux x by
    apply this.congr_of_eventuallyEq
    apply eventuallyEq_of_mem (s := e.baseSet) (by simp [e.open_baseSet.mem_nhds hxe])
    intro y hy
    simp [aux, e.localFrame_coeff_eq_coeff hy]
  simp only [aux]
  -- step 2: `s` read in trivialization `e` is differentiable
  have h₁ : MDiffAt (fun x ↦ (e ((T% s) x)).2) x := by
    simpa using (e.mdifferentiableAt_section_iff I s hxe).1 hs
  -- step 3: `b.repr` is a linear map, so the composition is smooth
  let breprl : F →ₗ[𝕜] 𝕜 :=
    { toFun v := b.repr v i
      map_add' m m' := by simp
      map_smul' m x := by simp }
  have : MDifferentiableAt 𝓘(𝕜, F) 𝓘(𝕜) breprl.toContinuousLinearMap (e ((T% s) x)).2 :=
    mdifferentiableAt_iff_differentiableAt.mpr <| by fun_prop
  exact this.comp x h₁