mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : 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 F TotalSpace.proj := trivializationAt F E x₀
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ (fun b ↦ (↑e ⟨b, (f • s) b⟩).2) =ᶠ[𝓝[u] x₀] fun p ↦ f p • (↑e ⟨p, s p⟩).2

pp: case refine_2
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : 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 F TotalSpace.proj := trivializationAt F E x₀
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ (↑e ⟨x₀, (f • s) x₀⟩).2 = f x₀ • (↑e ⟨x₀, s x₀⟩).2

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : 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 F TotalSpace.proj := trivializationAt F E x₀
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ (fun b ↦ (↑e ⟨b, (f • s) b⟩).2) =ᶠ[𝓝[u] x₀] fun p ↦ f p • (↑e ⟨p, s p⟩).2
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1.hU
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : 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 F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ e.baseSet ∈ 𝓝[u] x₀

pp: case refine_1.h
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : 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 F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet, (fun b ↦ (↑e ⟨b, (f • s) b⟩).2) x = (fun p ↦ f p • (↑e ⟨p, s p⟩).2) x

Tactic:
·

Goal state after:
case refine_1.hU
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : 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 F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ e.baseSet ∈ 𝓝[u] x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1.h
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : 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 F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet, (fun b ↦ (↑e ⟨b, (f • s) b⟩).2) x = (fun p ↦ f p • (↑e ⟨p, s p⟩).2) x

Tactic:
·

Goal state after:
case refine_1.h
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : 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 F TotalSpace.proj := ⋯
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ ∀ x ∈ e.baseSet, (fun b ↦ (↑e ⟨b, (f • s) b⟩).2) x = (fun p ↦ f p • (↑e ⟨p, s p⟩).2) x
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_2
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : 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 F TotalSpace.proj := trivializationAt F E x₀
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ (↑e ⟨x₀, (f • s) x₀⟩).2 = f x₀ • (↑e ⟨x₀, s x₀⟩).2

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : 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 F TotalSpace.proj := trivializationAt F E x₀
hs : (MDiffAt[u] fun b ↦ (↑e ⟨b, s b⟩).2) x₀
⊢ (↑e ⟨x₀, (f • s) x₀⟩).2 = f x₀ • (↑e ⟨x₀, s x₀⟩).2
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst✝¹³] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
⊢ MDiff[(tsupport ψ)ᶜ] fun x ↦ ⟨x, (ψ • s) x⟩

pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst✝¹³] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
⊢ u ∪ (tsupport ψ)ᶜ = univ

Tactic:
·

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst✝¹³] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
⊢ MDiff[(tsupport ψ)ᶜ] fun x ↦ ⟨x, (ψ • s) x⟩
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst✝¹³] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
⊢ u ∪ (tsupport ψ)ᶜ = univ

Tactic:
·

Goal state after:
𝕜 : Type u_1
B : Type u_2
F : Type u_4
E : B → Type u_6
inst✝¹³ : TopologicalSpace B
inst✝¹² : TopologicalSpace (TotalSpace F E)
inst✝¹¹ : (x : B) → TopologicalSpace (E x)
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : FiberBundle F E
inst✝⁶ : (x : B) → AddCommGroup (E x)
inst✝⁵ : (x : B) → Module 𝕜 (E x)
inst✝⁴ : VectorBundle 𝕜 F E
HB : Type u_7
inst✝³ : TopologicalSpace HB
inst✝² : ChartedSpace HB B
EB : Type u_8
inst✝¹ : NormedAddCommGroup EB
inst✝ : NormedSpace 𝕜 EB
I : ModelWithCorners 𝕜 EB HB
u : Set B
s : (x : B) → E x
ψ : B → 𝕜
hψ : MDiff[u] ψ
ht : IsOpen[inst✝¹³] u
ht' : tsupport ψ ⊆ u
hs : MDiff[u] (T% s)
⊢ u ∪ (tsupport ψ)ᶜ = univ
Module: Mathlib.Topology.VectorBundle.Hom

Goal state before:
pp: case hb
𝕜₁ : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝¹³ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝⁹ : (x : B) → AddCommGroup (E₂ x)
inst✝⁸ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁶ : TopologicalSpace B
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : FiberBundle F₁ E₁
inst✝³ : (x : B) → TopologicalSpace (E₂ x)
inst✝² : FiberBundle F₂ E₂
inst✝¹ : Trivialization.IsLinear 𝕜₁ e₁
inst✝ : Trivialization.IsLinear 𝕜₂ e₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ →SL[σ] F₂
⊢ b ∈ (continuousLinearMap σ e₁ e₂).baseSet

Tactic:
·

