awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
hϕ : (MDiffAt[univ] fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀
hv : (MDiffAt[univ] fun (m : M) ↦ ⟨b₁ m, v m⟩) m₀
hb₂ : MDiffAt[univ] b₂ m₀
⊢ (MDiffAt[univ] fun (m : M) ↦ ⟨b₂ m, (ϕ m : (a : E₁ (b₁ m)) → E₂ (b₂ m)) (v m)⟩) m₀

Tactic:
exact MDifferentiableWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂

Premises used: MDifferentiableWithinAt.clm_apply_of_inCoordinates
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
⊢ ∃ s ∈ 𝓝 x₀, ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) s

Tactic:
⟨t.baseSet, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Bundle.Trivialization.baseSet
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
refine_1 : t.baseSet ∈ 𝓝 x₀
refine_2 :
  ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) t.baseSet
⊢ ∃ s ∈ 𝓝 x₀, ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) s

Tactic:
refine ⟨t.baseSet, ?_, ?_⟩
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
⊢ t.baseSet ∈ 𝓝 x₀

Tactic:
t.open_baseSet.mem_nhds ?_

Premises used: Bundle.Trivialization.open_baseSet, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
refine_1 : x₀ ∈ t.baseSet
⊢ t.baseSet ∈ 𝓝 x₀

Tactic:
refine t.open_baseSet.mem_nhds ?_

Premises used: Bundle.Trivialization.open_baseSet, IsOpen.mem_nhds
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
⊢ x₀ ∈ t.baseSet

Tactic:
FiberBundle.mem_baseSet_trivializationAt' x₀

Premises used: FiberBundle.mem_baseSet_trivializationAt', Set.Mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
⊢ x₀ ∈ t.baseSet

Tactic:
exact FiberBundle.mem_baseSet_trivializationAt' x₀

Premises used: FiberBundle.mem_baseSet_trivializationAt'
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
this :
  ContMDiffOn I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x, extend F (E := V) σ₀ x⟩).2)
    t.baseSet
x : M
hx : x ∈ t.baseSet
rw :
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x, extend F (E := V) σ₀ x⟩).2)
    t.baseSet x
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) t.baseSet
    x

Tactic:
rw [t.contMDiffWithinAt_section _ hx]

Premises used: Bundle.Trivialization.contMDiffWithinAt_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
this :
  ContMDiffOn I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x, extend F (E := V) σ₀ x⟩).2)
    t.baseSet
x : M
hx : x ∈ t.baseSet
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x, extend F (E := V) σ₀ x⟩).2)
    t.baseSet x

Tactic:
this x hx
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
this :
  ContMDiffOn I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x, extend F (E := V) σ₀ x⟩).2)
    t.baseSet
x : M
hx : x ∈ t.baseSet
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x, extend F (E := V) σ₀ x⟩).2)
    t.baseSet x

Tactic:
exact this x hx
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
refine_2 :
  ContMDiffOn I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x, extend F (E := V) σ₀ x⟩).2)
    t.baseSet
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) t.baseSet

Tactic:
suffices ContMDiffOn I 𝓘(𝕜, F) k (fun x ↦ (t ⟨x, extend F σ₀ x⟩).2) t.baseSet by
    intro x hx
    rw [t.contMDiffWithinAt_section _ hx]
    exact this x hx
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
w : F := ((↑t : TotalSpace F V → M × F) ⟨x₀, σ₀⟩).2
⊢ ContMDiffOn I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) t.baseSet

Tactic:
have : ContMDiffOn I 𝓘(𝕜, F) k (fun _x ↦ w) t.baseSet := contMDiffOn_const
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
w : F := ((↑t : TotalSpace F V → M × F) ⟨x₀, σ₀⟩).2
this : ContMDiffOn I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) t.baseSet
x : M
hx : x ∈ t.baseSet
⊢ ((↑t : TotalSpace F V → M × F) ⟨x, extend F (E := V) σ₀ x⟩).2 = w

Tactic:
simp [extend, t, w, hx]

Premises used: FiberBundle.extend
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
inst_14 : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
w : F := ((↑t : TotalSpace F V → M × F) ⟨x₀, σ₀⟩).2
this : ContMDiffOn I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) t.baseSet
⊢ ContMDiffOn I 𝓘(𝕜, F) (M' := F) k (fun (x : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x, extend F (E := V) σ₀ x⟩).2)
    t.baseSet

Tactic:
exact this.congr (fun x hx ↦ by simp [extend, t, w, hx])

Premises used: ContMDiffOn.congr
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
rw :
  ContMDiffAt I 𝓘(𝕜, F) (M' := F) k
    (fun (x_1 : M) ↦ ((↑(trivializationAt F V x) : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) x
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) k (fun (x' : M) ↦ ⟨x', extend F (E := V) σ₀ x'⟩) x

Tactic:
rw [contMDiffAt_section]

Premises used: Bundle.contMDiffAt_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
set :
  let t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x;
  ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2)
    x
⊢ ContMDiffAt I 𝓘(𝕜, F) (M' := F) k
    (fun (x_1 : M) ↦ ((↑(trivializationAt F V x) : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) x

Tactic:
set t := trivializationAt F V x

Premises used: FiberBundle.trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
w : F := ((↑t : TotalSpace F V → M × F) ⟨x, σ₀⟩).2
⊢ ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) x

Tactic:
have : CMDiffAt k (fun (_x : M) ↦ w) x := contMDiffAt_const
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
w : F := ((↑t : TotalSpace F V → M × F) ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) x
⊢ ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2)
    x

Tactic:
this.congr_of_eventuallyEq ?_

Premises used: ContMDiffAt.congr_of_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
w : F := ((↑t : TotalSpace F V → M × F) ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) x
refine :
  EventuallyEq.{u_4, u_5} (β := F) (𝓝 x)
    (fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) fun (_x : M) ↦ w
⊢ ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2)
    x

Tactic:
refine this.congr_of_eventuallyEq ?_

Premises used: ContMDiffAt.congr_of_eventuallyEq
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
w : F := ((↑t : TotalSpace F V → M × F) ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) x
apply :
  ∃ (t_1 : Set M),
    (∀ y ∈ t_1,
        Eq.{u_5 + 1} (α := F) ((fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) y)
          ((fun (_x : M) ↦ w) y)) ∧
      IsOpen[inst_4] t_1 ∧ x ∈ t_1
⊢ EventuallyEq.{u_4, u_5} (β := F) (𝓝 x)
    (fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) fun (_x : M) ↦ w

Tactic:
apply eventually_nhds_iff.mpr

Premises used: Iff.mpr, eventually_nhds_iff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
F : Type u_5
inst_6 : NormedAddCommGroup F
V : M → Type u_6
inst_7 : TopologicalSpace (TotalSpace F V)
inst_8 : (x : M) → AddCommGroup (V x)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x
w : F := ((↑t : TotalSpace F V → M × F) ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) (M' := F) k (fun (_x : M) ↦ w) x
⊢ ∃ (t_1 : Set M),
    (∀ y ∈ t_1,
        Eq.{u_5 + 1} (α := F) ((fun (x_1 : M) ↦ ((↑t : TotalSpace F V → M × F) ⟨x_1, extend F (E := V) σ₀ x_1⟩).2) y)
          ((fun (_x : M) ↦ w) y)) ∧
      IsOpen[inst_4] t_1 ∧ x ∈ t_1

Tactic:
⟨t.baseSet, ?_, t.open_baseSet, ?_⟩

Premises used: Bundle.Trivialization.open_baseSet, And.intro, Exists.intro, Bundle.Trivialization.baseSet