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
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
p : TotalSpace F E
⊢ MDiffAt (TotalSpace.proj (E := E)) p

Tactic:
(mdifferentiable_proj E).mdifferentiableAt

Premises used: MDifferentiable.mdifferentiableAt, Bundle.mdifferentiable_proj
-- 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)
p : TotalSpace F E
⊢ MDiffAt[s] (TotalSpace.proj (E := E)) p

Tactic:
(mdifferentiableAt_proj E).mdifferentiableWithinAt

Premises used: Bundle.mdifferentiableAt_proj, MDifferentiableAt.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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
rw : (MDiffAt fun (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 0⟩).2) x
⊢ (MDiffAt fun (x : B) ↦ ⟨x, 0⟩) x

Tactic:
rw [mdifferentiableAt_section]

Premises used: mdifferentiableAt_section
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
apply :
  EventuallyEq.{u_2, u_4} (β := F) (𝓝 x) (fun (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 0⟩).2)
    fun (x : B) ↦ 0
⊢ (MDiffAt fun (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 0⟩).2) x

Tactic:
apply (mdifferentiableAt_const (c := 0)).congr_of_eventuallyEq

Premises used: MDifferentiableAt.congr_of_eventuallyEq, mdifferentiableAt_const
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x y : B
hy : y ∈ Trivialization.baseSet (trivializationAt F E x)
⊢ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨y, 0⟩).2 = 0

Tactic:
congr_arg Prod.snd <| (trivializationAt F E x).zeroSection 𝕜 hy

Premises used: Bundle.zeroSection, Bundle.Trivialization.zeroSection, congr_arg, FiberBundle.trivializationAt, Prod.snd
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
h :
  ∀ (a : B),
    Membership.mem (γ := Set B)
      {x_1 : B |
        x_1 ∈ Trivialization.baseSet (trivializationAt F E x) →
          Membership.mem (γ := Set B)
            {x_2 : B |
              (fun (x_3 : B) ↦
                  Eq.{u_4 + 1} (α := F)
                    ((fun (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 0⟩).2) x_3)
                    ((fun (x : B) ↦ (0 : F)) x_3))
                x_2}
            x_1}
      a
h₁ h₂ :
  ∀ (y : B) (hy : y ∈ Trivialization.baseSet (trivializationAt F E x)),
    ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨y, 0⟩).2 = 0
⊢ EventuallyEq.{u_2, u_4} (β := F) (𝓝 x) (fun (b : B) ↦ ((↑(trivializationAt F E x) : TotalSpace F E → B × F) ⟨b, 0⟩).2)
    fun (x : B) ↦ 0

Tactic:
filter_upwards [(trivializationAt F E x).open_baseSet.mem_nhds
    (mem_baseSet_trivializationAt F E x)] with y hy
    using congr_arg Prod.snd <| (trivializationAt F E x).zeroSection 𝕜 hy

Premises used: Bundle.Trivialization.open_baseSet, congr_arg, FiberBundle.trivializationAt, IsOpen.mem_nhds, FiberBundle.mem_baseSet_trivializationAt, Prod.snd
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
t : Set B
⊢ MDiff[t] (zeroSection F E)

Tactic:
(mdifferentiable_zeroSection _ _).mdifferentiableOn

Premises used: Bundle.mdifferentiable_zeroSection, MDifferentiable.mdifferentiableOn
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
x : B
⊢ MDiffAt (zeroSection F E) x

Tactic:
(mdifferentiable_zeroSection _ _).mdifferentiableAt

Premises used: MDifferentiable.mdifferentiableAt, Bundle.mdifferentiable_zeroSection
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
t : Set B
x : B
⊢ MDiffAt[t] (zeroSection F E) x

Tactic:
(mdifferentiable_zeroSection _ _ x).mdifferentiableWithinAt

