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
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)
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)

Tactic:
(Trivialization.coordChangeL_apply' e e' hy (g y)).symm

Premises used: Bundle.Trivialization.coordChange, Bundle.Trivialization.coordChangeL_apply', Eq.symm
-- 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)
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)

Tactic:
exact (Trivialization.coordChangeL_apply' e e' hy (g y)).symm

Premises used: Bundle.Trivialization.coordChangeL_apply', Eq.symm
-- 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.coordChange e' (f x) (g x) =
    ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)

Tactic:
(Trivialization.coordChangeL_apply' e e' ⟨he, he'⟩ (g x)).symm

Premises used: Bundle.Trivialization.coordChange, And.intro, Bundle.Trivialization.coordChangeL_apply', Eq.symm
-- 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.coordChange e' (f x) (g x) =
    ((↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f x)) : F →L[𝕜] F) : (a : F) → F) (g x)

Tactic:
exact (Trivialization.coordChangeL_apply' e e' ⟨he, he'⟩ (g x)).symm

Premises used: And.intro, Bundle.Trivialization.coordChangeL_apply', Eq.symm
-- 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
g : M → F
x : M
hf : MDiffAt f x
hg : MDiffAt g x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ (MDiffAt fun (y : M) ↦ e.coordChange e' (f y) (g y)) x

Tactic:
MDifferentiableWithinAt.coordChange hf hg he he'

Premises used: MDifferentiableWithinAt.coordChange, MDifferentiableAt, 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
g : M → F
hf : MDiff[s] f
hg : MDiff[s] g
he : MapsTo f s e.baseSet
he' : MapsTo f s e'.baseSet
⊢ MDiff[s] fun (y : M) ↦ e.coordChange e' (f y) (g y)

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

Premises used: MDifferentiableWithinAt.coordChange, 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
g : M → F
hf : MDiff f
hg : MDiff g
he : ∀ (x : M), f x ∈ e.baseSet
he' : ∀ (x : M), f x ∈ e'.baseSet
⊢ MDiff fun (y : M) ↦ e.coordChange e' (f y) (g y)

Tactic:
fun x ↦
  (hf x).coordChange (hg x) (he x) (he' x)

Premises used: MDifferentiableAt.coordChange, 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)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
he'f : (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
he : f x₀ ∈ e.source
he' : f x₀ ∈ e'.source
⊢ (f x₀).proj (E := E) ∈ e.baseSet

Tactic:
rw [Trivialization.mem_source] at he he'

Premises used: Bundle.Trivialization.mem_source
-- 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)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
he'f : (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
he : f x₀ ∈ e.source
he' : f x₀ ∈ e'.source
he₁ : (f x₀).proj (E := E) ∈ e.baseSet
⊢ (f x₀).proj (E := E) ∈ e'.baseSet

Tactic:
rw [Trivialization.mem_source] at he he'

Premises used: Bundle.Trivialization.mem_source
-- 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)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
he'f : (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
he : (f x₀).proj (E := E) ∈ e.baseSet
he' : (f x₀).proj (E := E) ∈ e'.baseSet
⊢ ((↑e' : TotalSpace F E → B × F) (f x₀)).2 =
    e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) x₀) ((↑e : TotalSpace F E → B × F) (f x₀)).2

Tactic:
simp [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)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
he'f : (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
he : (f x₀).proj (E := E) ∈ e.baseSet
he' : (f x₀).proj (E := E) ∈ e'.baseSet
refine :
  EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x₀) (fun (x : M) ↦ ((↑e' : TotalSpace F E → B × F) (f x)).2) fun (y : M) ↦
    e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2
⊢ (MDiffAt[s] fun (x : M) ↦ ((↑e' : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
refine (hf.coordChange he'f he he').congr_of_eventuallyEq ?_ (by simp [he])

Premises used: MDifferentiableWithinAt.coordChange, MDifferentiableWithinAt.congr_of_eventuallyEq
-- 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)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
he'f : (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
he : (f x₀).proj (E := E) ∈ e.baseSet
he' : (f x₀).proj (E := E) ∈ e'.baseSet
h :
  ∀ (y : M) (hy : y ∈ TotalSpace.proj (E := E) ∘ f ⁻¹' e.baseSet),
    ((↑e' : TotalSpace F E → B × F) (f y)).2 =
      e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2
⊢ EventuallyEq.{u_5, u_4} (β := F) (𝓝[s] x₀) (fun (x : M) ↦ ((↑e' : TotalSpace F E → B × F) (f x)).2) fun (y : M) ↦
    e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2

Tactic:
filter_upwards [hf.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy

Premises used: Bundle.Trivialization.open_baseSet, IsOpen.mem_nhds, MDifferentiableWithinAt.continuousWithinAt
-- 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)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
he'f : (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀
he : (f x₀).proj (E := E) ∈ e.baseSet
he' : (f x₀).proj (E := E) ∈ e'.baseSet
y : M
hy : y ∈ TotalSpace.proj (E := E) ∘ f ⁻¹' e.baseSet
⊢ ((↑e' : TotalSpace F E → B × F) (f y)).2 =
    e.coordChange e' ((TotalSpace.proj (E := E) ∘ f) y) ((↑e : TotalSpace F E → B × F) (f y)).2

Tactic:
simp_all
-- 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)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
s : Set M
x₀ : M
hex₀ : f x₀ ∈ e.source
he'x₀ : f x₀ ∈ e'.source
hf : MDiffAt[s] (TotalSpace.proj (E := E) ∘ f) x₀
⊢ (MDiffAt[s] fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀ ↔
    (MDiffAt[s] fun (x : M) ↦ ((↑e' : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
⟨(hf.change_section_trivialization IB · hex₀ he'x₀),
   (hf.change_section_trivialization IB · he'x₀ hex₀)⟩

Premises used: Iff.intro, MDifferentiableWithinAt.change_section_trivialization
-- 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)
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle 1 F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_20 : MemTrivializationAtlas (E := E) e
inst_21 : MemTrivializationAtlas (E := E) e'
f : M → TotalSpace F E
x₀ : M
he : f x₀ ∈ e.source
he' : f x₀ ∈ e'.source
hf : (MDiffAt fun (x : M) ↦ (f x).proj (E := E)) x₀
⊢ (MDiffAt fun (x : M) ↦ ((↑e : TotalSpace F E → B × F) (f x)).2) x₀ ↔
    (MDiffAt fun (x : M) ↦ ((↑e' : TotalSpace F E → B × F) (f x)).2) x₀

Tactic:
simpa [← mdifferentiableWithinAt_univ] using
    e.mdifferentiableWithinAt_snd_comp_iff₂ IB he he' hf

Premises used: mdifferentiableWithinAt_univ, Bundle.Trivialization.mdifferentiableWithinAt_snd_comp_iff₂