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)
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_12 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_13 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_14 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_15 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
b : B
hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ e₂'.baseSet
v₁ : F₁
v₂ : F₂
𝕜₁ :
  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₂)
    (((↑(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₂) :
          (a : F₁ × F₂) → F₁ × F₂)
        (v₁, v₂) :
      F₁ × F₂)
    (Prod.map (⇑(↑(coordChangeL 𝕜 (E := E₁) e₁ e₁' b) : F₁ →L[𝕜] F₁) : (a : F₁) → F₁)
        (⇑(↑(coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂) : (a : 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)
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_12 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_13 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_14 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_15 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
b : B
hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ e₂'.baseSet
v₁ : F₁
v₂ : F₂
rw :
  ((↑(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)
hb₁ : b ∈ (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet
hb₂ : b ∈ e₂.baseSet ∩ e₂'.baseSet
hb₃ : 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)
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_12 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_13 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_14 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_15 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
b : B
hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ 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)
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_12 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_13 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_14 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_15 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
b : B
hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ 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, setOf, Set.inter
-- 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)
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_12 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_13 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_14 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_15 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
b : B
hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ 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)
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_12 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_13 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_14 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_15 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
b : B
hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ 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)
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_12 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_13 : Trivialization.IsLinear 𝕜 (E := E₁) e₁'
inst_14 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
inst_15 : Trivialization.IsLinear 𝕜 (E := E₂) e₂'
b : B
hb : (b ∈ e₁.baseSet ∧ b ∈ e₂.baseSet) ∧ b ∈ e₁'.baseSet ∧ b ∈ 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)
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_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 : Trivialization.IsLinear 𝕜 (E := E₁) e₁
inst_17 : Trivialization.IsLinear 𝕜 (E := E₂) e₂
x : B
hx₁ : x ∈ e₁.baseSet
hx₂ : x ∈ e₂.baseSet
v₁ : E₁ x
v₂ : E₂ x
⊢ (↑(e₁.prod (E₁ := E₁) (E₂ := E₂) e₂) : (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 (v₁, v₂)) =
    (x, (continuousLinearEquivAt 𝕜 (E := E₁) e₁ x hx₁ : (a : E₁ x) → F₁) v₁,
      (continuousLinearEquivAt 𝕜 (E := E₂) e₂ x hx₂ : (a : E₂ x) → F₂) v₂)

Tactic:
rfl

Premises used: Bundle.Trivialization.toFun', Bundle.Trivialization.Prod.toFun', 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₂
⊢ Trivialization.IsLinear 𝕜 (E := fun (x : B) ↦ Prod.{u_4, u_6} (E₁ x) (E₂ x)) (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂)

Tactic:
infer_instance
-- 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₂'
⊢ ContinuousOn (Y := 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₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)

Tactic:
(((continuousOn_coordChange 𝕜 e₁ e₁').mono ?_).prod_mapL 𝕜
      ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)).congr ?_

Premises used: setOf, ContinuousOn.prod_mapL, ContinuousOn.congr, ContinuousOn.mono, continuousOn_coordChange
-- 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₂'
refine_1 :
  (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet ⊆ e₁.baseSet ∩ e₁'.baseSet
refine_2 :
  (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet ⊆ e₂.baseSet ∩ e₂'.baseSet
refine_3 :
  EqOn (β := 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₂))
    (fun (x : B) ↦
      ContinuousLinearMap.prodMap (↑(coordChangeL 𝕜 (E := E₁) e₁ e₁' x) : F₁ →L[𝕜] F₁)
        (↑(coordChangeL 𝕜 (E := E₂) e₂ e₂' x) : F₂ →L[𝕜] F₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)
⊢ ContinuousOn (Y := 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₂))
    ((e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet)

Tactic:
refine (((continuousOn_coordChange 𝕜 e₁ e₁').mono ?_).prod_mapL 𝕜
      ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)).congr ?_

Premises used: ContinuousOn.prod_mapL, ContinuousOn.congr, ContinuousOn.mono, continuousOn_coordChange
-- 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₂'
refine_1 refine_1₁ refine_1₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₁.baseSet ∩ e₁'.baseSet
refine_1₃ refine_1₄ :
  ∀ ⦃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.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₂'
refine_2 refine_2₁ refine_2₂ :
  ∀ ⦃my_y : B⦄, my_y ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) → my_y ∈ e₂.baseSet ∩ e₂'.baseSet
refine_2₃ refine_2₄ :
  ∀ ⦃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