Module: Mathlib.Geometry.Manifold.VectorBundle.Hom

Goal state before:
pp: case refine_1
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝²⁷ : NontriviallyNormedField 𝕜
inst✝²⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁵ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁴ : NormedAddCommGroup F₁
inst✝²³ : NormedSpace 𝕜 F₁
inst✝²² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²¹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁸ : NormedAddCommGroup F₂
inst✝¹⁷ : NormedSpace 𝕜 F₂
inst✝¹⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁵ : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : ContMDiffVectorBundle n F₁ E₁ IB
inst✝⁴ : ContMDiffVectorBundle n F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
h₁ : ContMDiffOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ : ContMDiffOn IB 𝓘(𝕜, F₂ →L[𝕜] F₂) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet

pp: case refine_2
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝²⁷ : NontriviallyNormedField 𝕜
inst✝²⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁵ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁴ : NormedAddCommGroup F₁
inst✝²³ : NormedSpace 𝕜 F₁
inst✝²² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²¹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁸ : NormedAddCommGroup F₂
inst✝¹⁷ : NormedSpace 𝕜 F₂
inst✝¹⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁵ : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : ContMDiffVectorBundle n F₁ E₁ IB
inst✝⁴ : ContMDiffVectorBundle n F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
h₁ : ContMDiffOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ : ContMDiffOn IB 𝓘(𝕜, F₂ →L[𝕜] F₂) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet

Tactic:
<;>

Goal state after:
case refine_1
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝²⁷ : NontriviallyNormedField 𝕜
inst✝²⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁵ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁴ : NormedAddCommGroup F₁
inst✝²³ : NormedSpace 𝕜 F₁
inst✝²² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²¹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁸ : NormedAddCommGroup F₂
inst✝¹⁷ : NormedSpace 𝕜 F₂
inst✝¹⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁵ : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : ContMDiffVectorBundle n F₁ E₁ IB
inst✝⁴ : ContMDiffVectorBundle n F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
h₁ : ContMDiffOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ : ContMDiffOn IB 𝓘(𝕜, F₂ →L[𝕜] F₂) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet

case refine_2
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
n : WithTop ℕ∞
E₁ : B → Type u_6
E₂ : B → Type u_7
inst✝²⁷ : NontriviallyNormedField 𝕜
inst✝²⁶ : (x : B) → AddCommGroup (E₁ x)
inst✝²⁵ : (x : B) → Module 𝕜 (E₁ x)
inst✝²⁴ : NormedAddCommGroup F₁
inst✝²³ : NormedSpace 𝕜 F₁
inst✝²² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝²¹ : (x : B) → TopologicalSpace (E₁ x)
inst✝²⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝¹⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁸ : NormedAddCommGroup F₂
inst✝¹⁷ : NormedSpace 𝕜 F₂
inst✝¹⁶ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝¹⁵ : (x : B) → TopologicalSpace (E₂ x)
EB : Type u_8
inst✝¹⁴ : NormedAddCommGroup EB
inst✝¹³ : NormedSpace 𝕜 EB
HB : Type u_9
inst✝¹² : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝¹¹ : TopologicalSpace B
inst✝¹⁰ : ChartedSpace HB B
inst✝⁹ : FiberBundle F₁ E₁
inst✝⁸ : VectorBundle 𝕜 F₁ E₁
inst✝⁷ : FiberBundle F₂ E₂
inst✝⁶ : VectorBundle 𝕜 F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : ContMDiffVectorBundle n F₁ E₁ IB
inst✝⁴ : ContMDiffVectorBundle n F₂ E₂ IB
inst✝³ : MemTrivializationAtlas e₁
inst✝² : MemTrivializationAtlas e₁'
inst✝¹ : MemTrivializationAtlas e₂
inst✝ : MemTrivializationAtlas e₂'
h₁ : ContMDiffOn IB 𝓘(𝕜, F₁ →L[𝕜] F₁) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)
h₂ : ContMDiffOn IB 𝓘(𝕜, F₂ →L[𝕜] F₂) n (fun b ↦ ↑(Trivialization.coordChangeL 𝕜 e₂ e₂' b)) (e₂.baseSet ∩ e₂'.baseSet)
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet