awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀
⊢ (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:
(mdifferentiableWithinAt_prod_iff _).trans (and_congr ?_ Iff.rfl)

Premises used: Iff.rfl, setOf, instTopologicalSpaceModelProd._aux_1, Iff.trans, mdifferentiableWithinAt_prod_iff, ModelProd, and_congr
-- 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₀
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₀
⊢ (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:
refine (mdifferentiableWithinAt_prod_iff _).trans (and_congr ?_ Iff.rfl)

Premises used: Iff.rfl, Iff.trans, mdifferentiableWithinAt_prod_iff, and_congr
-- 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₀
⊢ (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 _))
-- 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₀
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₀

Tactic:
EventuallyEq.mdifferentiableWithinAt_iff (eventually_of_mem h1 fun x hx => ?_) ?_

Premises used: Filter.eventually_of_mem, Filter.EventuallyEq.mdifferentiableWithinAt_iff
-- 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₀
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
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
⊢ 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:
simp_rw [Function.comp, OpenPartialHomeomorph.coe_coe, Trivialization.coe_coe]

Premises used: OpenPartialHomeomorph.coe_coe, Function.comp, Bundle.Trivialization.coe_coe
-- 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₀
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
refine_1 : (f x).proj (E := E) ∈ Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))
⊢ (↑(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:
rw [Trivialization.coe_fst']

Premises used: Bundle.Trivialization.coe_fst'
-- 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₀
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
⊢ (f x).proj (E := E) ∈ Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))

Tactic:
hx

Premises used: Set.Mem, setOf, Set.preimage
-- 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₀
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
⊢ (f x).proj (E := E) ∈ Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E)))

Tactic:
exact hx
-- 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₀
h1 :
  (fun (x : M) ↦ (f x).proj (E := E)) ⁻¹' Trivialization.baseSet (trivializationAt F E ((f x₀).proj (E := E))) ∈ 𝓝[s] x₀
⊢ (↑(extChartAt IB ((f x₀).proj (E := E))) : B → EB) ((f x₀).proj (E := E)) =
    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:
simp only [mfld_simps]
-- 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
x₀ : M
⊢ MDiffAt f x₀ ↔
    (MDiffAt fun (x : M) ↦ (f x).proj (E := E)) x₀ ∧
      (MDiffAt fun (x : M) ↦ ((↑(trivializationAt F E ((f x₀).proj (E := E))) : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
simpa [← mdifferentiableWithinAt_univ] using mdifferentiableWithinAt_totalSpace _ f

Premises used: mdifferentiableWithinAt_totalSpace, mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
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₀
⊢ MDiffAt[u] (T% s) b₀ ↔
    (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E b₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) b₀

Tactic:
rw [mdifferentiableWithinAt_totalSpace]

Premises used: mdifferentiableWithinAt_totalSpace
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
change :
  MDiffAt[u] id 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₀
⊢ (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:
change MDifferentiableWithinAt _ _ id _ _ ∧ _ ↔ _

Premises used: id, MDifferentiableWithinAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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] id 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:
simp [mdifferentiableWithinAt_id]

Premises used: mdifferentiableWithinAt_id
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
b₀ : B
⊢ MDiffAt (T% s) b₀ ↔ (MDiffAt fun (b : B) ↦ ((↑(trivializationAt F E b₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) b₀

Tactic:
simpa [← mdifferentiableWithinAt_univ] using mdifferentiableWithinAt_section _ _

Premises used: mdifferentiableWithinAt_section, mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
x : TotalSpace F E
⊢ MDiffAt id x

Tactic:
have : MDifferentiableAt (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) id x := mdifferentiableAt_id
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
x : TotalSpace F E
this : MDiffAt id x
⊢ (MDiffAt fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) x ∧
    (MDiffAt fun (x_1 : TotalSpace F E) ↦
        ((↑(trivializationAt F E ((id x).proj (E := E))) : TotalSpace F E → B × F) (id x_1)).2)
      x

Tactic:
rw [mdifferentiableAt_totalSpace] at this

Premises used: mdifferentiableAt_totalSpace
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
x : TotalSpace F E
this :
  (MDiffAt fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) x ∧
    (MDiffAt fun (x_1 : TotalSpace F E) ↦
        ((↑(trivializationAt F E ((id x).proj (E := E))) : TotalSpace F E → B × F) (id x_1)).2)
      x
⊢ MDiffAt (TotalSpace.proj (E := E)) x

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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
x : TotalSpace F E
this :
  (MDiffAt fun (x : TotalSpace F E) ↦ (id x).proj (E := E)) x ∧
    (MDiffAt fun (x_1 : TotalSpace F E) ↦
        ((↑(trivializationAt F E ((id x).proj (E := E))) : TotalSpace F E → B × F) (id x_1)).2)
      x
⊢ MDiffAt (TotalSpace.proj (E := E)) x

Tactic:
exact this.1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
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 : Set (TotalSpace F E)
⊢ MDiff[s] (TotalSpace.proj (E := E))

Tactic:
(mdifferentiable_proj E).mdifferentiableOn

Premises used: Bundle.mdifferentiable_proj, MDifferentiable.mdifferentiableOn