mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝¹⁸ : NontriviallyNormedField 𝕜
B₁ : Type u_3
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 B₁
inst✝¹² : TopologicalSpace (TotalSpace F₁ E₁)
inst✝¹¹ : (x : B₁) → TopologicalSpace (E₁ x)
inst✝¹⁰ : FiberBundle F₁ E₁
inst✝⁹ : VectorBundle 𝕜 F₁ E₁
B₂ : Type u_6
F₂ : Type u_7
inst✝⁸ : NormedAddCommGroup F₂
inst✝⁷ : NormedSpace 𝕜 F₂
E₂ : B₂ → Type u_8
inst✝⁶ : (x : B₂) → AddCommGroup (E₂ x)
inst✝⁵ : (x : B₂) → Module 𝕜 (E₂ x)
inst✝⁴ : TopologicalSpace B₂
inst✝³ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝² : (x : B₂) → TopologicalSpace (E₂ x)
inst✝¹ : FiberBundle F₂ E₂
inst✝ : VectorBundle 𝕜 F₂ E₂
x₀ x : B₁
y₀ y : B₂
ϕ : E₁ x [⋀^ι]→L[𝕜] E₂ y
hx : x ∈ (trivializationAt F₁ E₁ x₀).baseSet
hy : y ∈ (trivializationAt F₂ E₂ y₀).baseSet
⊢ inCoordinates F₁ F₂ x₀ x y₀ y ϕ =
    ((↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₂ E₂ y₀) y hy)).compContinuousAlternatingMap
          ϕ).compContinuousLinearMap
      ↑(Trivialization.continuousLinearEquivAt 𝕜 (trivializationAt F₁ E₁ x₀) x hx).symm

Tactic:
ext
  simp [inCoordinates, *, Function.comp_def]

Goal state after:
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:
by
    rintro ⟨x, L⟩ ⟨h₁, h₂⟩
    simp only [TotalSpace.mk_inj]
    ext v
    simp [Function.comp_def, h₁, h₂]

Goal state after: