awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_2, u_5} 𝕜 (E x)
K : Type u_7
inst_8 : FunLike K B' B
inst_9 : ContinuousMapClass K B' B
inst_10 : (x : B) → TopologicalSpace (E x)
inst_11 : FiberBundle F E
inst_12 : VectorBundle 𝕜 F E
f : K
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
b : B'
hb : Membership.mem (α := B) (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b : B)
v : F
⊢ Eq (α := F)
    (((fun (b : B') ↦
              ((↑(Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f)
                      (e'.pullback (E := E) f) b) :
                  F →L[𝕜] F) :
                F →L[𝕜] F))
            b :
          (a : F) → F)
        v :
      F)
    ((((fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) ∘ (⇑f : (a : B') → B)) b :
          (a : F) → F)
        v :
      F)
have h : Eq (α := F)
  ((Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f) (e'.pullback (E := E) f) b :
        (a : F) → F)
      v :
    F)
  ((Trivialization.coordChangeL 𝕜 (E := E) e e' ((f : (a : B') → B) b) : (a : F) → F) v : F)
Tactic: change ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_2, u_5} 𝕜 (E x)
K : Type u_7
inst_8 : FunLike K B' B
inst_9 : ContinuousMapClass K B' B
inst_10 : (x : B) → TopologicalSpace (E x)
inst_11 : FiberBundle F E
inst_12 : VectorBundle 𝕜 F E
f : K
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
b : B'
hb : Membership.mem (α := B) (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b : B)
v : F
⊢ Eq (α := F)
    ((Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f) (e'.pullback (E := E) f) b :
          (a : F) → F)
        v :
      F)
    ((Trivialization.coordChangeL 𝕜 (E := E) e e' ((f : (a : B') → B) b) : (a : F) → F) v : F)
have h : ((↑(e'.pullback (E := E) f) : TotalSpace F ((⇑f : (a : B') → B) *ᵖ E) → B' × F)
      ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (e.pullback (E := E) f))) :
          B' × F → TotalSpace F ((⇑f : (a : B') → B) *ᵖ E))
        (b, v))).2 =
  ((↑e' : TotalSpace F E → B × F)
      (TotalSpace.mk (E := E) ((f : (a : B') → B) b) (e.symm (E := E) ((f : (a : B') → B) b) v))).2
Tactic: rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_2, u_5} 𝕜 (E x)
K : Type u_7
inst_8 : FunLike K B' B
inst_9 : ContinuousMapClass K B' B
inst_10 : (x : B) → TopologicalSpace (E x)
inst_11 : FiberBundle F E
inst_12 : VectorBundle 𝕜 F E
f : K
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
b : B'
hb : Membership.mem (α := B) (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b : B)
v : F
h :
  ((↑(e'.pullback (E := E) f) : TotalSpace F ((⇑f : (a : B') → B) *ᵖ E) → B' × F)
        ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (e.pullback (E := E) f))) :
            B' × F → TotalSpace F ((⇑f : (a : B') → B) *ᵖ E))
          (b, v))).2 =
    ((↑e' : TotalSpace F E → B × F)
        (TotalSpace.mk (E := E) ((f : (a : B') → B) b) (e.symm (E := E) ((f : (a : B') → B) b) v))).2
⊢ Eq (α := F)
    ((Trivialization.coordChangeL 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f) (e'.pullback (E := E) f) b :
          (a : F) → F)
        v :
      F)
    ((Trivialization.coordChangeL 𝕜 (E := E) e e' ((f : (a : B') → B) b) : (a : F) → F) v : F)
