-- 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₂'
x : B
L : ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι
h₁ :
  TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L) ∈
    e₁.baseSet
h₂ :
  TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L) ∈
    e₂.baseSet
simp :
  ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
      (Trivialization.symmL 𝕜 (E := E₂) e₂ x)
      (ContinuousAlternatingMap.compContinuousLinearMap.{u_1, u_4, u_5, u_6, u_2} (M := F₁)
        (ContinuousLinearMap.compContinuousAlternatingMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂ x)
          (L.compContinuousLinearMap (Trivialization.symmL 𝕜 (E := E₁) e₁ x)))
        (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁ x)) =
    L
⊢ Eq (α := TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
            ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
            (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L),
          ContinuousLinearMap.compContinuousAlternatingMap (N :=
            E₂
              (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
                  L)))
            (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂
              (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
                  L)))
            (ContinuousAlternatingMap.compContinuousLinearMap (M :=
              E₁
                (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                  ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                  (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
                    L)))
              (TotalSpace.snd (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
                  L))
              (Trivialization.symmL 𝕜 (E := E₁) e₁
                (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                  ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                  (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
                    L))))).1
      (ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
        (Trivialization.symmL 𝕜 (E := E₂) e₂
          (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
                  L),
              ContinuousLinearMap.compContinuousAlternatingMap (N :=
                E₂
                  (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                    ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      x L)))
                (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂
                  (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                    ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      x L)))
                (ContinuousAlternatingMap.compContinuousLinearMap (M :=
                  E₁
                    (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      (TotalSpace.mk (E := fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L)))
                  (TotalSpace.snd (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                    ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      x L))
                  (Trivialization.symmL 𝕜 (E := E₁) e₁
                    (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      (TotalSpace.mk (E := fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L))))).1)
        (ContinuousAlternatingMap.compContinuousLinearMap
          (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
                  L),
              ContinuousLinearMap.compContinuousAlternatingMap (N :=
                E₂
                  (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                    ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      x L)))
                (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂
                  (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                    ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      x L)))
                (ContinuousAlternatingMap.compContinuousLinearMap (M :=
                  E₁
                    (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      (TotalSpace.mk (E := fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L)))
                  (TotalSpace.snd (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                    ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      x L))
                  (Trivialization.symmL 𝕜 (E := E₁) e₁
                    (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      (TotalSpace.mk (E := fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L))))).2
          (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁
            (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                  ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                  (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x
                    L),
                ContinuousLinearMap.compContinuousAlternatingMap (N :=
                  E₂
                    (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      (TotalSpace.mk (E := fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L)))
                  (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂
                    (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      (TotalSpace.mk (E := fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L)))
                  (ContinuousAlternatingMap.compContinuousLinearMap (M :=
                    E₁
                      (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                        (TotalSpace.mk (E := fun (x : B) ↦
                          ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L)))
                    (TotalSpace.snd (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                      (TotalSpace.mk (E := fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L))
                    (Trivialization.symmL 𝕜 (E := E₁) e₁
                      (TotalSpace.proj (F := F₁ [⋀^ι]→L[𝕜] F₂) (E := fun (x : B) ↦
                        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
                        (TotalSpace.mk (E := fun (x : B) ↦
                          ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L))))).1))))
    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x L)

Tactic:
simp only [TotalSpace.mk_inj]

Premises used: Bundle.TotalSpace.mk_inj