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)
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)
⊢ 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)
have 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₂)
Tactic: rw [ContinuousLinearMap.ext_iff]
-- 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₂'
b : B
hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)
v₁ : F₁
v₂ : 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₂)
have 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₂)
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)
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₂
⊢ 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 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)
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₂'
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)
⊢ 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 refine_3₁ : 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)
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
⊢ 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 refine_3₂ : 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₂'
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
⊢ 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 refine_3₃ : 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₂
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
⊢ 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₂)
have 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 sorry)
            (continuousLinearEquivAt 𝕜 (E := E₂) e₂ x sorry) :
          (a : E₁ x × E₂ x) → F₁ × F₂)
        v :
      F₁ × F₂)
Tactic: ext v : 2
-- 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₂
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)
⊢ 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₂)
have 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 sorry)
            (continuousLinearEquivAt 𝕜 (E := E₂) e₂ x sorry) :
          (a : E₁ x × E₂ x) → F₁ × F₂)
        (v₁, v₂) :
      F₁ × F₂)
Tactic: obtain ⟨v₁, v₂⟩ := v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_2, u_5} 𝕜 (E x)
K : Type u_7
inst_8 : FunLike K B' B
inst_9 : ContinuousMapClass K B' B
inst_10 : (x : B) → TopologicalSpace (E x)
inst_11 : FiberBundle F E
inst_12 : VectorBundle 𝕜 F E
f : K
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
⊢ 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))
have 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)
Tactic: refine ((continuousOn_coordChange 𝕜 e e').comp
      (map_continuous f).continuousOn fun b hb => hb).congr ?_
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
R : Type u_1
𝕜 : Type u_2
B : Type u_3
F : Type u_4
E : B → Type u_5
B' : Type u_6
f_1 : B' → B
inst : TopologicalSpace B'
inst_1 : TopologicalSpace (TotalSpace F E)
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → AddCommMonoid (E x)
inst_7 : (x : B) → Module.{u_2, u_5} 𝕜 (E x)
K : Type u_7
inst_8 : FunLike K B' B
inst_9 : ContinuousMapClass K B' B
inst_10 : (x : B) → TopologicalSpace (E x)
inst_11 : FiberBundle F E
inst_12 : VectorBundle 𝕜 F E
f : K
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : MemTrivializationAtlas (E := E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : MemTrivializationAtlas (E := E) e'
b : B'
hb : Membership.mem (α := B) (e.baseSet ∩ e'.baseSet) ((f : (a : B') → B) b : B)
⊢ 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)
have 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)
Tactic: ext v