awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t t' : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
this : Fintype ι := hs.fintypeOfFiniteDimensional (V := V) (u := u) hx
⊢ t x = t' x ↔
    ∀ (i : ι),
      Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
        ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)

Tactic:
⟨fun h i ↦ hs.coeff_congr h i, fun h ↦ hs.eq_of_coeff_eq hx h⟩

Premises used: IsLocalFrameOn.coeff_congr, IsLocalFrameOn.eq_of_coeff_eq, Iff.intro
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t t' : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F (V := V) n s u
hx : x ∈ u
this : Fintype ι := hs.fintypeOfFiniteDimensional (V := V) (u := u) hx
⊢ t x = t' x ↔
    ∀ (i : ι),
      Eq.{u_1 + 1} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜)
        ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t' x) : 𝕜)

Tactic:
exact ⟨fun h i ↦ hs.coeff_congr h i, fun h ↦ hs.eq_of_coeff_eq hx h⟩
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
inl :
  ∀ (hs : IsLocalFrameOn I F (V := V) n s ∅)
    (h :
      ∀ (i : ι),
        ContMDiffOn.{u_1, u_2, u_3, u_4, u_1, u_1, u_1} I (M := M) 𝓘(𝕜, 𝕜) (M' := 𝕜) n
          ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                  (hs.coeff (V := V) (u := ∅) i) :
                ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
              (a : (x : M) → V x) → M → 𝕜)
            t)
          ∅),
    ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) ∅
inr : ∀ (x : M) (hx : x ∈ u), ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u

Tactic:
rcases u.eq_empty_or_nonempty with rfl | ⟨x, hx⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- 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
ι : Type u_7
s : ι → (x : M) → V x
n : ℕ∞ω
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F (V := V) n s ∅
h :
  ∀ (i : ι),
    ContMDiffOn.{u_1, u_2, u_3, u_4, u_1, u_1, u_1} I (M := M) 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := ∅) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      ∅
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) ∅

Tactic:
simp
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
x : M
hx : x ∈ u
inr : ∀ (this : Fintype ι), ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u

Tactic:
have := fintypeOfFiniteDimensional hs hx
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
x : M
hx : x ∈ u
this : Fintype ι
⊢ ∀ (i : ι),
    ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
      (fun (x : M) ↦
        ⟨x,
          HSMul.hSMul (α := M → 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t :
              M → 𝕜)
            (s i) x⟩)
      u

Tactic:
have this (i) : CMDiff[u] n (T% ((LinearMap.piApply (hs.coeff i)) t • s i)) :=
    (h i).smul_section (hs.contMDiffOn i)
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
x : M
hx : x ∈ u
this_1 : Fintype ι
this :
  ∀ (i : ι),
    ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
      (fun (x : M) ↦
        ⟨x,
          HSMul.hSMul (α := M → 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t :
              M → 𝕜)
            (s i) x⟩)
      u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
    (fun (x : M) ↦
      ⟨x,
        ∑ i : ι,
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t x :
              𝕜)
            (s i x)⟩)
    u

Tactic:
have almost : CMDiff[u] n (T% (fun x ↦ ∑ i, ((LinearMap.piApply (hs.coeff i)) t) x • s i x)) :=
    .sum_section fun i _ ↦ this i
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
x : M
hx : x ∈ u
this_1 : Fintype ι
this :
  ∀ (i : ι),
    ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
      (fun (x : M) ↦
        ⟨x,
          HSMul.hSMul (α := M → 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t :
              M → 𝕜)
            (s i) x⟩)
      u
almost :
  ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
    (fun (x : M) ↦
      ⟨x,
        ∑ i : ι,
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t x :
              𝕜)
            (s i x)⟩)
    u
inr :
  ∀ y ∈ u,
    ⟨y, t y⟩ =
      ⟨y,
        ∑ i : ι,
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t y :
              𝕜)
            (s i y)⟩
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u

Tactic:
apply almost.congr

