Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝¹⁹ : NontriviallyNormedField 𝕜
B : Type u_3
inst✝¹⁸ : TopologicalSpace B
F₁ : Type u_4
inst✝¹⁷ : NormedAddCommGroup F₁
inst✝¹⁶ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁵ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁴ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝¹⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
⊢ ∀ ⦃x : TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun x ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x⦄,
    x ∈ TotalSpace.proj ⁻¹' (e₁.baseSet ∩ e₂.baseSet) →
      {
          proj :=
            (x.proj,
                (Trivialization.continuousLinearMapAt 𝕜 e₂ x.proj).compContinuousAlternatingMap
                  (x.snd.compContinuousLinearMap (Trivialization.symmL 𝕜 e₁ x.proj))).1,
          snd :=
            (Trivialization.symmL 𝕜 e₂
                  (x.proj,
                      (Trivialization.continuousLinearMapAt 𝕜 e₂ x.proj).compContinuousAlternatingMap
                        (x.snd.compContinuousLinearMap
                          (Trivialization.symmL 𝕜 e₁ x.proj))).1).compContinuousAlternatingMap
              ((x.proj,
                      (Trivialization.continuousLinearMapAt 𝕜 e₂ x.proj).compContinuousAlternatingMap
                        (x.snd.compContinuousLinearMap (Trivialization.symmL 𝕜 e₁ x.proj))).2.compContinuousLinearMap
                (Trivialization.continuousLinearMapAt 𝕜 e₁
                  (x.proj,
                      (Trivialization.continuousLinearMapAt 𝕜 e₂ x.proj).compContinuousAlternatingMap
                        (x.snd.compContinuousLinearMap (Trivialization.symmL 𝕜 e₁ x.proj))).1)) } =
        x

Tactic:
rintro ⟨x, L⟩ ⟨h₁, h₂⟩

Goal state after:
𝕜 : Type u_1
ι : Type u_2
inst✝¹⁹ : NontriviallyNormedField 𝕜
B : Type u_3
inst✝¹⁸ : TopologicalSpace B
F₁ : Type u_4
inst✝¹⁷ : NormedAddCommGroup F₁
inst✝¹⁶ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁵ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁴ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹³ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹² : NormedAddCommGroup F₂
inst✝¹¹ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝¹⁰ : (x : B) → AddCommGroup (E₂ x)
inst✝⁹ : (x : B) → Module 𝕜 (E₂ x)
inst✝⁸ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁶ : FiberBundle F₁ E₁
inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁴ : FiberBundle F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝³ : Trivialization.IsLinear 𝕜 e₁
inst✝² : Trivialization.IsLinear 𝕜 e₁'
inst✝¹ : Trivialization.IsLinear 𝕜 e₂
inst✝ : Trivialization.IsLinear 𝕜 e₂'
x : B
L : E₁ x [⋀^ι]→L[𝕜] E₂ x
h₁ : { proj := x, snd := L }.proj ∈ e₁.baseSet
h₂ : { proj := x, snd := L }.proj ∈ e₂.baseSet
⊢ {
      proj :=
        ({ proj := x, snd := L }.proj,
            (Trivialization.continuousLinearMapAt 𝕜 e₂ { proj := x, snd := L }.proj).compContinuousAlternatingMap
              ({ proj := x, snd := L }.snd.compContinuousLinearMap
                (Trivialization.symmL 𝕜 e₁ { proj := x, snd := L }.proj))).1,
      snd :=
        (Trivialization.symmL 𝕜 e₂
              ({ proj := x, snd := L }.proj,
                  (Trivialization.continuousLinearMapAt 𝕜 e₂ { proj := x, snd := L }.proj).compContinuousAlternatingMap
                    ({ proj := x, snd := L }.snd.compContinuousLinearMap
                      (Trivialization.symmL 𝕜 e₁ { proj := x, snd := L }.proj))).1).compContinuousAlternatingMap
          (({ proj := x, snd := L }.proj,
                  (Trivialization.continuousLinearMapAt 𝕜 e₂ { proj := x, snd := L }.proj).compContinuousAlternatingMap
                    ({ proj := x, snd := L }.snd.compContinuousLinearMap
                      (Trivialization.symmL 𝕜 e₁ { proj := x, snd := L }.proj))).2.compContinuousLinearMap
            (Trivialization.continuousLinearMapAt 𝕜 e₁
              ({ proj := x, snd := L }.proj,
                  (Trivialization.continuousLinearMapAt 𝕜 e₂ { proj := x, snd := L }.proj).compContinuousAlternatingMap
                    ({ proj := x, snd := L }.snd.compContinuousLinearMap
                      (Trivialization.symmL 𝕜 e₁ { proj := x, snd := L }.proj))).1)) } =
    { proj := x, snd := L }