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₂
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : VectorBundle 𝕜 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₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) 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₂))
he₁' : MemTrivializationAtlas (E := E₁) e₁'
he₂' : MemTrivializationAtlas (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
refine_3 :
  ∀ (x : F₁ × F₂),
    Eq (α := F₁ × F₂)
      (((fun (b : B) ↦
                ((↑(coordChangeL 𝕜 (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x)) (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂)
                        (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') b) :
                    F₁ × F₂ →L[𝕜] F₁ × F₂) :
                  F₁ × F₂ →L[𝕜] F₁ × F₂))
              b :
            (a : F₁ × F₂) → F₁ × F₂)
          x :
        F₁ × F₂)
      (((fun (x : B) ↦
                (ContinuousLinearMap.prodMap (↑(coordChangeL 𝕜 (E := E₁) e₁ e₁' x) : F₁ →L[𝕜] F₁)
                    (↑(coordChangeL 𝕜 (E := E₂) e₂ e₂' x) : F₂ →L[𝕜] F₂) :
                  F₁ × F₂ →L[𝕜] F₁ × F₂))
              b :
            (a : F₁ × F₂) → F₁ × F₂)
          x :
        F₁ × F₂)
⊢ Eq (α := F₁ × F₂ →L[𝕜] F₁ × F₂)
    ((fun (b : B) ↦
        ((↑(coordChangeL 𝕜 (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x)) (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂)
                (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') b) :
            F₁ × F₂ →L[𝕜] F₁ × F₂) :
          F₁ × F₂ →L[𝕜] F₁ × F₂))
      b)
    ((fun (x : B) ↦
        (ContinuousLinearMap.prodMap (↑(coordChangeL 𝕜 (E := E₁) e₁ e₁' x) : F₁ →L[𝕜] F₁)
            (↑(coordChangeL 𝕜 (E := E₂) e₂ e₂' x) : F₂ →L[𝕜] F₂) :
          F₁ × F₂ →L[𝕜] F₁ × F₂))
      b)

Tactic:
rw [ContinuousLinearMap.ext_iff]

Premises used: ContinuousLinearMap.ext_iff
-- 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₂
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : VectorBundle 𝕜 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₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) 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₂))
he₁' : MemTrivializationAtlas (E := E₁) e₁'
he₂' : MemTrivializationAtlas (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
refine_3 :
  Eq (α := F₁ × F₂)
    ((coordChangeL 𝕜 (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x)) (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂)
            (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') b :
          (a : F₁ × F₂) → F₁ × F₂)
        (v₁, v₂) :
      F₁ × F₂)
    (((coordChangeL 𝕜 (E := E₁) e₁ e₁' b : (a : F₁) → F₁) v₁, (coordChangeL 𝕜 (E := E₂) e₂ e₂' b : (a : F₂) → F₂) v₂) :
      F₁ × F₂)
⊢ Eq (α := F₁ × F₂)
    (((fun (b : B) ↦
              ((↑(coordChangeL 𝕜 (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x)) (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂)
                      (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') b) :
                  F₁ × F₂ →L[𝕜] F₁ × F₂) :
                F₁ × F₂ →L[𝕜] F₁ × F₂))
            b :
          (a : F₁ × F₂) → F₁ × F₂)
        (v₁, v₂) :
      F₁ × F₂)
    (((fun (x : B) ↦
              (ContinuousLinearMap.prodMap (↑(coordChangeL 𝕜 (E := E₁) e₁ e₁' x) : F₁ →L[𝕜] F₁)
                  (↑(coordChangeL 𝕜 (E := E₂) e₂ e₂' x) : F₂ →L[𝕜] F₂) :
                F₁ × F₂ →L[𝕜] F₁ × F₂))
            b :
          (a : F₁ × F₂) → F₁ × F₂)
        (v₁, v₂) :
      F₁ × F₂)

Tactic:
change (e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) =
        (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)

Premises used: Bundle.Trivialization.coordChangeL, Prod.mk, Bundle.Trivialization.prod, DFunLike.coe
-- 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₂
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : VectorBundle 𝕜 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₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) 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₂))
he₁' : MemTrivializationAtlas (E := E₁) e₁'
he₂' : MemTrivializationAtlas (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
refine_3 :
  ((↑(e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') : (TotalSpace (F₁ × F₂) fun (x : B) ↦ E₁ x × E₂ x) → B × F₁ × F₂)
        ((↑(e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).symm : B × F₁ × F₂ → TotalSpace (F₁ × F₂) fun (x : B) ↦ E₁ x × E₂ x)
          (b, v₁, v₂))).2 =
    (((↑e₁' : TotalSpace F₁ E₁ → B × F₁) (TotalSpace.mk (E := E₁) b (e₁.symm (E := E₁) b v₁))).2,
      ((↑e₂' : TotalSpace F₂ E₂ → B × F₂) (TotalSpace.mk (E := E₂) b (e₂.symm (E := E₂) b v₂))).2)
refine_3₁ : b ∈ (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet
refine_3₂ : b ∈ e₂.baseSet ∩ e₂'.baseSet
refine_3₃ : b ∈ e₁.baseSet ∩ e₁'.baseSet
⊢ Eq (α := F₁ × F₂)
    ((coordChangeL 𝕜 (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x)) (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂)
            (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') b :
          (a : F₁ × F₂) → F₁ × F₂)
        (v₁, v₂) :
      F₁ × F₂)
    (((coordChangeL 𝕜 (E := E₁) e₁ e₁' b : (a : F₁) → F₁) v₁, (coordChangeL 𝕜 (E := E₂) e₂ e₂' b : (a : F₂) → F₂) v₂) :
      F₁ × F₂)

Tactic:
rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']

Premises used: Bundle.Trivialization.coordChangeL_apply, Bundle.Trivialization.coordChangeL_apply', Bundle.Trivialization.prod
-- 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₂
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : VectorBundle 𝕜 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₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) 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₂))
he₁' : MemTrivializationAtlas (E := E₁) e₁'
he₂' : MemTrivializationAtlas (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ ((↑(e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') : (TotalSpace (F₁ × F₂) fun (x : B) ↦ E₁ x × E₂ x) → B × F₁ × F₂)
        ((↑(e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).symm : B × F₁ × F₂ → TotalSpace (F₁ × F₂) fun (x : B) ↦ E₁ x × E₂ x)
          (b, v₁, v₂))).2 =
    (((↑e₁' : TotalSpace F₁ E₁ → B × F₁) (TotalSpace.mk (E := E₁) b (e₁.symm (E := E₁) b v₁))).2,
      ((↑e₂' : TotalSpace F₂ E₂ → B × F₂) (TotalSpace.mk (E := E₂) b (e₂.symm (E := E₂) b v₂))).2)

Tactic:
rfl

Premises used: Bundle.Trivialization.symm, Set.Mem, dite, Bundle.Pretrivialization.symm, rfl
-- 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₂
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : VectorBundle 𝕜 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₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) 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₂))
he₁' : MemTrivializationAtlas (E := E₁) e₁'
he₂' : MemTrivializationAtlas (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ b ∈ (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet

Tactic:
hb

Premises used: Set.Mem
-- 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₂
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : VectorBundle 𝕜 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₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) 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₂))
he₁' : MemTrivializationAtlas (E := E₁) e₁'
he₂' : MemTrivializationAtlas (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ b ∈ e₂.baseSet ∩ e₂'.baseSet

Tactic:
⟨hb.1.2, hb.2.2⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, And.intro
-- 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₂
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : VectorBundle 𝕜 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₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) 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₂))
he₁' : MemTrivializationAtlas (E := E₁) e₁'
he₂' : MemTrivializationAtlas (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ b ∈ e₁.baseSet ∩ e₁'.baseSet

Tactic:
⟨hb.1.1, hb.2.1⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, And.intro
-- 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₂
inst_16 : VectorBundle 𝕜 F₁ E₁
inst_17 : VectorBundle 𝕜 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₂))
he₁ : MemTrivializationAtlas (E := E₁) e₁
he₂ : MemTrivializationAtlas (E := E₂) 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₂))
he₁' : MemTrivializationAtlas (E := E₁) e₁'
he₂' : MemTrivializationAtlas (E := E₂) e₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : F₂
⊢ ((↑(e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂') : (TotalSpace (F₁ × F₂) fun (x : B) ↦ E₁ x × E₂ x) → B × F₁ × F₂)
        ((↑(e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).symm : B × F₁ × F₂ → TotalSpace (F₁ × F₂) fun (x : B) ↦ E₁ x × E₂ x)
          (b, v₁, v₂))).2 =
    (((↑e₁' : TotalSpace F₁ E₁ → B × F₁) (TotalSpace.mk (E := E₁) b (e₁.symm (E := E₁) b v₁))).2,
      ((↑e₂' : TotalSpace F₂ E₂ → B × F₂) (TotalSpace.mk (E := E₂) b (e₂.symm (E := E₂) b v₂))).2)

Tactic:
exacts [rfl, hb, ⟨hb.1.2, hb.2.2⟩, ⟨hb.1.1, hb.2.1⟩]

Premises used: rfl
-- 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
h :
  ∀ (v : Prod.{u_4, u_6} (E₁ x) (E₂ x)),
    Eq (α := F₁ × F₂)
      (((continuousLinearEquivAt 𝕜 (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x))
                (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂) x hx :
              Prod.{u_4, u_6} (E₁ x) (E₂ x) ≃L[𝕜] F₁ × F₂) :
            (a : E₁ x × E₂ x) → F₁ × F₂)
          v :
        F₁ × F₂)
      ((ContinuousLinearEquiv.prodCongr (continuousLinearEquivAt 𝕜 (E := E₁) e₁ x ⋯)
              (continuousLinearEquivAt 𝕜 (E := E₂) e₂ x ⋯) :
            (a : E₁ x × E₂ x) → F₁ × F₂)
          v :
        F₁ × F₂)
⊢ Eq (α := Prod.{u_4, u_6} (E₁ x) (E₂ x) ≃L[𝕜] F₁ × F₂)
    (continuousLinearEquivAt 𝕜 (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x))
        (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂) x hx :
      Prod.{u_4, u_6} (E₁ x) (E₂ x) ≃L[𝕜] F₁ × F₂)
    (ContinuousLinearEquiv.prodCongr (continuousLinearEquivAt 𝕜 (E := E₁) e₁ x ⋯)
        (continuousLinearEquivAt 𝕜 (E := E₂) e₂ x ⋯) :
      Prod.{u_4, u_6} (E₁ x) (E₂ x) ≃L[𝕜] F₁ × F₂)

Tactic:
ext v : 2
-- 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 : Prod.{u_4, u_6} (E₁ x) (E₂ x)
h :
  ∀ (v₁ : E₁ x) (v₂ : E₂ x),
    Eq (α := F₁ × F₂)
      (((continuousLinearEquivAt 𝕜 (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x))
                (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂) x hx :
              Prod.{u_4, u_6} (E₁ x) (E₂ x) ≃L[𝕜] F₁ × F₂) :
            (a : E₁ x × E₂ x) → F₁ × F₂)
          (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₂)
⊢ Eq (α := F₁ × F₂)
    (((continuousLinearEquivAt 𝕜 (F := F₁ × F₂) (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x))
              (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂) x hx :
            Prod.{u_4, u_6} (E₁ x) (E₂ x) ≃L[𝕜] F₁ × F₂) :
          (a : E₁ x × E₂ x) → F₁ × F₂)
        v :
      F₁ × F₂)
    ((ContinuousLinearEquiv.prodCongr (continuousLinearEquivAt 𝕜 (E := E₁) e₁ x ⋯)
            (continuousLinearEquivAt 𝕜 (E := E₂) e₂ x ⋯) :
          (a : E₁ x × E₂ x) → F₁ × F₂)
        v :
      F₁ × F₂)

Tactic:
obtain ⟨v₁, v₂⟩ := v
-- 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:
(congr_arg Prod.snd (prod_apply' 𝕜 hx.1 hx.2 v₁ v₂) :)

Premises used: setOf, Bundle.Trivialization.prod_apply', Prod.map, congr_arg, And.right, And.left, Bundle.Trivialization.prod, Prod.snd