awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.Constructions
Goal:
𝕜 : Type u_1
B : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : TopologicalSpace B
F₁ : Type u_3
inst_2 : NormedAddCommGroup F₁
inst_3 : NormedSpace 𝕜 F₁
E₁ : B → Type u_4
inst_4 : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_5
inst_5 : NormedAddCommGroup F₂
inst_6 : NormedSpace 𝕜 F₂
E₂ : B → Type u_6
inst_7 : TopologicalSpace (TotalSpace F₂ E₂)
inst_8 : (x : B) → AddCommMonoid (E₁ x)
inst_9 : (x : B) → Module.{u_1, u_4} 𝕜 (E₁ x)
inst_10 : (x : B) → AddCommMonoid (E₂ x)
inst_11 : (x : B) → Module.{u_1, u_6} 𝕜 (E₂ x)
inst_12 : (x : B) → TopologicalSpace (E₁ x)
inst_13 : (x : B) → TopologicalSpace (E₂ x)
inst_14 : FiberBundle F₁ E₁
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₂
x : B
hx : x ∈ (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet
v₁ : E₁ x
v₂ : E₂ x
⊢ Eq (α := F₁ × F₂)
    ((fun (y : Prod.{u_4, u_6} (E₁ x) (E₂ x)) ↦
          ((↑{ toFun := Prod.toFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂, invFun := Prod.invFun' (E₁ := E₁) (E₂ := E₂) e₁ e₂,
                    source :=
                      TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x)) ⁻¹' (e₁.baseSet ∩ e₂.baseSet),
                    target := SProd.sprod (β := Set (F₁ × F₂)) (e₁.baseSet ∩ e₂.baseSet) univ, map_source' := ⋯,
                    map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯,
                    continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, baseSet := e₁.baseSet ∩ e₂.baseSet,
                    open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ :
                    Trivialization (B := B) (F₁ × F₂) (Z :=
                      TotalSpace (F₁ × F₂) fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x))
                      (TotalSpace.proj (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x))) } :
                (TotalSpace (F₁ × F₂) fun (x : B) ↦ E₁ x × E₂ x) → B × F₁ × F₂)
              (TotalSpace.mk (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x)) x y)).2)
        (v₁, v₂) :
      F₁ × F₂)
    ((ContinuousLinearEquiv.prodCongr (continuousLinearEquivAt 𝕜 (E := E₁) e₁ x ⋯)
            (continuousLinearEquivAt 𝕜 (E := E₂) e₂ x ⋯) :
          (a : E₁ x × E₂ x) → F₁ × F₂)
        (v₁, v₂) :
      F₁ × F₂)

Tactic:
exact (congr_arg Prod.snd (prod_apply' 𝕜 hx.1 hx.2 v₁ v₂) :)

Premises used: Bundle.Trivialization.prod_apply', congr_arg, And.right, And.left, Prod.snd
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
⊢ Trivialization.IsLinear 𝕜 (E := (⇑f : (a : B') → B) *ᵖ E) (e.pullback (E := E) f)

Tactic:
infer_instance
-- Module: Mathlib.Topology.VectorBundle.Constructions
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'
⊢ ContinuousOn.{u_6, u_4} (Y := F →L[𝕜] 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))
    (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:
((continuousOn_coordChange 𝕜 e e').comp
      (map_continuous f).continuousOn fun b hb => hb).congr ?_

Premises used: Continuous.continuousOn, Set.Mem, setOf, Bundle.Pullback, Set.inter, ContinuousOn.comp, ContinuousOn.congr, Set.preimage, ContinuousMapClass.map_continuous, continuousOn_coordChange
-- Module: Mathlib.Topology.VectorBundle.Constructions
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'
refine :
  EqOn.{u_6, u_4} (β := F →L[𝕜] 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))
    ((fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) ∘ (⇑f : (a : B') → B))
    fun (b : B') ↦ (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b)
⊢ ContinuousOn.{u_6, u_4} (Y := F →L[𝕜] 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))
    (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:
refine ((continuousOn_coordChange 𝕜 e e').comp
      (map_continuous f).continuousOn fun b hb => hb).congr ?_

Premises used: Continuous.continuousOn, ContinuousOn.comp, ContinuousOn.congr, ContinuousMapClass.map_continuous, continuousOn_coordChange
-- Module: Mathlib.Topology.VectorBundle.Constructions
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)
h :
  ∀ (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)
⊢ Eq.{u_4 + 1} (α := F →L[𝕜] 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)
    (((fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := E) e e' b) : F →L[𝕜] F)) ∘ (⇑f : (a : B') → B)) b)

Tactic:
ext v
-- Module: Mathlib.Topology.VectorBundle.Constructions
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 :
  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)
⊢ 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)

Tactic:
change ((e.pullback f).coordChangeL 𝕜 (e'.pullback f) b) v = (e.coordChangeL 𝕜 e' (f b)) v

Premises used: Bundle.Trivialization.pullback, Bundle.Trivialization.coordChangeL, DFunLike.coe
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
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)
⊢ 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:
rw [e.coordChangeL_apply e' hb, (e.pullback f).coordChangeL_apply' _]

Premises used: Bundle.Trivialization.coordChangeL_apply, Bundle.Trivialization.pullback, Bundle.Trivialization.coordChangeL_apply'
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
⊢ ((↑(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:
rfl

Premises used: Bundle.Trivialization.symm, Set.Mem, Bundle.Pullback, Bundle.Trivialization.pullback, dite, Bundle.Pretrivialization.symm, Bundle.Pullback.lift, rfl
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
⊢ 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:
hb

Premises used: Set.Mem, setOf, Bundle.Pullback, Set.inter, Set.preimage
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
⊢ ((↑(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:
exacts [rfl, hb]

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
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₀)
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₂)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
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₀)
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:
simp [inCoordinates, *]

Premises used: ContinuousAlternatingMap.inCoordinates
-- 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₂'
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))
⊢ 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 ι

Premises used: nonempty_fintype