-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace F₂ E₂)
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
e₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) e₂
e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
he₁' : MemTrivializationAtlas (E := E₁) e₁'
he₂' : MemTrivializationAtlas (E := E₂) e₂'
⊢ ∃ (f : B → F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂),
    ContinuousOn f
        (baseSet (F := F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
            TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
            (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂) ∩
          baseSet (F := F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
            TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
            (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁' e₂')) ∧
      ∀
        b ∈
          baseSet (F := F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
              TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦
                ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
              (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂) ∩
            baseSet (F := F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
              TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦
                ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
              (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁' e₂'),
        ∀ (v : F₁ [⋀^ι]→L[𝕜] F₂),
          Eq (α := F₁ [⋀^ι]→L[𝕜] F₂) ((f b : (a : F₁ [⋀^ι]→L[𝕜] F₂) → F₁ [⋀^ι]→L[𝕜] F₂) v : F₁ [⋀^ι]→L[𝕜] F₂)
            (((↑(continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁' e₂') :
                    (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x) → B × F₁ [⋀^ι]→L[𝕜] F₂)
                  (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) b
                    (Pretrivialization.symm (E := fun (x : B) ↦
                      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂ :
                        Pretrivialization (B := B) (F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
                          TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦
                            ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                          (TotalSpace.proj (E := fun (x : B) ↦
                            ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)))
                      b v))).2 :
              F₁ [⋀^ι]→L[𝕜] F₂)

Tactic:
exact ⟨continuousAlternatingMapCoordChange 𝕜 ι e₁ e₁' e₂ e₂',
      continuousOn_continuousAlternatingMapCoordChange,
      continuousAlternatingMapCoordChange_apply⟩