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 : (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 : TotalSpace F V → M × F) ⟨x₀, (-s) x₀⟩).2 = -((↑e : TotalSpace F V → M × F) ⟨x₀, s x₀⟩).2

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

Premises used: FiberBundle.mem_baseSet_trivializationAt', IsLinearMap.map_neg, Bundle.Trivialization.linear
-- 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
x₀ : M
hs : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s 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 : (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₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (-s) x⟩) Set.univ x₀

Tactic:
hs.neg_section

Premises used: ContMDiffWithinAt.neg_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
x₀ : M
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) Set.univ x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (-s) x⟩) Set.univ x₀

Tactic:
exact hs.neg_section

Premises used: ContMDiffWithinAt.neg_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
hs : ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (-s) x⟩) u

Tactic:
fun x₀ hx₀ ↦ (hs x₀ hx₀).neg_section

Premises used: ContMDiffWithinAt.neg_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 : (x : M) → V x
hs : ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, s x⟩
⊢ ContMDiff I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n fun (x : M) ↦ ⟨x, (-s) x⟩

Tactic:
fun x₀ ↦ (hs x₀).neg_section

Premises used: ContMDiff, ContMDiffAt.neg_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
x₀ : M
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u x₀
ht : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u x₀
rw : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + -t) x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s - t) x⟩) u x₀

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_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 t : (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₀
ht : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + -t) x⟩) u x₀

Tactic:
hs.add_section ht.neg_section

Premises used: ContMDiffWithinAt.add_section, ContMDiffWithinAt.neg_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
x₀ : M
hs : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, s x⟩) u x₀
ht : ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, t x⟩) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + -t) x⟩) u x₀

Tactic:
exact hs.add_section ht.neg_section

Premises used: ContMDiffWithinAt.add_section, ContMDiffWithinAt.neg_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 : 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₀
rw : ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + -t) x⟩) x₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s - t) x⟩) x₀

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_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 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₀
⊢ ContMDiffAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (s + -t) x⟩) x₀

Tactic:
apply hs.add_section ht.neg_section

Premises used: ContMDiffAt.add_section, ContMDiffAt.neg_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₀).sub_section (ht x₀ hx₀)

Premises used: ContMDiffWithinAt.sub_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₀).sub_section (ht x₀)

Premises used: ContMDiff, ContMDiffAt.sub_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
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
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, (f • s) x⟩).2) u x₀
⊢ ContMDiffWithinAt I (I.prod 𝓘(𝕜, F)) (M' := TotalSpace F V) n (fun (x : M) ↦ ⟨x, (f • 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
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
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, (f • s) x⟩).2) u x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n
    (fun (x : M) ↦ ((↑(trivializationAt F V x₀) : TotalSpace F V → M × F) ⟨x, (f • 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
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
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, (f • s) x⟩).2) u x₀

Tactic:
(hf.smul hs).congr_of_eventuallyEq ?_ ?_

Premises used: ContMDiffWithinAt.smul, ContMDiffWithinAt.congr_of_eventuallyEq
-- 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
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
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 :
  (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) =ᶠ[nhdsWithin x₀ u]
    HSMul.hSMul (β := M → F) f fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2
refine_2 :
  ((↑e : TotalSpace F V → M × F) ⟨x₀, (f • s) x₀⟩).2 =
    HSMul.hSMul (β := M → F) f (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) x₀
⊢ ContMDiffWithinAt I 𝓘(𝕜, F) (M' := F) n (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) u x₀

Tactic:
refine (hf.smul hs).congr_of_eventuallyEq ?_ ?_

Premises used: ContMDiffWithinAt.smul, ContMDiffWithinAt.congr_of_eventuallyEq
-- 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
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
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,
    (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) x =
      HSMul.hSMul (β := M → F) 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, (f • s) x⟩).2) =ᶠ[nhdsWithin x₀ u]
    HSMul.hSMul (β := M → F) f 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
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
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
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
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
f : M → 𝕜
s : (x : M) → V x
u : Set M
x₀ : M
hf : ContMDiffWithinAt I 𝓘(𝕜, 𝕜) n f u x₀
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
⊢ (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, (f • s) x⟩).2) x =
    HSMul.hSMul (β := M → F) f (fun (x : M) ↦ ((↑e : TotalSpace F V → M × F) ⟨x, s x⟩).2) x

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

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