awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
v : ι → E₁ x
⊢ Eq.{u_7 + 1} (α := E₂ x)
    (((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)) :
            ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) :
          (a : ι → E₁ x) → E₂ x)
        v :
      E₂ x)
    ((L : (a : ι → E₁ x) → E₂ x) v : E₂ x)

Tactic:
simp [Function.comp_def, h₁, h₂]

Premises used: Function.comp_def
-- 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
f : F₁ [⋀^ι]→L[𝕜] F₂
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
H :
  ∀ (v : ι → F₁),
    Eq.{u_6 + 1} (α := F₂)
      ((ContinuousLinearMap.compContinuousAlternatingMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂ x)
              (ContinuousAlternatingMap.compContinuousLinearMap
                (ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
                  (Trivialization.symmL 𝕜 (E := E₂) e₂ x)
                  (f.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁ x)))
                (Trivialization.symmL 𝕜 (E := E₁) e₁ x)) :
            (a : ι → F₁) → F₂)
          v :
        F₂)
      ((f : (a : ι → F₁) → F₂) v : F₂)
⊢ ContinuousLinearMap.compContinuousAlternatingMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂ x)
      (ContinuousAlternatingMap.compContinuousLinearMap
        (ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
          (Trivialization.symmL 𝕜 (E := E₂) e₂ x)
          (f.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁ x)))
        (Trivialization.symmL 𝕜 (E := E₁) e₁ x)) =
    f

Tactic:
ext v
-- 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
f : F₁ [⋀^ι]→L[𝕜] F₂
h₁ : (x, f).1 ∈ e₁.baseSet
h₂ : (x, f).1 ∈ e₂.baseSet
v : ι → F₁
⊢ Eq.{u_6 + 1} (α := F₂)
    ((ContinuousLinearMap.compContinuousAlternatingMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂ x)
            (ContinuousAlternatingMap.compContinuousLinearMap
              (ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
                (Trivialization.symmL 𝕜 (E := E₂) e₂ x)
                (f.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁ x)))
              (Trivialization.symmL 𝕜 (E := E₁) e₁ x)) :
          (a : ι → F₁) → F₂)
        v :
      F₂)
    ((f : (a : ι → F₁) → F₂) v : F₂)

Tactic:
simp [Function.comp_def, h₁, h₂]

Premises used: Function.comp_def
-- 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₂'
inst_20 : ∀ (x : B), ContinuousAdd.{u_7} (E₂ x)
inst_21 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
x : B
h :
  x ∈
    baseSet (F := F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
      TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂)
L L' : ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι
x_1 : ι → F₁
⊢ Eq.{u_6 + 1} (α := 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) ι) x
                (L + L'))).2 :
          (a : ι → F₁) → F₂)
        x_1 :
      F₂)
    ((HAdd.hAdd (α := 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) ι) x
                  L)).2
            ((↑(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) ι) x
                  L')).2 :
          (a : ι → F₁) → F₂)
        x_1 :
      F₂)

Tactic:
simp [continuousAlternatingMap, Pretrivialization.toFun']

Premises used: Bundle.Pretrivialization.toFun', Bundle.Pretrivialization.continuousAlternatingMap
-- 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₂'
inst_20 : ∀ (x : B), ContinuousAdd.{u_7} (E₂ x)
inst_21 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
x : B
h :
  x ∈
    baseSet (F := F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
      TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂)
c : 𝕜
L : ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι
H :
  ∀ (x_1 : ι → F₁),
    Eq.{u_6 + 1} (α := 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) ι) x
                  (c • L))).2 :
            (a : ι → F₁) → F₂)
          x_1 :
        F₂)
      ((HSMul.hSMul (β := F₁ [⋀^ι]→L[𝕜] F₂) c
              ((↑(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) ι) x
                    L)).2 :
            (a : ι → F₁) → F₂)
          x_1 :
        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) ι) x
          (c • L))).2 =
    HSMul.hSMul (β := F₁ [⋀^ι]→L[𝕜] F₂) c
      ((↑(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) ι) x L)).2

