awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace F₂ E₂)
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
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₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (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) ι),
      ContinuousAlternatingMap.compContinuousLinearMap (M :=
        E₁ (p.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)))
        (ContinuousLinearMap.compContinuousAlternatingMap
          (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) ι)))
        (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.Trivialization.toFun', ContinuousAlternatingMap.compContinuousLinearMap, MultilinearMap.compLinearMap, ContinuousMultilinearMap.compContinuousLinearMap, rfl
-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace F₂ E₂)
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
x₀ : B
⊢ Eq (α :=
    Trivialization (B := B) (F₁ [⋀^ι]→L[𝕜] F₂) (Z :=
      TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (TotalSpace.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)))
    (trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂) (fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      x₀)
    (Trivialization.continuousAlternatingMap 𝕜 ι (E₁ := E₁) (E₂ := E₂) (trivializationAt F₁ E₁ x₀)
      (trivializationAt F₂ E₂ x₀))

Tactic:
rfl

Premises used: Bundle.Trivialization.continuousAlternatingMap, VectorPrebundle.trivializationOfMemPretrivializationAtlas, Bundle.Pretrivialization.continuousAlternatingMap, rfl
-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace F₂ E₂)
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
x₀ : B
x : TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι
⊢ (↑(trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂) (fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
            x₀) :
        (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ E₁ x [⋀^ι]→L[𝕜] E₂ x) → B × F₁ [⋀^ι]→L[𝕜] F₂)
      x =
    (x.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι),
      inCoordinates F₁ (E₁ := E₁) F₂ (E₂ := E₂) x₀
        (x.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)) x₀
        (x.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
        (x.snd (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)))

Tactic:
rfl