Premises used: ContMDiffOn.congr
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffOn I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      u
x : M
hx : x ∈ u
this_1 : Fintype ι
this :
  ∀ (i : ι),
    ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
      (fun (x : M) ↦
        ⟨x,
          HSMul.hSMul (α := M → 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t :
              M → 𝕜)
            (s i) x⟩)
      u
almost :
  ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
    (fun (x : M) ↦
      ⟨x,
        ∑ i : ι,
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t x :
              𝕜)
            (s i x)⟩)
    u
y : M
hy : y ∈ u
⊢ ⟨y, t y⟩ =
    ⟨y,
      ∑ i : ι,
        HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
          ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                    (hs.coeff (V := V) (u := u) i) :
                  ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                (a : (x : M) → V x) → M → 𝕜)
              t y :
            𝕜)
          (s i y)⟩

Tactic:
simpa using congrArg (TotalSpace.mk' F y) (hs.coeff_sum_eq t hy)

Premises used: congrArg, Bundle.TotalSpace.mk', IsLocalFrameOn.coeff_sum_eq
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      x
hu : u ∈ 𝓝 x
have : ∀ (this : Fintype ι), ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x

Tactic:
have := fintypeOfFiniteDimensional hs (mem_of_mem_nhds hu)
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      x
hu : u ∈ 𝓝 x
this : Fintype ι
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
    (fun (x : M) ↦
      ⟨x,
        ∑ i : ι,
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t x :
              𝕜)
            (s i x)⟩)
    x

Tactic:
have almost : CMDiffAt n (T% (fun x ↦ ∑ i, ((LinearMap.piApply (hs.coeff i)) t) x • s i x)) x :=
    .sum_section (fun i _ ↦ (h i).smul_section <| (hs.contMDiffOn i).contMDiffAt hu)
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      x
hu : u ∈ 𝓝 x
this : Fintype ι
almost :
  ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
    (fun (x : M) ↦
      ⟨x,
        ∑ i : ι,
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t x :
              𝕜)
            (s i x)⟩)
    x
⊢ ∀ (x : M),
    t x =
        ∑ i : ι,
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (t x) : 𝕜) (s i x) →
      Eq (α := TotalSpace F V) ((fun (x : M) ↦ ⟨x, t x⟩) x)
        ((fun (x : M) ↦
            (⟨x,
                ∑ i : ι,
                  HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
                    ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                              (hs.coeff (V := V) (u := u) i) :
                            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                          (a : (x : M) → V x) → M → 𝕜)
                        t x :
                      𝕜)
                    (s i x)⟩ :
              TotalSpace F V))
          x)

Tactic:
simp
-- 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
ι : Type u_7
s : ι → (x : M) → V x
u : Set M
n : ℕ∞ω
x : M
t : (x : M) → V x
hs : IsLocalFrameOn I F (V := V) n s u
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    ContMDiffAt I 𝓘(𝕜, 𝕜) (M' := 𝕜) n
      ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
              (hs.coeff (V := V) (u := u) i) :
            ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
          (a : (x : M) → V x) → M → 𝕜)
        t)
      x
hu : u ∈ 𝓝 x
this : Fintype ι
almost :
  ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n
    (fun (x : M) ↦
      ⟨x,
        ∑ i : ι,
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜)
            ((((LinearMap.piApply (V := V) : (a : (x : M) → V x →ₗ[𝕜] 𝕜) → ((x : M) → V x) →ₗ[𝕜] M → 𝕜)
                      (hs.coeff (V := V) (u := u) i) :
                    ((x : M) → V x) →ₗ[𝕜] M → 𝕜) :
                  (a : (x : M) → V x) → M → 𝕜)
                t x :
              𝕜)
            (s i x)⟩)
    x
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x

Tactic:
exact almost.congr_of_eventuallyEq <| (hs.eventually_eq_sum_coeff_smul t hu).mono (by simp)

Premises used: IsLocalFrameOn.eventually_eq_sum_coeff_smul, Filter.Eventually.mono, ContMDiffAt.congr_of_eventuallyEq