have h₁ : b ∈
  Trivialization.baseSet (Z := TotalSpace.{u_6, u_4, u_5} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
      (e.pullback (E := E) f) ∩
    Trivialization.baseSet (Z := TotalSpace.{u_6, u_4, u_5} (B := B') F ((⇑f : (a : B') → B) *ᵖ E))
      (e'.pullback (E := E) f)
Tactic: rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : NontriviallyNormedField 𝕜
B₁ : Type u_3
F₁ : Type u_4
inst_1 : NormedAddCommGroup F₁
inst_2 : NormedSpace 𝕜 F₁
E₁ : B₁ → Type u_5
inst_3 : (x : B₁) → AddCommGroup (E₁ x)
inst_4 : (x : B₁) → Module.{u_1, u_5} 𝕜 (E₁ x)
inst_5 : TopologicalSpace B₁
inst_6 : TopologicalSpace (TotalSpace F₁ E₁)
inst_7 : (x : B₁) → TopologicalSpace (E₁ x)
inst_8 : FiberBundle F₁ E₁
inst_9 : VectorBundle 𝕜 F₁ E₁
B₂ : Type u_6
F₂ : Type u_7
inst_10 : NormedAddCommGroup F₂
inst_11 : NormedSpace 𝕜 F₂
E₂ : B₂ → Type u_8
inst_12 : (x : B₂) → AddCommGroup (E₂ x)
inst_13 : (x : B₂) → Module.{u_1, u_8} 𝕜 (E₂ x)
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace (TotalSpace F₂ E₂)
inst_16 : (x : B₂) → TopologicalSpace (E₂ x)
inst_17 : FiberBundle F₂ E₂
inst_18 : VectorBundle 𝕜 F₂ E₂
x₀ x : B₁
y₀ y : B₂
ϕ : ContinuousAlternatingMap.{u_1, u_5, u_8, u_2} 𝕜 (E₁ x) (E₂ y) ι
hx : x ∈ Trivialization.baseSet (trivializationAt F₁ E₁ x₀)
hy : y ∈ Trivialization.baseSet (trivializationAt F₂ E₂ y₀)
⊢ Eq (α := F₁ [⋀^ι]→L[𝕜] F₂) (inCoordinates F₁ (E₁ := E₁) F₂ (E₂ := E₂) x₀ x y₀ y ϕ)
    (compContinuousLinearMap
      (ContinuousLinearMap.compContinuousAlternatingMap
        (↑(Trivialization.continuousLinearEquivAt 𝕜 (E := E₂) (trivializationAt F₂ E₂ y₀) y hy) : E₂ y →L[𝕜] F₂) ϕ)
      (↑(ContinuousLinearEquiv.symm
            (Trivialization.continuousLinearEquivAt 𝕜 (E := E₁) (trivializationAt F₁ E₁ x₀) x hx)) :
        F₁ →L[𝕜] E₁ x))
have H : ∀ (x_1 : ι → F₁),
  Eq.{u_7 + 1} (α := F₂) ((inCoordinates F₁ (E₁ := E₁) F₂ (E₂ := E₂) x₀ x y₀ y ϕ : (a : ι → F₁) → F₂) x_1 : F₂)
    ((compContinuousLinearMap
            (ContinuousLinearMap.compContinuousAlternatingMap
              (↑(Trivialization.continuousLinearEquivAt 𝕜 (E := E₂) (trivializationAt F₂ E₂ y₀) y hy) : E₂ y →L[𝕜] F₂)
              ϕ)
            (↑(ContinuousLinearEquiv.symm
                  (Trivialization.continuousLinearEquivAt 𝕜 (E := E₁) (trivializationAt F₁ E₁ x₀) x hx)) :
              F₁ →L[𝕜] E₁ x) :
          (a : ι → F₁) → F₂)
        x_1 :
      F₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
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₂'
⊢ 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))
have intro : ∀ (val : Fintype ι),
  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: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
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₂)
    (continuousAlternatingMapCoordChange 𝕜 ι (E₁ := E₁) (E₂ := E₂) e₁ e₁' e₂ e₂')
    (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
have 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))
Tactic: simp +unfoldPartialApp only [continuousAlternatingMapCoordChange,
    ContinuousLinearEquiv.coe_continuousAlternatingMapCongr, ContinuousLinearEquiv.symm_symm]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
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))
have 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))
Tactic: refine .clm_comp ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
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))
⊢ 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))
have 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))
Tactic: refine .clm_comp ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
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))
have intro : e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
Tactic: refine map_continuous (ContinuousLinearMap.compContinuousAlternatingMapCLM (ι := ι) 𝕜 F₁ F₂ F₂)
      |>.comp_continuousOn ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
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 ι
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
have intro : ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
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
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
have 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
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
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))
have 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))
Tactic: refine ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM.comp_continuousOn ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.ContinuousAlternatingMap (goal)
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 ι
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁'.baseSet ∩ e₁.baseSet
have mfld_set_tac : ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₁'.baseSet ∩ e₁.baseSet
Tactic: mfld_set_tac