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 : (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 : IsOpen[inst_4] u
hx : x ∈ u
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 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 : ℕ∞ω
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 : IsOpen[inst_4] u
hx : x ∈ u
this : Fintype ι
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x

Tactic:
hs.contMDiffAt_of_coeff h (hu.mem_nhds hx)

Premises used: IsLocalFrameOn.contMDiffAt_of_coeff, IsOpen.mem_nhds
-- 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 : IsOpen[inst_4] u
hx : x ∈ u
this : Fintype ι
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x

Tactic:
exact hs.contMDiffAt_of_coeff h (hu.mem_nhds hx)

Premises used: IsLocalFrameOn.contMDiffAt_of_coeff, IsOpen.mem_nhds
-- 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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((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)
inl :
  ∀ (hs : IsLocalFrameOn I F (V := V) 1 s ∅)
    (h :
      ∀ (i : ι),
        MDiff[∅]
          ((((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)),
    MDiff[∅] (T% t)
inr : ∀ (x : M) (hx : x ∈ u), MDiff[u] (T% t)
⊢ MDiff[u] (T% t)

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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
inst_14 : FiniteDimensional 𝕜 F
hs : IsLocalFrameOn I F (V := V) 1 s ∅
h :
  ∀ (i : ι),
    MDiff[∅]
      ((((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)
⊢ MDiff[∅] (T% t)

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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((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 : M
hx : x ∈ u
inr : ∀ (this : Fintype ι), MDiff[u] (T% t)
⊢ MDiff[u] (T% t)

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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((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 : M
hx : x ∈ u
this : Fintype ι
⊢ ∀ (i : ι),
    MDiff[u] 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⟩

Tactic:
have this (i) : MDiff[u] (T% ((LinearMap.piApply (hs.coeff i)) t • s i)) :=
    (h i).smul_section ((hs.contMDiffOn i).mdifferentiableOn one_ne_zero)
-- 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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((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 : M
hx : x ∈ u
this_1 : Fintype ι
this :
  ∀ (i : ι),
    MDiff[u] 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⟩
⊢ MDiff[u] fun (x : M) ↦
    ⟨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)⟩

Tactic:
have almost : MDiff[u] (T% (fun x ↦ ∑ i, hs.coeff i x (t x) • s i x)) :=
    .sum_section (fun i _ hx ↦ this i _ 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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((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 : M
hx : x ∈ u
this_1 : Fintype ι
this :
  ∀ (i : ι),
    MDiff[u] 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⟩
almost :
  MDiff[u] fun (x : M) ↦
    ⟨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)⟩
inr :
  ∀ y ∈ u,
    ⟨y, t y⟩ =
      ⟨y,
        ∑ i : ι,
          HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i y : (a : V y) → 𝕜) (t y) : 𝕜) (s i y)⟩
⊢ MDiff[u] (T% t)

Tactic:
apply almost.congr

Premises used: MDifferentiableOn.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
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiff[u]
      ((((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 : M
hx : x ∈ u
this_1 : Fintype ι
this :
  ∀ (i : ι),
    MDiff[u] 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⟩
almost :
  MDiff[u] fun (x : M) ↦
    ⟨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)⟩
y : M
hy : y ∈ u
⊢ ⟨y, t y⟩ =
    ⟨y,
      ∑ i : ι,
        HSMul.hSMul.{u_1, u_6, u_6} (α := 𝕜) ((hs.coeff (V := V) (u := u) i y : (a : V y) → 𝕜) (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
x : M
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiffAt
        ((((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 ι), MDiffAt (T% t) x
⊢ MDiffAt (T% t) 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
x : M
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiffAt
        ((((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 ι
⊢ (MDiffAt fun (x : M) ↦
      ⟨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)⟩)
    x

Tactic:
have almost : MDiffAt (T% (fun x ↦ ∑ i, hs.coeff i x (t x) • s i x)) x :=
    .sum_section (fun i ↦ (h i).smul_section <|
      ((hs.contMDiffOn i).mdifferentiableOn one_ne_zero).mdifferentiableAt 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
x : M
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiffAt
        ((((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 :
  (MDiffAt fun (x : M) ↦
      ⟨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)⟩)
    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} (α := 𝕜) ((hs.coeff (V := V) (u := u) i x : (a : V x) → 𝕜) (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
x : M
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiffAt
        ((((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 :
  (MDiffAt fun (x : M) ↦
      ⟨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)⟩)
    x
⊢ MDiffAt (T% t) x

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

Premises used: MDifferentiableAt.congr_of_eventuallyEq, IsLocalFrameOn.eventually_eq_sum_coeff_smul, Filter.Eventually.mono
-- 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
x : M
t : (x : M) → V x
inst_13 : VectorBundle 𝕜 F V
hs : IsLocalFrameOn I F (V := V) 1 s u
inst_14 : FiniteDimensional 𝕜 F
h :
  ∀ (i : ι),
    MDiffAt
        ((((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 : IsOpen[inst_4] u
hx : x ∈ u
⊢ MDiffAt (T% t) x

Tactic:
hs.mdifferentiableAt_of_coeff h (hu.mem_nhds hx)

Premises used: IsOpen.mem_nhds, IsLocalFrameOn.mdifferentiableAt_of_coeff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
M : Type u_4
inst_1 : TopologicalSpace M
F : Type u_5
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
V : M → Type u_6
inst_4 : TopologicalSpace (TotalSpace F V)
inst_5 : (x : M) → AddCommGroup (V x)
inst_6 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_7 : (x : M) → TopologicalSpace (V x)
inst_8 : FiberBundle F V
inst_9 : VectorBundle 𝕜 F V
ι : Type u_7
x : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_10 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
i : ι
hx : x ∈ e.baseSet
⊢ e.localFrame (V := V) b i x = (e.basisAt (V := V) b hx : (a : ι) → V x) i

Tactic:
simp [localFrame, hx]

Premises used: Bundle.Trivialization.localFrame
-- Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
M : Type u_4
inst_1 : TopologicalSpace M
F : Type u_5
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 F
V : M → Type u_6
inst_4 : TopologicalSpace (TotalSpace F V)
inst_5 : (x : M) → AddCommGroup (V x)
inst_6 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_7 : (x : M) → TopologicalSpace (V x)
inst_8 : FiberBundle F V
inst_9 : VectorBundle 𝕜 F V
ι : Type u_7
x : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V))
inst_10 : MemTrivializationAtlas (E := V) e
b : Basis ι 𝕜 F
i : ι
hx : x ∉ e.baseSet
⊢ e.localFrame (V := V) b i x = 0

Tactic:
simp [localFrame, hx]

Premises used: Bundle.Trivialization.localFrame