awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
hs : MDiffAt[u] (T% s) x₀
rw :
  ∀ (hs : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀),
    (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, (-s) x⟩) x₀

Tactic:
rw [mdifferentiableWithinAt_section] at hs ⊢

Premises used: mdifferentiableWithinAt_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
hs : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
set :
  let e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀;
  ∀ (hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀),
    (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x₀

Tactic:
set e := trivializationAt F E x₀

Premises used: FiberBundle.trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x₀

Tactic:
hs.neg.congr_of_eventuallyEq ?_ ?_

Premises used: MDifferentiableWithinAt.congr_of_eventuallyEq, MDifferentiableWithinAt.neg
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
refine_1 :
  EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2)
    (-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
refine_2 :
  ((↑e : TotalSpace F E → B × F) ⟨x₀, (-s) x₀⟩).2 = (-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x₀

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

Premises used: MDifferentiableWithinAt.congr_of_eventuallyEq, MDifferentiableWithinAt.neg
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
refine_1 : e.baseSet ∈ 𝓝[u] x₀
refine_1₁ :
  ∀ x ∈ e.baseSet,
    Eq.{u_4 + 1} (α := F) ((fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x)
      ((-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x)
⊢ EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2)
    (-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)

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

Premises used: Filter.eventually_of_mem
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ e.baseSet ∈ 𝓝[u] x₀

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

Premises used: Bundle.Trivialization.open_baseSet, mem_nhdsWithin_of_mem_nhds, IsOpen.mem_nhds, FiberBundle.mem_baseSet_trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ e.baseSet ∈ 𝓝[u] x₀

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

Premises used: Bundle.Trivialization.open_baseSet, mem_nhdsWithin_of_mem_nhds, IsOpen.mem_nhds, FiberBundle.mem_baseSet_trivializationAt
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet,
    Eq.{u_4 + 1} (α := F) ((fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x)
      ((-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x)

Tactic:
fun x hx ↦ (e.linear 𝕜 hx).map_neg ..

Premises used: IsLinearMap.map_neg, Bundle.Trivialization.linear
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet,
    Eq.{u_4 + 1} (α := F) ((fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (-s) b⟩).2) x)
      ((-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x)

Tactic:
exact fun x hx ↦ (e.linear 𝕜 hx).map_neg ..

Premises used: IsLinearMap.map_neg, Bundle.Trivialization.linear
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ ((↑e : TotalSpace F E → B × F) ⟨x₀, (-s) x₀⟩).2 = (-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀

Tactic:
(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.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
x₀ : B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E)) := trivializationAt F E x₀
hs : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀
⊢ ((↑e : TotalSpace F E → B × F) ⟨x₀, (-s) x₀⟩).2 = (-fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀

Tactic:
exact (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.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
⊢ MDiffAt[univ] (T% s) x₀

Tactic:
rw [← mdifferentiableWithinAt_univ] at hs ⊢

Premises used: mdifferentiableWithinAt_univ
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
x₀ : B
hs : MDiffAt[univ] (T% s) x₀
⊢ (MDiffAt[univ] fun (x : B) ↦ ⟨x, (-s) x⟩) x₀

Tactic:
mdifferentiableWithinAt_neg_section hs

Premises used: mdifferentiableWithinAt_neg_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
x₀ : B
hs : MDiffAt[univ] (T% s) x₀
⊢ (MDiffAt[univ] fun (x : B) ↦ ⟨x, (-s) x⟩) x₀

Tactic:
exact mdifferentiableWithinAt_neg_section hs

Premises used: mdifferentiableWithinAt_neg_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
u : Set B
hs : MDiff[u] (T% s)
⊢ MDiff[u] fun (x : B) ↦ ⟨x, (-s) x⟩

Tactic:
fun x₀ hx₀ ↦ mdifferentiableWithinAt_neg_section (hs x₀ hx₀)

Premises used: mdifferentiableWithinAt_neg_section, MDifferentiableOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s : (x : B) → E x
hs : MDiff (T% s)
⊢ MDiff fun (x : B) ↦ ⟨x, (-s) x⟩

Tactic:
fun x₀ ↦ mdifferentiableAt_neg_section (hs x₀)

Premises used: mdifferentiableAt_neg_section, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
u : Set B
x₀ : B
hs : MDiffAt[u] (T% s) x₀
ht : MDiffAt[u] (T% t) x₀
rw : (MDiffAt[u] fun (x : B) ↦ ⟨x, (s + -t) x⟩) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, (s - t) x⟩) x₀

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
u : Set B
x₀ : B
hs : MDiffAt[u] (T% s) x₀
ht : MDiffAt[u] (T% t) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, (s + -t) x⟩) x₀

Tactic:
apply mdifferentiableWithinAt_add_section hs <| mdifferentiableWithinAt_neg_section ht

Premises used: mdifferentiableWithinAt_neg_section, mdifferentiableWithinAt_add_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
ht : MDiffAt (T% t) x₀
rw : (MDiffAt fun (x : B) ↦ ⟨x, (s + -t) x⟩) x₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, (s - t) x⟩) x₀

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
ht : MDiffAt (T% t) x₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, (s + -t) x⟩) x₀

Tactic:
apply mdifferentiableAt_add_section hs <| mdifferentiableAt_neg_section ht

Premises used: mdifferentiableAt_add_section, mdifferentiableAt_neg_section
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
u : Set B
hs : MDiff[u] (T% s)
ht : MDiff[u] (T% t)
⊢ MDiff[u] fun (x : B) ↦ ⟨x, (s - t) x⟩

Tactic:
fun x₀ hx₀ ↦ mdifferentiableWithinAt_sub_section (hs x₀ hx₀) (ht x₀ hx₀)

Premises used: mdifferentiableWithinAt_sub_section, MDifferentiableOn
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
s t : (x : B) → E x
hs : MDiff (T% s)
ht : MDiff (T% t)
⊢ MDiff fun (x : B) ↦ ⟨x, (s - t) x⟩

Tactic:
fun x₀ ↦ mdifferentiableAt_sub_section (hs x₀) (ht x₀)

Premises used: mdifferentiableAt_sub_section, MDifferentiable
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : TopologicalSpace B
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : (x : B) → TopologicalSpace (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_9 : VectorBundle 𝕜 F E
HB : Type u_7
inst_10 : TopologicalSpace HB
inst_11 : ChartedSpace HB B
EB : Type u_8
inst_12 : NormedAddCommGroup EB
inst_13 : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
hs : MDiffAt[u] (T% s) x₀
rw :
  ∀ (hs : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀),
    (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, (f • s) x⟩) x₀

Tactic:
rw [mdifferentiableWithinAt_section] at hs ⊢

Premises used: mdifferentiableWithinAt_section