-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
B : Type u_3
inst_1 : TopologicalSpace B
F₁ : Type u_4
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_4 : (x : B) → AddCommGroup (E₁ x)
inst_5 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst_7 : NormedAddCommGroup F₂
inst_8 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_9 : (x : B) → AddCommGroup (E₂ x)
inst_10 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₁ x)
inst_13 : FiberBundle F₁ E₁
inst_14 : (x : B) → TopologicalSpace (E₂ x)
inst_15 : FiberBundle F₂ E₂
e₁ e₁' : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (E := E₁))
e₂ e₂' : Trivialization (B := B) F₂ (Z := TotalSpace F₂ E₂) (TotalSpace.proj (E := E₂))
inst_16 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_17 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_18 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_19 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
L : F₁ [⋀^ι]→L[𝕜] F₂
H :
  ∀ (v : ι → F₁),
    Eq.{u_6 + 1} (α := F₂)
      ((((continuousAlternatingMapCoordChange 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂' b :
                  (a : F₁ [⋀^ι]→L[𝕜] F₂) → F₁ [⋀^ι]→L[𝕜] F₂)
                L :
              F₁ [⋀^ι]→L[𝕜] F₂) :
            (a : ι → F₁) → F₂)
          v :
        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 L))).2 :
            (a : ι → F₁) → F₂)
          v :
        F₂)
⊢ Eq (α := F₁ [⋀^ι]→L[𝕜] F₂)
    ((continuousAlternatingMapCoordChange 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂' b :
          (a : F₁ [⋀^ι]→L[𝕜] F₂) → F₁ [⋀^ι]→L[𝕜] F₂)
        L :
      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 L))).2 :
      F₁ [⋀^ι]→L[𝕜] F₂)

Tactic:
ext v