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 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
intro :
  ContinuousOn (Y := F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
    (fun (b : B) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 F₁ F₂ F₂ ι :
            (a : F₂ →L[𝕜] F₂) → F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
          (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂))
        (ContinuousAlternatingMap.compContinuousLinearMapCLM
          (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
⊢ ContinuousOn (Y := F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
    (continuousAlternatingMapCoordChange 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
simp +unfoldPartialApp only [continuousAlternatingMapCoordChange,
    ContinuousLinearEquiv.coe_continuousAlternatingMapCongr, ContinuousLinearEquiv.symm_symm]

Premises used: ContinuousLinearEquiv.symm_symm, ContinuousLinearEquiv.coe_continuousAlternatingMapCongr, Bundle.Pretrivialization.continuousAlternatingMapCoordChange
-- 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 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
⊢ ContinuousOn (Y := F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
    (fun (b : B) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 F₁ F₂ F₂ ι :
            (a : F₂ →L[𝕜] F₂) → F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
          (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂))
        (ContinuousAlternatingMap.compContinuousLinearMapCLM
          (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
.clm_comp ?_ ?_

Premises used: ContinuousOn.clm_comp
-- 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 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
intro :
  ContinuousOn (Y := F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
    (fun (b : B) ↦
      (ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 F₁ F₂ F₂ ι :
          (a : F₂ →L[𝕜] F₂) → F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
        (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
intro₁ :
  ContinuousOn (Y := F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
    (fun (b : B) ↦
      ContinuousAlternatingMap.compContinuousLinearMapCLM
        (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
⊢ ContinuousOn (Y := F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
    (fun (b : B) ↦
      ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜)
        ((ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 F₁ F₂ F₂ ι :
            (a : F₂ →L[𝕜] F₂) → F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
          (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂))
        (ContinuousAlternatingMap.compContinuousLinearMapCLM
          (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁)))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
refine .clm_comp ?_ ?_
-- 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 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
⊢ ContinuousOn (Y := F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
    (fun (b : B) ↦
      (ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 F₁ F₂ F₂ ι :
          (a : F₂ →L[𝕜] F₂) → F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
        (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
map_continuous (ContinuousLinearMap.compContinuousAlternatingMapCLM (ι := ι) 𝕜 F₁ F₂ F₂)
      |>.comp_continuousOn ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)

Premises used: ContinuousLinearMap.compContinuousAlternatingMapCLM, Continuous.comp_continuousOn, ContinuousOn.mono, ContinuousMapClass.map_continuous, continuousOn_coordChange
-- 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 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
intro : e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
⊢ ContinuousOn (Y := F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
    (fun (b : B) ↦
      (ContinuousLinearMap.compContinuousAlternatingMapCLM 𝕜 F₁ F₂ F₂ ι :
          (a : F₂ →L[𝕜] F₂) → F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
        (↑(Trivialization.coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
refine map_continuous (ContinuousLinearMap.compContinuousAlternatingMapCLM (ι := ι) 𝕜 F₁ F₂ F₂)
      |>.comp_continuousOn ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)

Premises used: ContinuousLinearMap.compContinuousAlternatingMapCLM, Continuous.comp_continuousOn, ContinuousOn.mono, ContinuousMapClass.map_continuous, continuousOn_coordChange
-- 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 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
intro intro₁ intro₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
intro₃ intro₄ :
  ∀ ⦃my_y : B⦄,
    (my_y ∈ e₁.baseSet ∧ my_y ∈ e₂.baseSet) ∧ my_y ∈ e₁'.baseSet ∧ my_y ∈ e₂'.baseSet → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet

Tactic:
mfld_set_tac
-- 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 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
⊢ ContinuousOn (Y := F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
    (fun (b : B) ↦
      ContinuousAlternatingMap.compContinuousLinearMapCLM
        (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM.comp_continuousOn ?_

Premises used: Continuous.comp_continuousOn, ContinuousAlternatingMap.compContinuousLinearMapCLM, ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM
-- 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 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
intro :
  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 ∩ (e₁'.baseSet ∩ e₂'.baseSet))
⊢ ContinuousOn (Y := F₁ [⋀^ι]→L[𝕜] F₂ →L[𝕜] F₁ [⋀^ι]→L[𝕜] F₂)
    (fun (b : B) ↦
      ContinuousAlternatingMap.compContinuousLinearMapCLM
        (↑(Trivialization.coordChangeL 𝕜 (E := E₁) e₁' e₁ b) : F₁ →L[𝕜] F₁))
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
refine ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM.comp_continuousOn ?_

Premises used: Continuous.comp_continuousOn, ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM
-- 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 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
mfld_set_tac mfld_set_tac₁ mfld_set_tac₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
mfld_set_tac₃ mfld_set_tac₄ :
  ∀ ⦃my_y : B⦄,
    (my_y ∈ e₁.baseSet ∧ my_y ∈ e₂.baseSet) ∧ my_y ∈ e₁'.baseSet ∧ my_y ∈ e₂'.baseSet → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet

Tactic:
mfld_set_tac
-- 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 : Finite ι
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : VectorBundle 𝕜 F₂ E₂
inst_19 : MemTrivializationAtlas (E := E₁) e₁
inst_20 : MemTrivializationAtlas (E := E₁) e₁'
inst_21 : MemTrivializationAtlas (E := E₂) e₂
inst_22 : MemTrivializationAtlas (E := E₂) e₂'
val : Fintype ι
⊢ 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 ∩ (e₁'.baseSet ∩ e₂'.baseSet))

Tactic:
exact continuousOn_coordChange 𝕜 e₁' e₁ |>.mono (by mfld_set_tac)

Premises used: ContinuousOn.mono, continuousOn_coordChange
-- 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
H :
  ∀ (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)
⊢ 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)) =
    L

Tactic:
ext v