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
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 : ι
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 fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ((fun (x : M) ↦ ⟨x, s x⟩) x)).2) x

Tactic:
have h₁ : MDiffAt (fun x ↦ (e ((T% s) x)).2) x := by
    simpa using (e.mdifferentiableAt_section_iff I s hxe).1 hs
-- 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 : ι
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
m m' : F
⊢ (((b.repr : (a : F) → ι →₀ 𝕜) (m + m') : ι →₀ 𝕜) : (a : ι) → 𝕜) i =
    HAdd.hAdd (α := 𝕜) (β := 𝕜) ((((b.repr : (a : F) → ι →₀ 𝕜) m : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)
      ((((b.repr : (a : F) → ι →₀ 𝕜) m' : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)

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
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_1 : M
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
hxe : x_1 ∈ e.baseSet
hs : MDiffAt (T% s) x_1
i : ι
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_1
m : 𝕜
x : F
⊢ (((b.repr : (a : F) → ι →₀ 𝕜) (m • x) : ι →₀ 𝕜) : (a : ι) → 𝕜) i =
    HSMul.hSMul (α := 𝕜) (β := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) m : 𝕜)
      ((((b.repr : (a : F) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜) i : 𝕜)

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
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 : ι
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
breprl : F →ₗ[𝕜] 𝕜 :=
  { toFun := fun (v : F) ↦ (((b.repr : (a : F) → ι →₀ 𝕜) v : ι →₀ 𝕜) : (a : ι) → 𝕜) i, map_add' := ⋯, map_smul' := ⋯ }
⊢ DifferentiableAt 𝕜 (F := 𝕜)
    (⇑(((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

Tactic:
fun_prop
-- 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 : ι
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
breprl : F →ₗ[𝕜] 𝕜 :=
  { toFun := fun (v : F) ↦ (((b.repr : (a : F) → ι →₀ 𝕜) v : ι →₀ 𝕜) : (a : ι) → 𝕜) i, map_add' := ⋯, map_smul' := ⋯ }
⊢ 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

Tactic:
have : MDifferentiableAt 𝓘(𝕜, F) 𝓘(𝕜) breprl.toContinuousLinearMap (e ((T% s) x)).2 :=
    mdifferentiableAt_iff_differentiableAt.mpr <| by fun_prop
-- 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 : ι
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
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

Tactic:
this.comp x h₁

Premises used: MDifferentiableAt.comp
-- 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 : ι
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
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

Tactic:
exact this.comp x h₁

Premises used: MDifferentiableAt.comp
-- 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
t : Set M
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
ht : IsOpen[inst_4] t
ht' : t ⊆ e.baseSet
hs : MDiff[t] (T% s)
i : ι
⊢ MDiff[t]
    ((((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)

Tactic:
fun _ hx ↦ (mdifferentiableAt_localFrame_coeff b (ht' hx)
    (hs.mdifferentiableAt (ht.mem_nhds hx)) i).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, MDifferentiableOn.mdifferentiableAt, MDifferentiableOn, IsOpen.mem_nhds, mdifferentiableAt_localFrame_coeff
-- 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
inst_16 : FiniteDimensional 𝕜 F
inst_17 : CompleteSpace 𝕜
hs : MDiff[e.baseSet] (T% s)
i : ι
⊢ MDiff[e.baseSet]
    ((((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)

Tactic:
mdifferentiableOn_localFrame_coeff b e.open_baseSet (subset_refl _) hs _

Premises used: mdifferentiableOn_localFrame_coeff, Bundle.Trivialization.open_baseSet, subset_refl
-- 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 𝕜
hx : x' ∈ e.baseSet
⊢ MDiffAt (T% s) x' ↔
    ∀ (i : ι),
      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:
⟨fun h i ↦ mdifferentiableAt_localFrame_coeff b hx h i, fun hi ↦
    (e.isLocalFrameOn_localFrame_baseSet I 1 b).mdifferentiableAt_of_coeff_aux hi e.open_baseSet hx⟩

Premises used: IsLocalFrameOn.mdifferentiableAt_of_coeff_aux, Bundle.Trivialization.open_baseSet, Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet, Iff.intro, OfNat.ofNat, mdifferentiableAt_localFrame_coeff
-- 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
simp :
  ContinuousWithinAt f s x₀ ∧ MDiffAt[s] ((↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) : TotalSpace F E → EB × F) ∘ f) x₀ ↔
    (ContinuousWithinAt.{u_5, u_2} (Y := B) (fun (x : M) ↦ (f x).proj (E := E)) s x₀ ∧
        MDiffAt[s] ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ∘ fun (x : M) ↦ (f x).proj (E := E)) x₀) ∧
      ContinuousWithinAt.{u_5, u_4} (Y := F)
          (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) s x₀ ∧
        MDiffAt[s]
            ((↑(extChartAt 𝓘(𝕜, F)
                    ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x₀)).2) :
                F → F) ∘
              fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2)
          x₀
⊢ MDiffAt[s] f x₀ ↔
    (MDiffAt[s] fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧
      (MDiffAt[s] fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
simp +singlePass only [mdifferentiableWithinAt_iff_target]

Premises used: mdifferentiableWithinAt_iff_target
-- 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
rw :
  ContinuousWithinAt f s x₀ →
    (MDiffAt[s] ((↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) : TotalSpace F E → EB × F) ∘ f) x₀ ↔
      MDiffAt[s] ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ∘ fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧
        MDiffAt[s]
            ((↑(extChartAt 𝓘(𝕜, F)
                    ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x₀)).2) :
                F → F) ∘
              fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2)
          x₀)
⊢ ContinuousWithinAt f s x₀ ∧ MDiffAt[s] ((↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) : TotalSpace F E → EB × F) ∘ f) x₀ ↔
    (ContinuousWithinAt.{u_5, u_2} (Y := B) (fun (x : M) ↦ (f x).proj (E := E)) s x₀ ∧
        MDiffAt[s] ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ∘ fun (x : M) ↦ (f x).proj (E := E)) x₀) ∧
      ContinuousWithinAt.{u_5, u_4} (Y := F)
          (fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) s x₀ ∧
        MDiffAt[s]
            ((↑(extChartAt 𝓘(𝕜, F)
                    ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x₀)).2) :
                F → F) ∘
              fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2)
          x₀

Tactic:
rw [and_and_and_comm, ← FiberBundle.continuousWithinAt_totalSpace, and_congr_right_iff]

Premises used: FiberBundle.continuousWithinAt_totalSpace, and_congr_right_iff, and_and_and_comm
-- 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₀
simp_rw :
  (MDiffAt[s] 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₀ ∧
      (MDiffAt[s] fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) x₀
⊢ MDiffAt[s] ((↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) : TotalSpace F E → EB × F) ∘ f) x₀ ↔
    MDiffAt[s] ((↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ∘ fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧
      MDiffAt[s]
          ((↑(extChartAt 𝓘(𝕜, F) ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x₀)).2) :
              F → F) ∘
            fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2)
        x₀

Tactic:
simp_rw +instances [modelWithCornersSelf_prod, FiberBundle.extChartAt, Function.comp_def,
    PartialEquiv.trans_apply, PartialEquiv.prod_coe, PartialEquiv.refl_coe,
    extChartAt_self_apply, modelWithCornersSelf_coe, Function.id_def, ← chartedSpaceSelf_prod]

Premises used: Function.id_def, PartialEquiv.trans_apply, chartedSpaceSelf_prod, extChartAt_self_apply, FiberBundle.extChartAt, modelWithCornersSelf_prod, Function.comp_def, PartialEquiv.prod_coe, modelWithCornersSelf_coe, PartialEquiv.refl_coe