Module: Mathlib.Geometry.Manifold.VectorBundle.Hom

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
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
EM : Type u_10
inst✝¹² : NormedAddCommGroup EM
inst✝¹¹ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹⁰ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace HM M
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✝³ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝² : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
inst✝¹ : ContMDiffVectorBundle n F₁ E₁ IB
inst✝ : ContMDiffVectorBundle n F₂ E₂ IB
⊢ ∀ e ∈ (vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂).pretrivializationAtlas,
    ∀ e' ∈ (vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂).pretrivializationAtlas,
      ∃ f,
        ContMDiffOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n f (e.baseSet ∩ e'.baseSet) ∧
          ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F₁ →L[𝕜] F₂), (f b) v = (↑e' ⟨b, e.symm b v⟩).2

Tactic:
rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩ _ ⟨e₁', e₂', he₁', he₂', rfl⟩

Goal state after:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
M : Type u_5
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
EM : Type u_10
inst✝¹² : NormedAddCommGroup EM
inst✝¹¹ : NormedSpace 𝕜 EM
HM : Type u_11
inst✝¹⁰ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace HM M
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✝³ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝² : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
inst✝¹ : ContMDiffVectorBundle n F₁ E₁ IB
inst✝ : ContMDiffVectorBundle n F₂ E₂ IB
e₁ : Trivialization F₁ TotalSpace.proj
e₂ : Trivialization F₂ TotalSpace.proj
he₁ : MemTrivializationAtlas e₁
he₂ : MemTrivializationAtlas e₂
e₁' : Trivialization F₁ TotalSpace.proj
e₂' : Trivialization F₂ TotalSpace.proj
he₁' : MemTrivializationAtlas e₁'
he₂' : MemTrivializationAtlas e₂'
⊢ ∃ f,
    ContMDiffOn IB 𝓘(𝕜, (F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₂) n f
        ((continuousLinearMap (RingHom.id 𝕜) e₁ e₂).baseSet ∩ (continuousLinearMap (RingHom.id 𝕜) e₁' e₂').baseSet) ∧
      ∀ b ∈ (continuousLinearMap (RingHom.id 𝕜) e₁ e₂).baseSet ∩ (continuousLinearMap (RingHom.id 𝕜) e₁' e₂').baseSet,
        ∀ (v : F₁ →L[𝕜] F₂),
          (f b) v =
            (↑(continuousLinearMap (RingHom.id 𝕜) e₁' e₂') ⟨b, (continuousLinearMap (RingHom.id 𝕜) e₁ e₂).symm b v⟩).2