Premises used: Bundle.Trivialization.toFun', ContinuousAlternatingMap.compContinuousLinearMap, MultilinearMap.compLinearMap, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousAlternatingMap.inCoordinates, rfl
-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace F₂ E₂)
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
x₀ : B
⊢ Eq (α :=
    Set (TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
    (PartialEquiv.source
      (OpenPartialHomeomorph.toPartialEquiv
        (Trivialization.toOpenPartialHomeomorph
          (trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂)
            (fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x₀))))
    (TotalSpace.proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) ⁻¹'
      (Trivialization.baseSet (trivializationAt F₁ E₁ x₀) ∩ Trivialization.baseSet (trivializationAt F₂ E₂ x₀)))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace F₂ E₂)
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
x₀ : B
⊢ PartialEquiv.target (α :=
      TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)
      (OpenPartialHomeomorph.toPartialEquiv
        (Trivialization.toOpenPartialHomeomorph
          (trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂)
            (fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x₀))) =
    SProd.sprod (β := Set (F₁ [⋀^ι]→L[𝕜] F₂))
      (Trivialization.baseSet (trivializationAt F₁ E₁ x₀) ∩ Trivialization.baseSet (trivializationAt F₂ E₂ x₀)) univ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace F₂ E₂)
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
x₀ : B
⊢ Trivialization.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) ι)
      (trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂)
        (fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι) x₀) =
    Trivialization.baseSet (trivializationAt F₁ E₁ x₀) ∩ Trivialization.baseSet (trivializationAt F₂ E₂ x₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace F₂ E₂)
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
X : Type u_8
inst_21 : TopologicalSpace X
s : Set X
x₀ : X
f : X → TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι
⊢ ContinuousWithinAt f s x₀ ↔
    ContinuousWithinAt.{u_8, u_3} (Y := B)
        (fun (x : X) ↦ (f x).proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
        s x₀ ∧
      ContinuousWithinAt (Y := F₁ [⋀^ι]→L[𝕜] F₂)
        (fun (x : X) ↦
          inCoordinates F₁ (E₁ := E₁) F₂ (E₂ := E₂)
            ((f x₀).proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
            ((f x).proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
            ((f x₀).proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
            ((f x).proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
            ((f x).snd (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)))
        s x₀

Tactic:
FiberBundle.continuousWithinAt_totalSpace ..

Premises used: FiberBundle.continuousWithinAt_totalSpace, ContinuousAlternatingMap.compContinuousLinearMap, MultilinearMap.compLinearMap, ContinuousLinearMap.compContinuousAlternatingMap, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousAlternatingMap.inCoordinates
-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : Fintype ι
B : Type u_3
inst_2 : TopologicalSpace B
F₁ : Type u_4
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst_5 : (x : B) → AddCommGroup (E₁ x)
inst_6 : (x : B) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_7 : TopologicalSpace (TotalSpace F₁ E₁)
inst_8 : (x : B) → TopologicalSpace (E₁ x)
inst_9 : FiberBundle F₁ E₁
inst_10 : VectorBundle 𝕜 F₁ E₁
F₂ : Type u_6
inst_11 : NormedAddCommGroup F₂
inst_12 : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst_13 : (x : B) → AddCommGroup (E₂ x)
inst_14 : (x : B) → Module.{u_1, u_7} 𝕜 (E₂ x)
inst_15 : TopologicalSpace (TotalSpace F₂ E₂)
inst_16 : (x : B) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_20 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
X : Type u_8
inst_21 : TopologicalSpace X
x₀ : X
f : X → TotalSpace (F₁ [⋀^ι]→L[𝕜] F₂) fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι
⊢ ContinuousAt f x₀ ↔
    ContinuousAt.{u_8, u_3} (Y := B)
        (fun (x : X) ↦ (f x).proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
        x₀ ∧
      ContinuousAt (Y := F₁ [⋀^ι]→L[𝕜] F₂)
        (fun (x : X) ↦
          inCoordinates F₁ (E₁ := E₁) F₂ (E₂ := E₂)
            ((f x₀).proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
            ((f x).proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
            ((f x₀).proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
            ((f x).proj (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι))
            ((f x).snd (E := fun (x : B) ↦ ContinuousAlternatingMap.{u_1, u_5, u_7, u_2} 𝕜 (E₁ x) (E₂ x) ι)))
        x₀

Tactic:
FiberBundle.continuousAt_totalSpace ..

Premises used: FiberBundle.continuousAt_totalSpace, ContinuousAlternatingMap.compContinuousLinearMap, MultilinearMap.compLinearMap, ContinuousLinearMap.compContinuousAlternatingMap, ContinuousMultilinearMap.compContinuousLinearMap, ContinuousAlternatingMap.inCoordinates
-- Module: Mathlib.Topology.VectorBundle.FiniteDimensional
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : (x : B) → TopologicalSpace (E x)
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_4} R (E x)
inst_9 : VectorBundle R F E
b : B
inst_10 : FiniteDimensional R F
⊢ FiniteDimensional.{u_1, u_4} R (E b)

Tactic:
(continuousLinearEquivAt R F E b).symm.finiteDimensional

Premises used: VectorBundle.continuousLinearEquivAt, ContinuousLinearEquiv.symm, LinearEquiv.finiteDimensional, ContinuousLinearEquiv.toLinearEquiv
-- Module: Mathlib.Topology.VectorBundle.FiniteDimensional
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : TopologicalSpace B
inst_2 : TopologicalSpace (TotalSpace F E)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : (x : B) → TopologicalSpace (E x)
inst_6 : FiberBundle F E
inst_7 : (x : B) → AddCommGroup (E x)
inst_8 : (x : B) → Module.{u_1, u_4} R (E x)
inst_9 : VectorBundle R F E
b : B
⊢ Module.finrank.{u_1, u_4} R (E b) = Module.finrank R F

Tactic:
(continuousLinearEquivAt R F E b).finrank_eq

Premises used: VectorBundle.continuousLinearEquivAt, ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.finrank_eq
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
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_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
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_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : RingHomIsometric σ
inst_18 : VectorBundle 𝕜₁ F₁ E₁
inst_19 : VectorBundle 𝕜₂ F₂ E₂
inst_20 : MemTrivializationAtlas (E := E₁) e₁
inst_21 : MemTrivializationAtlas (E := E₁) e₁'
inst_22 : MemTrivializationAtlas (E := E₂) e₂
inst_23 : MemTrivializationAtlas (E := E₂) e₂'
⊢ Continuous (X := F₂ →L[𝕜₂] F₂) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) : (a : F₂ →L[𝕜₂] F₂) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)

Tactic:
have h₁ := (compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)).continuous
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
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_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
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_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : RingHomIsometric σ
inst_18 : VectorBundle 𝕜₁ F₁ E₁
inst_19 : VectorBundle 𝕜₂ F₂ E₂
inst_20 : MemTrivializationAtlas (E := E₁) e₁
inst_21 : MemTrivializationAtlas (E := E₁) e₁'
inst_22 : MemTrivializationAtlas (E := E₂) e₂
inst_23 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  Continuous (X := F₂ →L[𝕜₂] F₂) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) : (a : F₂ →L[𝕜₂] F₂) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
⊢ Continuous (X := F₁ →L[𝕜₁] F₁) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)) :
      (a : F₁ →L[𝕜₁] F₁) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)

Tactic:
have h₂ := (ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)).continuous
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
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_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
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_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : RingHomIsometric σ
inst_18 : VectorBundle 𝕜₁ F₁ E₁
inst_19 : VectorBundle 𝕜₂ F₂ E₂
inst_20 : MemTrivializationAtlas (E := E₁) e₁
inst_21 : MemTrivializationAtlas (E := E₁) e₁'
inst_22 : MemTrivializationAtlas (E := E₂) e₂
inst_23 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  Continuous (X := F₂ →L[𝕜₂] F₂) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) : (a : F₂ →L[𝕜₂] F₂) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₂ :
  Continuous (X := F₁ →L[𝕜₁] F₁) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)) :
      (a : F₁ →L[𝕜₁] F₁) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
