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
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
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, (f • s) b⟩).2) x₀
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑(trivializationAt F E x₀) : TotalSpace F E → B × F) ⟨b, (f • 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
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
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, (f • s) b⟩).2) x₀

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

Premises used: MDifferentiableWithinAt.congr_of_eventuallyEq, MDifferentiableWithinAt.smul
-- 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₀
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, (f • s) b⟩).2)
    fun (p : B) ↦ f p • ((↑e : TotalSpace F E → B × F) ⟨p, s p⟩).2
refine_2 : ((↑e : TotalSpace F E → B × F) ⟨x₀, (f • s) x₀⟩).2 = f x₀ • ((↑e : TotalSpace F E → B × F) ⟨x₀, s x₀⟩).2
⊢ (MDiffAt[u] fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2) x₀

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

Premises used: MDifferentiableWithinAt.congr_of_eventuallyEq, MDifferentiableWithinAt.smul
-- 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₀
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, (f • s) b⟩).2) x)
      ((fun (p : B) ↦ f p • ((↑e : TotalSpace F E → B × F) ⟨p, s p⟩).2) x)
⊢ EventuallyEq.{u_2, u_4} (β := F) (𝓝[u] x₀) (fun (b : B) ↦ ((↑e : TotalSpace F E → B × F) ⟨b, (f • s) b⟩).2)
    fun (p : B) ↦ f p • ((↑e : TotalSpace F E → B × F) ⟨p, s p⟩).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
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
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
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
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
f : B → 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hf : MDiffAt[u] f x₀
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, (f • s) b⟩).2) x)
      ((fun (p : B) ↦ f p • ((↑e : TotalSpace F E → B × F) ⟨p, s p⟩).2) x)

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

Premises used: Bundle.Trivialization.linear, IsLinearMap.map_smul
-- 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₀
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, (f • s) b⟩).2) x)
      ((fun (p : B) ↦ f p • ((↑e : TotalSpace F E → B × F) ⟨p, s p⟩).2) x)

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

Premises used: Bundle.Trivialization.linear, IsLinearMap.map_smul
-- 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₀
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₀, (f • s) x₀⟩).2 = f x₀ • ((↑e : TotalSpace F E → B × F) ⟨x₀, s x₀⟩).2

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

Premises used: FiberBundle.mem_baseSet_trivializationAt', Bundle.Trivialization.linear, IsLinearMap.map_smul
-- 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
x₀ : B
hf : MDiffAt f x₀
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
f : B → 𝕜
s : (x : B) → E x
x₀ : B
hf : MDiffAt f x₀
hs : MDiffAt[univ] (T% s) x₀
⊢ (MDiffAt[univ] fun (x : B) ↦ ⟨x, (f • s) x⟩) x₀

Tactic:
.smul_section hf hs

Premises used: MDifferentiableWithinAt.smul_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
f : B → 𝕜
s : (x : B) → E x
x₀ : B
hf : MDiffAt f x₀
hs : MDiffAt[univ] (T% s) x₀
⊢ (MDiffAt[univ] fun (x : B) ↦ ⟨x, (f • s) x⟩) x₀

Tactic:
exact .smul_section hf hs
-- 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
hf : MDiff[u] f
hs : MDiff[u] (T% s)
⊢ MDiff[u] fun (x : B) ↦ ⟨x, (f • s) x⟩

Tactic:
fun x₀ hx₀ ↦ .smul_section (hf x₀ hx₀) (hs x₀ hx₀)

Premises used: MDifferentiableOn, MDifferentiableWithinAt.smul_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
f : B → 𝕜
s : (x : B) → E x
hf : MDiff f
hs : MDiff (T% s)
⊢ MDiff fun (x : B) ↦ ⟨x, (f • s) x⟩

Tactic:
fun x₀ ↦ (hf x₀).smul_section (hs x₀)