Tactic:
ext
-- 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₂'
inst_20 : ∀ (x : B), ContinuousAdd.{u_7} (E₂ x)
inst_21 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
x : B
h :
  x ∈
    baseSet (F := F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
      TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂)
c : 𝕜
L : ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι
x_1 : ι → F₁
⊢ Eq.{u_6 + 1} (α := 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) ι) x
                (c • L))).2 :
          (a : ι → F₁) → F₂)
        x_1 :
      F₂)
    ((HSMul.hSMul (β := F₁ [⋀^ι]→L[𝕜] F₂) c
            ((↑(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) ι) x
                  L)).2 :
          (a : ι → F₁) → F₂)
        x_1 :
      F₂)

Tactic:
simp [continuousAlternatingMap, Pretrivialization.toFun']

Premises used: Bundle.Pretrivialization.toFun', Bundle.Pretrivialization.continuousAlternatingMap
-- 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₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (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₂
p : TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι
⊢ (↑(continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂) :
        (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x) → B × F₁ [⋀^ι]→L[𝕜] F₂)
      p =
    (p.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι),
      ContinuousLinearMap.compContinuousAlternatingMap (N :=
        E₂ (p.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)))
        (Trivialization.continuousLinearMapAt 𝕜 (E := E₂) e₂
          (p.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)))
        (p.snd (E := fun (x : B) ↦
              ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι).compContinuousLinearMap
          (Trivialization.symmL 𝕜 (E := E₁) e₁
            (p.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)))))

Tactic:
rfl

Premises used: Bundle.Pretrivialization.toFun', rfl
-- 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₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (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₂
p : B × F₁ [⋀^ι]→L[𝕜] F₂
⊢ Eq (α := TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
    ((↑(PartialEquiv.symm (toPartialEquiv (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂))) :
        B × F₁ [⋀^ι]→L[𝕜] F₂ → TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x)
      p)
    (TotalSpace.mk (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) p.1
      (ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
        (Trivialization.symmL 𝕜 (E := E₂) e₂ p.1)
        (p.2.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁ p.1))))

Tactic:
rfl

Premises used: rfl
-- 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₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (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₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ [⋀^ι]→L[𝕜] F₂
⊢ Eq (α := ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ b) (E₂ b) ι)
    (cast (α :=
        ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜
          (E₁
            (TotalSpace.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
              ((↑(PartialEquiv.symm (toPartialEquiv (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂))) :
                  B × F₁ [⋀^ι]→L[𝕜] F₂ → TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x)
                (b, L))))
          (E₂
            (TotalSpace.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
              ((↑(PartialEquiv.symm (toPartialEquiv (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂))) :
                  B × F₁ [⋀^ι]→L[𝕜] F₂ → TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x)
                (b, L))))
          ι)
        ⋯
        (TotalSpace.snd (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
          ((↑(PartialEquiv.symm (toPartialEquiv (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂))) :
              B × F₁ [⋀^ι]→L[𝕜] F₂ → TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x)
            (b, L))) :
      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ b) (E₂ b) ι)
    (ContinuousLinearMap.compContinuousAlternatingMap.{u_1, u_5, u_6, u_7, u_2} (N := F₂)
        (Trivialization.symmL 𝕜 (E := E₂) e₂ b)
        (L.compContinuousLinearMap (Trivialization.continuousLinearMapAt 𝕜 (E := E₁) e₁ b)) :
      ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ b) (E₂ b) ι)

Tactic:
rfl
-- 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₁ : Trivialization (B := B) F₁ (Z := TotalSpace F₁ E₁) (TotalSpace.proj (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₂
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet
L : F₁ [⋀^ι]→L[𝕜] F₂
⊢ b ∈
    baseSet (F := F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
      TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₂)

Tactic:
hb

Premises used: Set.Mem