⊢ ContinuousOn.{u_3, u_4} (Y := F₁ →L[𝕜₁] F₁)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₁ (E := E₁) e₁' e₁ b) : F₁ →L[𝕜₁] F₁)) (e₁'.baseSet ∩ e₁.baseSet)

Tactic:
have h₃ := continuousOn_coordChange 𝕜₁ e₁' e₁
-- Module: Mathlib.Topology.VectorBundle.Hom
Goal:
𝕜₁ : Type u_1
inst : NontriviallyNormedField 𝕜₁
𝕜₂ : Type u_2
inst_1 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B : Type u_3
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_2, u_7} 𝕜₂ (E₂ x)
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : TopologicalSpace B
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_13 : (x : B) → TopologicalSpace (E₁ x)
inst_14 : FiberBundle F₁ E₁
inst_15 : (x : B) → TopologicalSpace (E₂ x)
inst_16 : FiberBundle F₂ E₂
inst_17 : RingHomIsometric σ
inst_18 : VectorBundle 𝕜₁ F₁ E₁
inst_19 : VectorBundle 𝕜₂ F₂ E₂
inst_20 : MemTrivializationAtlas (E := E₁) e₁
inst_21 : MemTrivializationAtlas (E := E₁) e₁'
inst_22 : MemTrivializationAtlas (E := E₂) e₂
inst_23 : MemTrivializationAtlas (E := E₂) e₂'
h₁ :
  Continuous (X := F₂ →L[𝕜₂] F₂) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂)) : (a : F₂ →L[𝕜₂] F₂) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₂ :
  Continuous (X := F₁ →L[𝕜₁] F₁) (Y := (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
    (⇑(ContinuousLinearMap.flip (compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ)) :
      (a : F₁ →L[𝕜₁] F₁) → (F₁ →SL[σ] F₂) →L[𝕜₂] F₁ →SL[σ] F₂)
h₃ :
  ContinuousOn.{u_3, u_4} (Y := F₁ →L[𝕜₁] F₁)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₁ (E := E₁) e₁' e₁ b) : F₁ →L[𝕜₁] F₁)) (e₁'.baseSet ∩ e₁.baseSet)
⊢ ContinuousOn.{u_3, u_6} (Y := F₂ →L[𝕜₂] F₂)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜₂ (E := E₂) e₂ e₂' b) : F₂ →L[𝕜₂] F₂)) (e₂.baseSet ∩ e₂'.baseSet)

Tactic:
have h₄ := continuousOn_coordChange 𝕜₂ e₂ e₂'