-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.LocalFrame (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
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
k : ℕ∞ω
x : M
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
inst_18 : ContMDiffVectorBundle k F V I
hxe : x ∈ e.baseSet
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x : M) ↦ ⟨x, s x⟩) x
i : ι
step step₁ step₂ :
  ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) k
    ((((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;
  ContMDiffAt I 𝓘(𝕜, 𝕜) k aux x
step₄ :
  ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) k
    (fun (x : M) ↦ (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2 : ι →₀ 𝕜) : (a : ι) → 𝕜) i)
    x
step₅ step₆ :
  ∀
    (h₁ :
      ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2)
        x),
    ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) k
      (fun (x : M) ↦
        (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2 : ι →₀ 𝕜) : (a : ι) → 𝕜) i)
      x
⊢ ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) k
    ((((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
have 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₁ :
    ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (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' := sorry,
      map_smul' := sorry };
  ∀
    (this :
      ContMDiffAt 𝓘(𝕜, F) 𝓘(𝕜, 𝕜) (M' := 𝕜) k
        (⇑(((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),
    ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) k
      (fun (x : M) ↦
        (((b.repr : (a : F) → ι →₀ 𝕜) ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2 : ι →₀ 𝕜) : (a : ι) → 𝕜) i)
      x
Tactic: classical
  -- step 1: on e.baseSet, we know compute 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 CMDiffAt k 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 `C^k`
  have h₁ : CMDiffAt k (fun x ↦ (e ((T% s) x)).2) x := by
    simpa using (e.contMDiffAt_section_iff 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 : ContMDiffAt 𝓘(𝕜, F) 𝓘(𝕜) k breprl.toContinuousLinearMap (e ((T% s) x)).2 :=
    contMDiffAt_iff_contDiffAt.mpr <| by fun_prop
  exact this.comp x h₁