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 : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_8] a
ha' : a ⊆ e.baseSet
h : MDiff[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2
x : B
hx : x ∈ a
this : (MDiffAt fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) x
⊢ MDiffAt[a] (T% s) x

Tactic:
((e.mdifferentiableAt_section_iff _ _ (ha' hx)).mpr this).mdifferentiableWithinAt

Premises used: Iff.mpr, MDifferentiableAt.mdifferentiableWithinAt, Bundle.Trivialization.mdifferentiableAt_section_iff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
a : Set B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
ha : IsOpen[inst_8] a
ha' : a ⊆ e.baseSet
h : MDiff[a] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2
x : B
hx : x ∈ a
this : (MDiffAt fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2) x
⊢ MDiffAt[a] (T% s) x

Tactic:
exact ((e.mdifferentiableAt_section_iff _ _ (ha' hx)).mpr this).mdifferentiableWithinAt

Premises used: Iff.mpr, MDifferentiableAt.mdifferentiableWithinAt, Bundle.Trivialization.mdifferentiableAt_section_iff
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace (TotalSpace F E)
inst_4 : (x : B) → TopologicalSpace (E x)
EB : Type u_7
inst_5 : NormedAddCommGroup EB
inst_6 : NormedSpace 𝕜 EB
HB : Type u_8
inst_7 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_8 : TopologicalSpace B
inst_9 : ChartedSpace HB B
inst_10 : FiberBundle F E
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : VectorBundle 𝕜 F E
inst_14 : ContMDiffVectorBundle 1 F E IB
s : (x : B) → E x
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
inst_15 : MemTrivializationAtlas (E := E) e
⊢ MDiff[e.baseSet] (T% s) ↔ MDiff[e.baseSet] fun (x : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨x, s x⟩).2

Tactic:
e.mdifferentiableOn_section_iff e.open_baseSet subset_rfl

Premises used: Bundle.Trivialization.open_baseSet, Bundle.Trivialization.mdifferentiableOn_section_iff, subset_rfl
-- Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_12
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_13
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
F : Type u_14
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
M : Type u_15
inst_6 : TopologicalSpace M
inst_7 : ChartedSpace H M
Z : M → Type u_16
inst_8 : TopologicalSpace (TotalSpace F Z)
inst_9 : (b : M) → TopologicalSpace (Z b)
inst_10 : FiberBundle F Z
inst_11 : (b : M) → AddCommMonoid (Z b)
inst_12 : (b : M) → Module.{u_1, u_16} 𝕜 (Z b)
inst_13 : VectorBundle 𝕜 F Z
inst_14 : ContMDiffVectorBundle 1 F Z I
e : Trivialization (B := M) F (Z := TotalSpace F Z) (TotalSpace.proj (E := Z))
inst_15 : MemTrivializationAtlas (E := Z) e
⊢ OpenPartialHomeomorph.MDifferentiable (I.prod 𝓘(𝕜, F)) (I.prod 𝓘(𝕜, F)) e.toOpenPartialHomeomorph

Tactic:
⟨e.contMDiffOn.mdifferentiableOn one_ne_zero, e.contMDiffOn_symm.mdifferentiableOn one_ne_zero⟩

Premises used: Bundle.Trivialization.contMDiffOn, And.intro, OpenPartialHomeomorph.MDifferentiable, Bundle.Trivialization.contMDiffOn_symm, one_ne_zero, ContMDiffOn.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
u : Set B
x₀ : B
hs : MDiffAt[u] (T% s) x₀
ht : MDiffAt[u] (T% t) x₀
rw :
  ∀ (hs : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, s b⟩).2) x₀)
    (ht : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀),
    (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, (s + t) x⟩) x₀

Tactic:
rw [mdifferentiableWithinAt_section] at hs ht ⊢

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 t : (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₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, t 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₀)
    (ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀),
    (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (s + t) 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 t : (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₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x₀

Tactic:
(hs.add ht).congr_of_eventuallyEq ?_ ?_

Premises used: MDifferentiableWithinAt.add, MDifferentiableWithinAt.congr_of_eventuallyEq
-- 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
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₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
refine_1 :
  (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) =ᶠ[𝓝[u] x₀]
    HAdd.hAdd (α := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) fun (b : B) ↦
      ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2
refine_2 :
  ((↑e : TotalSpace F E → B × F) ⟨x₀, (s + t) x₀⟩).2 =
    HAdd.hAdd (α := B → F) (β := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
      (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x₀

Tactic:
refine (hs.add ht).congr_of_eventuallyEq ?_ ?_

Premises used: MDifferentiableWithinAt.add, MDifferentiableWithinAt.congr_of_eventuallyEq
-- 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
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₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
refine_1 : e.baseSet ∈ 𝓝[u] x₀
refine_1₁ :
  ∀ x ∈ e.baseSet,
    (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x =
      HAdd.hAdd (α := B → F) (β := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
        (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x
⊢ (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) =ᶠ[𝓝[u] x₀]
    HAdd.hAdd (α := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2) fun (b : B) ↦
      ((↑e : TotalSpace F E → B × F) ⟨b, t 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 t : (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₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t 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 t : (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₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t 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 t : (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₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet,
    (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x =
      HAdd.hAdd (α := B → F) (β := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
        (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x

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

Premises used: Bundle.Trivialization.linear, IsLinearMap.map_add
-- 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
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₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet,
    (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (s + t) b⟩).2) x =
      HAdd.hAdd (α := B → F) (β := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
        (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x

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

Premises used: Bundle.Trivialization.linear, IsLinearMap.map_add
-- 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
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₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
⊢ ((↑e : TotalSpace F E → B × F) ⟨x₀, (s + t) x₀⟩).2 =
    HAdd.hAdd (α := B → F) (β := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
      (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀

Tactic:
(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.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
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₀
ht : (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀
⊢ ((↑e : TotalSpace F E → B × F) ⟨x₀, (s + t) x₀⟩).2 =
    HAdd.hAdd (α := B → F) (β := B → F) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, s b⟩).2)
      (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, t b⟩).2) x₀

Tactic:
exact (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.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[univ] (T% s) x₀

Tactic:
rw [← mdifferentiableWithinAt_univ] at hs ht ⊢

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 t : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
ht : MDiffAt (T% t) x₀
hs₁ : MDiffAt[univ] (T% s) x₀
⊢ MDiffAt[univ] (T% t) x₀

Tactic:
rw [← mdifferentiableWithinAt_univ] at hs ht ⊢

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 t : (x : B) → E x
x₀ : B
hs : MDiffAt[univ] (T% s) x₀
ht : MDiffAt[univ] (T% t) x₀
⊢ (MDiffAt[univ] fun (x : B) ↦ ⟨x, (s + t) x⟩) x₀

Tactic:
apply mdifferentiableWithinAt_add_section hs ht

Premises used: 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
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_add_section (hs x₀ hx₀) (ht x₀ hx₀)

Premises used: mdifferentiableWithinAt_add_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_add_section (hs x₀) (ht x₀)

Premises used: mdifferentiableAt_add_section, MDifferentiable