awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
inst_16 : MemTrivializationAtlas (E := E) e'
rw :
  ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F))
    (e'.baseSet ∩ e.baseSet)
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F))
    (e.baseSet ∩ e'.baseSet)

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
inst_16 : MemTrivializationAtlas (E := E) e'
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F))
    (e'.baseSet ∩ e.baseSet)

Tactic:
(ContMDiffVectorBundle.contMDiffOn_coordChangeL e' e).congr fun b hb ↦ ?_

Premises used: ContMDiffVectorBundle.contMDiffOn_coordChangeL, ContMDiffOn.congr
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
inst_16 : MemTrivializationAtlas (E := E) e'
refine :
  ∀ (b : B) (hb : b ∈ e'.baseSet ∩ e.baseSet),
    Eq (α := F →L[𝕜] F) (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F)
      (↑(Trivialization.coordChangeL 𝕜 (E := E) e' e b) : F →L[𝕜] F)
⊢ ContMDiffOn.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F))
    (e'.baseSet ∩ e.baseSet)

Tactic:
refine (ContMDiffVectorBundle.contMDiffOn_coordChangeL e' e).congr fun b hb ↦ ?_

Premises used: ContMDiffVectorBundle.contMDiffOn_coordChangeL, ContMDiffOn.congr
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
inst_16 : MemTrivializationAtlas (E := E) e'
b : B
hb : b ∈ e'.baseSet ∩ e.baseSet
rw rw₁ :
  Eq (α := F →L[𝕜] F) (↑(Trivialization.coordChangeL 𝕜 (E := E) e' e b) : F →L[𝕜] F)
    (↑(Trivialization.coordChangeL 𝕜 (E := E) e' e b) : F →L[𝕜] F)
⊢ Eq (α := F →L[𝕜] F) (↑(ContinuousLinearEquiv.symm (Trivialization.coordChangeL 𝕜 (E := E) e e' b)) : F →L[𝕜] F)
    (↑(Trivialization.coordChangeL 𝕜 (E := E) e' e b) : F →L[𝕜] F)

Tactic:
rw [e.symm_coordChangeL e' hb]

Premises used: Bundle.Trivialization.symm_coordChangeL
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_8 : NormedAddCommGroup F
inst_9 : NormedSpace 𝕜 F
inst_10 : TopologicalSpace (TotalSpace F E)
inst_11 : (x : B) → TopologicalSpace (E x)
inst_12 : FiberBundle F E
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle n F E IB
e e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
inst_16 : MemTrivializationAtlas (E := E) e'
x : B
h : x ∈ e.baseSet
h' : x ∈ e'.baseSet
⊢ ContMDiffAt.{u_1, u_7, u_8, u_2, u_4, u_4, u_4} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) x

Tactic:
(contMDiffOn_coordChangeL e e').contMDiffAt <|
    (e.open_baseSet.inter e'.open_baseSet).mem_nhds ⟨h, h'⟩

Premises used: Bundle.Trivialization.open_baseSet, ContMDiffOn.contMDiffAt, And.intro, IsOpen.mem_nhds, IsOpen.inter, contMDiffOn_coordChangeL
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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'
s : Set M
f : M → B
x : M
hf : ContMDiffWithinAt IM IB n f s x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ ContMDiffWithinAt.{u_1, u_9, u_10, u_5, u_4, u_4, u_4} IM (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (y : M) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f y)) : F →L[𝕜] F)) s x

Tactic:
(contMDiffAt_coordChangeL he he').comp_contMDiffWithinAt _ hf

Premises used: contMDiffAt_coordChangeL, ContMDiffAt.comp_contMDiffWithinAt, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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 → B
x : M
hf : ContMDiffAt IM IB n f x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ ContMDiffAt.{u_1, u_9, u_10, u_5, u_4, u_4, u_4} IM (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (y : M) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f y)) : F →L[𝕜] F)) x

Tactic:
hf.coordChangeL he he'

Premises used: ContMDiffAt, ContMDiffWithinAt.coordChangeL
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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'
s : Set M
f : M → B
hf : ContMDiffOn IM IB n f s
he : MapsTo f s e.baseSet
he' : MapsTo f s e'.baseSet
⊢ ContMDiffOn.{u_1, u_9, u_10, u_5, u_4, u_4, u_4} IM (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
    (fun (y : M) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' (f y)) : F →L[𝕜] F)) s

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

Premises used: ContMDiffWithinAt.coordChangeL, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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 → B
hf : ContMDiff IM IB n f
he : ∀ (x : M), f x ∈ e.baseSet
he' : ∀ (x : M), f x ∈ e'.baseSet
⊢ ContMDiff.{u_1, u_9, u_10, u_5, u_4, u_4, u_4} IM (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n 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: ContMDiffAt.coordChangeL, ContMDiff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s x
he : f x ∈ e.baseSet
he' : f x ∈ e'.baseSet
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ e.coordChange e' (f y) (g y)) s x

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

Premises used: ContMDiffWithinAt.clm_apply, ContMDiffWithinAt.coordChangeL, ContMDiffWithinAt.congr_of_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s 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)
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F) (M' := F) n (fun (y : M) ↦ e.coordChange e' (f y) (g y)) s x

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

Premises used: ContMDiffWithinAt.clm_apply, ContMDiffWithinAt.coordChangeL, ContMDiffWithinAt.congr_of_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s 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.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s 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: ContMDiffWithinAt.continuousWithinAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s 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.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s 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.Basic
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n 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'
s : Set M
f : M → B
g : M → F
x : M
hf : ContMDiffWithinAt IM IB n f s x
hg : ContMDiffWithinAt IM 𝓘(𝕜, F) n g s 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