Premises used: MDifferentiableAt.mdifferentiableWithinAt, Bundle.mdifferentiable_zeroSection
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_13 : MemTrivializationAtlas (E := E) e
inst_14 : MemTrivializationAtlas (E := E) e'
inst_15 : VectorBundle 𝕜 F E
inst_16 : ContMDiffVectorBundle 1 F E IB
⊢ MDiff[e.baseSet ∩ e'.baseSet] fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)

Tactic:
(contMDiffOn_coordChangeL e e').mdifferentiableOn one_ne_zero

Premises used: contMDiffOn_coordChangeL, one_ne_zero, ContMDiffOn.mdifferentiableOn
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_13 : MemTrivializationAtlas (E := E) e
inst_14 : MemTrivializationAtlas (E := E) e'
inst_15 : VectorBundle 𝕜 F E
inst_16 : ContMDiffVectorBundle 1 F E IB
⊢ MDiff[e.baseSet ∩ e'.baseSet] fun (b : B) ↦
    (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F)

Tactic:
(contMDiffOn_symm_coordChangeL e e').mdifferentiableOn one_ne_zero

Premises used: contMDiffOn_symm_coordChangeL, one_ne_zero, ContMDiffOn.mdifferentiableOn
-- 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
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_13 : MemTrivializationAtlas (E := E) e
inst_14 : MemTrivializationAtlas (E := E) e'
inst_15 : VectorBundle 𝕜 F E
inst_16 : ContMDiffVectorBundle 1 F E IB
x : B
h : x ∈ e.baseSet
h' : x ∈ e'.baseSet
⊢ (MDiffAt fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) x

Tactic:
(contMDiffAt_coordChangeL h h').mdifferentiableAt one_ne_zero

Premises used: ContMDiffAt.mdifferentiableAt, contMDiffAt_coordChangeL, one_ne_zero
-- 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
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
x : M
hf : MDiffAt[s] f x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ (MDiffAt[s] fun (y : M) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f y)) : F →L[𝕜] F)) x

Tactic:
(mdifferentiableAt_coordChangeL he he').comp_mdifferentiableWithinAt _ hf

Premises used: MDifferentiableAt.comp_mdifferentiableWithinAt, mdifferentiableAt_coordChangeL, ContinuousLinearEquiv.toContinuousLinearMap
-- 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
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
f : M → B
x : M
hf : MDiffAt f x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ (MDiffAt fun (y : M) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f y)) : F →L[𝕜] F)) x

Tactic:
MDifferentiableWithinAt.coordChangeL hf he he'

Premises used: MDifferentiableAt, MDifferentiableWithinAt.coordChangeL, ChartedSpace.LiftPropAt
-- 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
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
hf : MDiff[s] f
he : MapsTo f s e.baseSet
he' : MapsTo f s e'.baseSet
⊢ MDiff[s] fun (y : M) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f y)) : F →L[𝕜] F)

Tactic:
fun x hx ↦ (hf x hx).coordChangeL (he hx) (he' hx)

Premises used: MDifferentiableWithinAt.coordChangeL, MDifferentiableOn
-- 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
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
f : M → B
hf : MDiff f
he : ∀ (x : M), f x ∈ e.baseSet
he' : ∀ (x : M), f x ∈ e'.baseSet
⊢ MDiff fun (y : M) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f y)) : F →L[𝕜] F)

Tactic:
fun x ↦ (hf x).coordChangeL (he x) (he' x)

Premises used: MDifferentiableAt.coordChangeL, MDifferentiable
-- 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
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ (MDiffAt[s] fun (y : M) ↦ e.coordChange e' (f y) (g y)) x

Tactic:
((hf.coordChangeL he he').clm_apply hg).congr_of_eventuallyEq ?_ ?_

Premises used: MDifferentiableWithinAt.coordChangeL, MDifferentiableWithinAt.congr_of_eventuallyEq, MDifferentiableWithinAt.clm_apply
-- 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
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
refine_1 :
  EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x) (fun (y : M) ↦ e.coordChange e' (f y) (g y)) fun (x : M) ↦
    ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)
refine_2 :
  e.coordChange e' (f x) (g x) =
    ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)
⊢ (MDiffAt[s] fun (y : M) ↦ e.coordChange e' (f y) (g y)) x

Tactic:
refine ((hf.coordChangeL he he').clm_apply hg).congr_of_eventuallyEq ?_ ?_

Premises used: MDifferentiableWithinAt.coordChangeL, MDifferentiableWithinAt.congr_of_eventuallyEq, MDifferentiableWithinAt.clm_apply
-- 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
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x)

Tactic:
have : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x) :=
     (e.open_baseSet.inter e'.open_baseSet).mem_nhds ⟨he, he'⟩
-- 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
inst_16 : (x : B) → AddCommMonoid (E x)
inst_17 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_18 : MemTrivializationAtlas (E := E) e
inst_19 : MemTrivializationAtlas (E := E) e'
inst_20 : VectorBundle 𝕜 F E
inst_21 : ContMDiffVectorBundle 1 F E IB
s : Set M
f : M → B
g : M → F
x : M
hf : MDiffAt[s] f x
hg : MDiffAt[s] g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
this : e.baseSet ∩ e'.baseSet ∈ 𝓝 (f x)
h :
  ∀ (y : M) (hy : y ∈ f ⁻¹' (e.baseSet ∩ e'.baseSet)),
    e.coordChange e' (f y) (g y) =
      ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f y)) : F →L[𝕜] F) : (a : F) → F) (g y)
⊢ EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x) (fun (y : M) ↦ e.coordChange e' (f y) (g y)) fun (x : M) ↦
    ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)

Tactic:
filter_upwards [hf.continuousWithinAt this] with y hy

Premises used: MDifferentiableWithinAt.continuousWithinAt