Goal state after:
case hb
𝕜₁ : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst✝¹⁷ : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
F₁ : Type u_4
inst✝¹⁶ : NormedAddCommGroup F₁
inst✝¹⁵ : NormedSpace 𝕜₁ F₁
E₁ : B → Type u_5
inst✝¹⁴ : (x : B) → AddCommGroup (E₁ x)
inst✝¹³ : (x : B) → Module 𝕜₁ (E₁ x)
inst✝¹² : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹¹ : NormedAddCommGroup F₂
inst✝¹⁰ : NormedSpace 𝕜₂ F₂
E₂ : B → Type u_7
inst✝⁹ : (x : B) → AddCommGroup (E₂ x)
inst✝⁸ : (x : B) → Module 𝕜₂ (E₂ x)
inst✝⁷ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁶ : TopologicalSpace B
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
inst✝⁵ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁴ : FiberBundle F₁ E₁
inst✝³ : (x : B) → TopologicalSpace (E₂ x)
inst✝² : FiberBundle F₂ E₂
inst✝¹ : Trivialization.IsLinear 𝕜₁ e₁
inst✝ : Trivialization.IsLinear 𝕜₂ e₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ →SL[σ] F₂
⊢ b ∈ (continuousLinearMap σ e₁ e₂).baseSet
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → AddCommGroup (V x)
inst✝⁵ : (x : M) → TopologicalSpace (V x)
inst✝⁴ : FiberBundle F V
inst✝³ : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization F TotalSpace.proj := trivializationAt F V x₀
⊢ t.baseSet ∈ 𝓝 x₀

pp: case refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → AddCommGroup (V x)
inst✝⁵ : (x : M) → TopologicalSpace (V x)
inst✝⁴ : FiberBundle F V
inst✝³ : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization F TotalSpace.proj := trivializationAt F V x₀
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) k (fun x' ↦ ⟨x', extend F σ₀ x'⟩) t.baseSet

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → AddCommGroup (V x)
inst✝⁵ : (x : M) → TopologicalSpace (V x)
inst✝⁴ : FiberBundle F V
inst✝³ : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization F TotalSpace.proj := trivializationAt F V x₀
⊢ t.baseSet ∈ 𝓝 x₀
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → AddCommGroup (V x)
inst✝⁵ : (x : M) → TopologicalSpace (V x)
inst✝⁴ : FiberBundle F V
inst✝³ : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization F TotalSpace.proj := trivializationAt F V x₀
⊢ t.baseSet ∈ 𝓝 x₀

pp: case refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → AddCommGroup (V x)
inst✝⁵ : (x : M) → TopologicalSpace (V x)
inst✝⁴ : FiberBundle F V
inst✝³ : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization F TotalSpace.proj := trivializationAt F V x₀
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) k (fun x' ↦ ⟨x', extend F σ₀ x'⟩) t.baseSet

Tactic:
· refine t.open_baseSet.mem_nhds ?_
    exact FiberBundle.mem_baseSet_trivializationAt' x₀

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F V)
inst✝⁶ : (x : M) → AddCommGroup (V x)
inst✝⁵ : (x : M) → TopologicalSpace (V x)
inst✝⁴ : FiberBundle F V
inst✝³ : NormedSpace 𝕜 F
k : WithTop ℕ∞
inst✝² : (x : M) → Module 𝕜 (V x)
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle k F V I
x₀ : M
σ₀ : V x₀
t : Trivialization F TotalSpace.proj := trivializationAt F V x₀
⊢ ContMDiffOn I (I.prod 𝓘(𝕜, F)) k (fun x' ↦ ⟨x', extend F σ₀ x'⟩) t.baseSet
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
w : F := (↑t ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) k (fun _x ↦ w) x
⊢ ∀ y ∈ t.baseSet, (fun x_1 ↦ (↑t ⟨x_1, extend F σ₀ x_1⟩).2) y = (fun _x ↦ w) y

pp: case refine_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
w : F := (↑t ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) k (fun _x ↦ w) x
⊢ x ∈ t.baseSet

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
w : F := (↑t ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) k (fun _x ↦ w) x
⊢ ∀ y ∈ t.baseSet, (fun x_1 ↦ (↑t ⟨x_1, extend F σ₀ x_1⟩).2) y = (fun _x ↦ w) y
Module: Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
w : F := (↑t ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) k (fun _x ↦ w) x
⊢ x ∈ t.baseSet

Tactic:
·

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
V : M → Type u_6
inst✝⁴ : TopologicalSpace (TotalSpace F V)
inst✝³ : (x : M) → AddCommGroup (V x)
inst✝² : (x : M) → TopologicalSpace (V x)
inst✝¹ : FiberBundle F V
inst✝ : NormedSpace 𝕜 F
k : WithTop ℕ∞
x : M
σ₀ : V x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
w : F := (↑t ⟨x, σ₀⟩).2
this : ContMDiffAt I 𝓘(𝕜, F) k (fun _x ↦ w) x
⊢ x ∈ t.baseSet