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 : B × F₁ [⋀^ι]→L[𝕜] F₂⦄,
    x ∈ (e₁.baseSet ∩ e₂.baseSet) ×ˢ univ →
      ({ proj := x.1,
              snd :=
                (Trivialization.symmL 𝕜 e₂ x.1).compContinuousAlternatingMap
                  (x.2.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 e₁ x.1)) }.proj,
          (Trivialization.continuousLinearMapAt 𝕜 e₂
                { proj := x.1,
                    snd :=
                      (Trivialization.symmL 𝕜 e₂ x.1).compContinuousAlternatingMap
                        (x.2.compContinuousLinearMap
                          (Trivialization.continuousLinearMapAt 𝕜 e₁ x.1)) }.proj).compContinuousAlternatingMap
            ({ proj := x.1,
                    snd :=
                      (Trivialization.symmL 𝕜 e₂ x.1).compContinuousAlternatingMap
                        (x.2.compContinuousLinearMap
                          (Trivialization.continuousLinearMapAt 𝕜 e₁ x.1)) }.snd.compContinuousLinearMap
              (Trivialization.symmL 𝕜 e₁
                { proj := x.1,
                    snd :=
                      (Trivialization.symmL 𝕜 e₂ x.1).compContinuousAlternatingMap
                        (x.2.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 e₁ x.1)) }.proj))) =
        x

Tactic:
rintro ⟨x, f⟩ ⟨⟨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
f : F₁ [⋀^ι]→L[𝕜] F₂
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
⊢ ({ proj := (x, f).1,
          snd :=
            (Trivialization.symmL 𝕜 e₂ (x, f).1).compContinuousAlternatingMap
              ((x, f).2.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 e₁ (x, f).1)) }.proj,
      (Trivialization.continuousLinearMapAt 𝕜 e₂
            { proj := (x, f).1,
                snd :=
                  (Trivialization.symmL 𝕜 e₂ (x, f).1).compContinuousAlternatingMap
                    ((x, f).2.compContinuousLinearMap
                      (Trivialization.continuousLinearMapAt 𝕜 e₁ (x, f).1)) }.proj).compContinuousAlternatingMap
        ({ proj := (x, f).1,
                snd :=
                  (Trivialization.symmL 𝕜 e₂ (x, f).1).compContinuousAlternatingMap
                    ((x, f).2.compContinuousLinearMap
                      (Trivialization.continuousLinearMapAt 𝕜 e₁ (x, f).1)) }.snd.compContinuousLinearMap
          (Trivialization.symmL 𝕜 e₁
            { proj := (x, f).1,
                snd :=
                  (Trivialization.symmL 𝕜 e₂ (x, f).1).compContinuousAlternatingMap
                    ((x, f).2.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 e₁ (x, f).1)) }.proj))) =
    (x, f)