awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀
refine_1 : e.baseSet ∈ nhdsWithin x₀ u
refine_1₁ :
  ∀ x ∈ e.baseSet,
    (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) x =
      HAdd.hAdd (α := M → F) (β := M → F) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2)
        (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) x
⊢ (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) =ᶠ[nhdsWithin x₀ u]
    HAdd.hAdd (α := M → F) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) fun (x : M) ↦
      ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2

Tactic:
apply eventually_of_mem (U := e.baseSet)

Premises used: Filter.eventually_of_mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀
⊢ e.baseSet ∈ nhdsWithin x₀ u

Tactic:
mem_nhdsWithin_of_mem_nhds <|
        (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀)

Premises used: Bundle.Trivialization.open_baseSet, mem_nhdsWithin_of_mem_nhds, IsOpen.mem_nhds, FiberBundle.mem_baseSet_trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀
⊢ e.baseSet ∈ nhdsWithin x₀ u

Tactic:
exact mem_nhdsWithin_of_mem_nhds <|
        (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀)

Premises used: Bundle.Trivialization.open_baseSet, mem_nhdsWithin_of_mem_nhds, IsOpen.mem_nhds, FiberBundle.mem_baseSet_trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀
x : M
hx : x ∈ e.baseSet
⊢ (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (s + t) x⟩).2) x =
    HAdd.hAdd (α := M → F) (β := M → F) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2)
      (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) x

Tactic:
apply (e.linear 𝕜 hx).1

Premises used: Bundle.Trivialization.linear, IsLinearMap.map_add
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
ht : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) u x₀
⊢ ((↑e : TotalSpace F V → M × F) ⟨x₀, (s + t) x₀⟩).2 =
    HAdd.hAdd (α := M → F) (β := M → F) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2)
      (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, t x⟩).2) x₀

Tactic:
apply (e.linear 𝕜 (FiberBundle.mem_baseSet_trivializationAt' x₀)).1

Premises used: FiberBundle.mem_baseSet_trivializationAt', Bundle.Trivialization.linear, IsLinearMap.map_add
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
x₀ : M
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) x₀
ht : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) Set.univ x₀

Tactic:
rw [← contMDiffWithinAt_univ] at hs ⊢

Premises used: contMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
x₀ : M
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) x₀
ht : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x₀
hs₁ : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) Set.univ x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x₀

Tactic:
rw [← contMDiffWithinAt_univ] at hs ⊢

Premises used: contMDiffWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
x₀ : M
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) Set.univ x₀
ht : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + t) x⟩) Set.univ x₀

Tactic:
hs.add_section ht

Premises used: ContMDiffWithinAt.add_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
x₀ : M
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) Set.univ x₀
ht : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + t) x⟩) Set.univ x₀

Tactic:
exact hs.add_section ht

Premises used: ContMDiffWithinAt.add_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
u : Set M
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u
ht : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + t) x⟩) u

Tactic:
fun x₀ hx₀ ↦ (hs x₀ hx₀).add_section (ht x₀ hx₀)

Premises used: ContMDiffWithinAt.add_section, ContMDiffOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s t : (x : M) → V x
hs : ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, s x⟩
ht : ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, t x⟩
⊢ ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, (s + t) x⟩

Tactic:
fun x₀ ↦ (hs x₀).add_section (ht x₀)

Premises used: ContMDiffAt.add_section, ContMDiff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u x₀
rw :
  ∀
    (hs :
      ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
        (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀),
    ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
      (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (-s) x⟩) u x₀

Tactic:
rw [contMDiffWithinAt_section] at hs ⊢

Premises used: Bundle.contMDiffWithinAt_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
hs :
  ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
set :
  let e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀;
  ∀ (hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀),
    ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) u x₀

Tactic:
set e := trivializationAt F V x₀

Premises used: FiberBundle.trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) u x₀

Tactic:
hs.neg.congr_of_eventuallyEq ?_ ?_

Premises used: ContMDiffWithinAt.congr_of_eventuallyEq, ContMDiffWithinAt.neg
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
refine_1 :
  EventuallyEq.{u_4, u_5} (β := F) (nhdsWithin x₀ u) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2)
    fun (x : M) ↦ -((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2
refine_2 : ((↑e : TotalSpace F V → M × F) ⟨x₀, (-s) x₀⟩).2 = -((↑e : TotalSpace F V → M × F) ⟨x₀, s x₀⟩).2
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) u x₀

Tactic:
refine hs.neg.congr_of_eventuallyEq ?_ ?_

Premises used: ContMDiffWithinAt.congr_of_eventuallyEq, ContMDiffWithinAt.neg
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
refine_1 : e.baseSet ∈ nhdsWithin x₀ u
refine_1₁ :
  ∀ x ∈ e.baseSet,
    Eq.{u_5 + 1} (α := F) ((fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) x)
      ((fun (x : M) ↦ -((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) x)
⊢ EventuallyEq.{u_4, u_5} (β := F) (nhdsWithin x₀ u) (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2)
    fun (x : M) ↦ -((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2

Tactic:
apply eventually_of_mem (U := e.baseSet)

Premises used: Filter.eventually_of_mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
⊢ e.baseSet ∈ nhdsWithin x₀ u

Tactic:
mem_nhdsWithin_of_mem_nhds <|
        (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀)

Premises used: Bundle.Trivialization.open_baseSet, mem_nhdsWithin_of_mem_nhds, IsOpen.mem_nhds, FiberBundle.mem_baseSet_trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
⊢ e.baseSet ∈ nhdsWithin x₀ u

Tactic:
exact mem_nhdsWithin_of_mem_nhds <|
        (e.open_baseSet.mem_nhds <| mem_baseSet_trivializationAt F V x₀)

Premises used: Bundle.Trivialization.open_baseSet, mem_nhdsWithin_of_mem_nhds, IsOpen.mem_nhds, FiberBundle.mem_baseSet_trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
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
inst_7 : NormedSpace 𝕜 F
n : ℕ∞ω
V : M → Type u_6
inst_8 : TopologicalSpace (TotalSpace F V)
inst_9 : (x : M) → TopologicalSpace (V x)
inst_10 : FiberBundle F V
inst_11 : (x : M) → AddCommGroup (V x)
inst_12 : (x : M) → Module.{u_1, u_6} 𝕜 (V x)
inst_13 : VectorBundle 𝕜 F V
s : (x : M) → V x
u : Set M
x₀ : M
e : Trivialization (B := M) F (Z := TotalSpace F V) (TotalSpace.proj (E := V)) := trivializationAt F V x₀
hs : ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) u x₀
x : M
hx : x ∈ e.baseSet
⊢ Eq.{u_5 + 1} (α := F) ((fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (-s) x⟩).2) x)
    ((fun (x : M) ↦ -((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) x)

Tactic:
apply (e.linear 𝕜 hx).map_neg

Premises used: IsLinearMap.map_neg, Bundle.Trivialization.linear