Premises used: MDifferentiableAt.smul_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
a : 𝕜
s : (x : B) → E x
u : Set B
x₀ : B
hs : MDiffAt[u] (T% s) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, (a • s) x⟩) x₀

Tactic:
.smul_section mdifferentiableWithinAt_const hs

Premises used: mdifferentiableWithinAt_const, MDifferentiableWithinAt.smul_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
a : 𝕜
s : (x : B) → E x
x₀ : B
hs : MDiffAt (T% s) x₀
⊢ (MDiffAt fun (x : B) ↦ ⟨x, (a • s) x⟩) x₀

Tactic:
.smul_section mdifferentiableAt_const hs

Premises used: MDifferentiableAt.smul_section, mdifferentiableAt_const
-- 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
a : 𝕜
s : (x : B) → E x
u : Set B
hs : MDiff[u] (T% s)
⊢ MDiff[u] fun (x : B) ↦ ⟨x, (a • s) x⟩

Tactic:
.smul_section mdifferentiableOn_const hs

Premises used: mdifferentiableOn_const, MDifferentiableOn.smul_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
a : 𝕜
s : (x : B) → E x
hs : MDiff (T% s)
⊢ MDiff fun (x : B) ↦ ⟨x, (a • s) x⟩

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

Premises used: MDifferentiable, MDifferentiableAt.smul_const_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
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
hs : ∀ (i : ι), MDiffAt[u] (T% t) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ ∅, t i x⟩) x₀

Tactic:
simpa using (contMDiffWithinAt_zeroSection 𝕜 E).mdifferentiableWithinAt one_ne_zero

Premises used: Bundle.contMDiffWithinAt_zeroSection, ContMDiffWithinAt.mdifferentiableWithinAt, one_ne_zero
-- 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
u : Set B
x₀ : B
ι : Type u_9
t : ι → (x : B) → E x
hs : ∀ (i : ι), MDiffAt[u] (T% t) x₀
i : ι
s : Finset ι
hi : i ∉ s
h : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ insert i s, t i x⟩) x₀

Tactic:
simpa [Finset.sum_insert hi] using mdifferentiableWithinAt_add_section (hs i) h

Premises used: mdifferentiableWithinAt_add_section, Finset.sum_insert
-- 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
u : Set B
x₀ : B
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
hs : ∀ (i : ι), MDiffAt[u] (T% t) x₀
empty : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ ∅, t i x⟩) x₀
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s) (h : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀),
    (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ Insert.insert i s, t i x⟩) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀

Tactic:
induction s using Finset.induction_on with
  | empty => simpa using (contMDiffWithinAt_zeroSection 𝕜 E).mdifferentiableWithinAt one_ne_zero
  | insert i s hi h =>
    simpa [Finset.sum_insert hi] using mdifferentiableWithinAt_add_section (hs i) h

Premises used: Bundle.contMDiffWithinAt_zeroSection, Insert.insert, ContMDiffWithinAt.mdifferentiableWithinAt, one_ne_zero
-- 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
u : Set B
x₀ : B
ι : Type u_9
s : Finset ι
t : ι → (x : B) → E x
hs : ∀ (i : ι), MDiffAt[u] (T% t) x₀
empty : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ ∅, t i x⟩) x₀
insert :
  ∀ (i : ι) (s : Finset ι) (hi : i ∉ s) (h : (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀),
    (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ Insert.insert i s, t i x⟩) x₀
⊢ (MDiffAt[u] fun (x : B) ↦ ⟨x, ∑ i ∈ s, t i x⟩) x₀

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simpa using (contMDiffWithinAt_zeroSection 𝕜 E).mdifferentiableWithinAt one_ne_zero
  | insert i s hi h =>
    simpa [Finset.sum_insert hi] using mdifferentiableWithinAt_add_section (hs i) h

Premises used: Bundle.contMDiffWithinAt_zeroSection, Insert.insert, ContMDiffWithinAt.mdifferentiableWithinAt, one_ne_zero