awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
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) :
            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₂)
have 𝕜₁ : 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: change
    (e₁.prod e₂).coordChangeL 𝕜 (e₁'.prod e₂') b (v₁, v₂) =
      (e₁.coordChangeL 𝕜 e₁' b v₁, e₂.coordChangeL 𝕜 e₂' b v₂)
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
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₂)
have 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)
Tactic: rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
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)
⊢ 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₂)
have hb₁ : b ∈ (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet
Tactic: rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
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
⊢ 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₂)
have hb₂ : b ∈ e₂.baseSet ∩ e₂'.baseSet
Tactic: rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
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
⊢ 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₂)
have hb₃ : b ∈ e₁.baseSet ∩ e₁'.baseSet
Tactic: rw [e₁.coordChangeL_apply e₁', e₂.coordChangeL_apply e₂', (e₁.prod e₂).coordChangeL_apply']
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
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)
have refine_1 : (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet ⊆ e₁.baseSet ∩ e₁'.baseSet
Tactic: refine (((continuousOn_coordChange 𝕜 e₁ e₁').mono ?_).prod_mapL 𝕜
      ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)).congr ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
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
⊢ 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)
have refine_2 : (e₁.prod (E₁ := E₁) (E₂ := E₂) e₂).baseSet ∩ (e₁'.prod (E₁ := E₁) (E₂ := E₂) e₂').baseSet ⊆ e₂.baseSet ∩ e₂'.baseSet
Tactic: refine (((continuousOn_coordChange 𝕜 e₁ e₁').mono ?_).prod_mapL 𝕜
      ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)).congr ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
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
⊢ 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)
have 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)
Tactic: refine (((continuousOn_coordChange 𝕜 e₁ e₁').mono ?_).prod_mapL 𝕜
      ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)).congr ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
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₂'
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁.baseSet ∩ e₁'.baseSet
have refine_1 : ∀ ⦃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.Constructions (goal)
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
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₁.baseSet ∩ e₁'.baseSet
have 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
Tactic: mfld_set_tac
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
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₂'
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
have refine_2 : ∀ ⦃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.Constructions (goal)
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
⊢ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet) ⊆ e₂.baseSet ∩ e₂'.baseSet
have 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
Tactic: mfld_set_tac