awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ 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
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;
MDiffAt aux 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₁
-- 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
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
⊢ 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
have 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
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₁
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
⊢ 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₀
have 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₀
Tactic: simp +singlePass only [mdifferentiableWithinAt_iff_target]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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
⊢ 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₀
have 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₀)
Tactic: rw [and_and_and_comm, ← FiberBundle.continuousWithinAt_totalSpace, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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₀
⊢ 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₀
have 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₀
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]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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₀
⊢ (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₀
have refine : MDiffAt[s]
      (Function.comp (β := EB × F) Prod.fst 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₀
Tactic: refine (mdifferentiableWithinAt_prod_iff _).trans (and_congr ?_ Iff.rfl)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (hypothesis)
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₀
⊢ MDiffAt[s]
        (Function.comp (β := EB × F) Prod.fst 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₀
have h1 : (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
Tactic: have h1 : (fun x => (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀ :=
    ((FiberBundle.continuous_proj F E).continuousWithinAt.comp hf (mapsTo_image f s))
      ((Trivialization.open_baseSet _).mem_nhds (mem_baseSet_trivializationAt F E _))
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
⊢ MDiffAt[s]
        (Function.comp (β := EB × F) Prod.fst 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₀
have refine_1 : ∀ (x : M)
  (hx :
    Membership.mem (γ := Set M)
      ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))) x),
  Eq.{u_7 + 1} (α := EB) ((fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) x)
    (Function.comp (β := EB × F) Prod.fst
      (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)
Tactic: refine EventuallyEq.mdifferentiableWithinAt_iff (eventually_of_mem h1 fun x hx => ?_) ?_
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
x : M
hx :
  Membership.mem (γ := Set M)
    ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))) x
⊢ Eq.{u_7 + 1} (α := EB) ((fun (x : M) ↦ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E))) x)
    (Function.comp (β := EB × F) Prod.fst
      (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)
have refine_1 : (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E)) =
  (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
    ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).1
Tactic: simp_rw [Function.comp, OpenPartialHomeomorph.coe_coe, Trivialization.coe_coe]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
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₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
x : M
hx :
  Membership.mem (γ := Set M)
    ((fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))) x
⊢ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x).proj (E := E)) =
    (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB)
      ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).1
have refine_1 : (f x).proj (E := E) ∈ Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))
Tactic: rw [Trivialization.coe_fst']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
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
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
s : (b : B) → E b
u : Set B
b₀ : B
⊢ MDiffAt[u] (T% s) b₀ ↔
    (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E b₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) b₀
have rw : (MDiffAt[u] fun (x : B) ↦ ⟨x, s x⟩.proj (E := E)) b₀ ∧
    (MDiffAt[u] fun (x : B) ↦
        ((↑(trivializationAt F E (⟨b₀, s b₀⟩.proj (E := E))) : TotalSpace F E → B × F) ⟨x, s x⟩).2)
      b₀ ↔
  (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E b₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) b₀
Tactic: rw [mdifferentiableWithinAt_totalSpace]