awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ :
  Trivialization.IsLinear R (E := E) (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
h₂ :
  Trivialization.IsLinear R (E := E)
    (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he')
⊢ Eq (α := F)
    (((↑(Trivialization.coordChangeL R (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((a.coordChange (E := E) he he' b : (a : F) → F) v : F)
have h : ((↑(a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') : TotalSpace F E → B × F)
      (TotalSpace.mk (E := E) b
        ((a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).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 [a.coordChange_apply he he' hb v, ContinuousLinearEquiv.coe_coe,
        Trivialization.coordChangeL_apply]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : NontriviallyNormedField R
inst_1 : (x : B) → AddCommMonoid (E x)
inst_2 : (x : B) → Module.{u_1, u_4} R (E x)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace R F
inst_5 : TopologicalSpace B
inst_6 : (x : B) → TopologicalSpace (E x)
a : VectorPrebundle R F E
this_1 : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology (E := E)
this : FiberBundle F E := a.toFiberBundle (E := E)
e : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he : e ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
e' : Pretrivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' : e' ∈ a.toFiberPrebundle (E := E).pretrivializationAtlas (E := E)
b : B
hb : b ∈ e.baseSet ∩ e'.baseSet
v : F
h₁ :
  Trivialization.IsLinear R (E := E) (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
h₂ :
  Trivialization.IsLinear R (E := E)
    (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he')
h :
  ((↑(a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') : TotalSpace F E → B × F)
        (TotalSpace.mk (E := E) b
          ((a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).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)
    (((↑(Trivialization.coordChangeL R (E := E)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he)
                (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he') b) :
            F →L[R] F) :
          (a : F) → F)
        v :
      F)
    ((a.coordChange (E := E) he he' b : (a : F) → F) v : F)
have h₃ : b ∈
  (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).baseSet ∩
    (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he').baseSet
Tactic: rw [a.coordChange_apply he he' hb v, ContinuousLinearEquiv.coe_coe,
        Trivialization.coordChangeL_apply]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : (x : B) → AddCommMonoid (E x)
inst_1 : NormedAddCommGroup F
inst_2 : TopologicalSpace B
inst_3 : (x : B) → TopologicalSpace (E x)
𝕜₁ : Type u_5
𝕜₂ : Type u_6
inst_4 : NontriviallyNormedField 𝕜₁
inst_5 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst_6 : TopologicalSpace B'
inst_7 : NormedSpace 𝕜₁ F
inst_8 : (x : B) → Module.{u_5, u_4} 𝕜₁ (E x)
inst_9 : TopologicalSpace (TotalSpace F E)
F' : Type u_8
inst_10 : NormedAddCommGroup F'
inst_11 : NormedSpace 𝕜₂ F'
E' : B' → Type u_9
inst_12 : (x : B') → AddCommMonoid (E' x)
inst_13 : (x : B') → Module.{u_6, u_9} 𝕜₂ (E' x)
inst_14 : TopologicalSpace (TotalSpace F' E')
inst_15 : FiberBundle F E
inst_16 : VectorBundle 𝕜₁ F E
inst_17 : (x : B') → TopologicalSpace (E' x)
inst_18 : FiberBundle F' E'
inst_19 : VectorBundle 𝕜₂ F' E'
x₀ x : B
y₀ y : B'
ϕ : ContinuousLinearMap.{u_5, u_6, u_4, u_9} σ (E x) (E' y)
hx : x ∈ Trivialization.baseSet (trivializationAt F E x₀)
hy : y ∈ Trivialization.baseSet (trivializationAt F' E' y₀)
⊢ Eq (α := F →SL[σ] F') (inCoordinates F E F' E' x₀ x y₀ y ϕ)
    ((↑(Trivialization.continuousLinearEquivAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y hy) : E' y →L[𝕜₂] F') ∘SL
      ϕ ∘SL
        (↑(ContinuousLinearEquiv.symm
              (Trivialization.continuousLinearEquivAt 𝕜₁ (E := E) (trivializationAt F E x₀) x hx)) :
          F →L[𝕜₁] E x))
have h : ∀ (x_1 : F),
  Eq.{u_8 + 1} (α := F') ((inCoordinates F E F' E' x₀ x y₀ y ϕ : (a : F) → F') x_1 : F')
    (((↑(Trivialization.continuousLinearEquivAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y hy) : E' y →L[𝕜₂] F') ∘SL
            ϕ ∘SL
              (↑(ContinuousLinearEquiv.symm
                    (Trivialization.continuousLinearEquivAt 𝕜₁ (E := E) (trivializationAt F E x₀) x hx)) :
                F →L[𝕜₁] E x) :
          (a : F) → F')
        x_1 :
      F')
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
B : Type u_2
F : Type u_3
E : B → Type u_4
inst : (x : B) → AddCommMonoid (E x)
inst_1 : NormedAddCommGroup F
inst_2 : TopologicalSpace B
inst_3 : (x : B) → TopologicalSpace (E x)
𝕜₁ : Type u_5
𝕜₂ : Type u_6
inst_4 : NontriviallyNormedField 𝕜₁
inst_5 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst_6 : TopologicalSpace B'
inst_7 : NormedSpace 𝕜₁ F
inst_8 : (x : B) → Module.{u_5, u_4} 𝕜₁ (E x)
inst_9 : TopologicalSpace (TotalSpace F E)
F' : Type u_8
inst_10 : NormedAddCommGroup F'
inst_11 : NormedSpace 𝕜₂ F'
E' : B' → Type u_9
inst_12 : (x : B') → AddCommMonoid (E' x)
inst_13 : (x : B') → Module.{u_6, u_9} 𝕜₂ (E' x)
inst_14 : TopologicalSpace (TotalSpace F' E')
inst_15 : FiberBundle F E
inst_16 : VectorBundle 𝕜₁ F E
inst_17 : (x : B') → TopologicalSpace (E' x)
inst_18 : FiberBundle F' E'
inst_19 : VectorBundle 𝕜₂ F' E'
x₀ x : B
y₀ y : B'
ϕ : ContinuousLinearMap.{u_5, u_6, u_4, u_9} σ (E x) (E' y)
hx : x ∈ Trivialization.baseSet (trivializationAt F E x₀)
hy : y ∈ Trivialization.baseSet (trivializationAt F' E' y₀)
x_1 : F
⊢ Eq.{u_8 + 1} (α := F') ((inCoordinates F E F' E' x₀ x y₀ y ϕ : (a : F) → F') x_1 : F')
    (((↑(Trivialization.continuousLinearEquivAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y hy) : E' y →L[𝕜₂] F') ∘SL
            ϕ ∘SL
              (↑(ContinuousLinearEquiv.symm
                    (Trivialization.continuousLinearEquivAt 𝕜₁ (E := E) (trivializationAt F E x₀) x hx)) :
                F →L[𝕜₁] E x) :
          (a : F) → F')
        x_1 :
      F')
have h : Eq.{u_8 + 1} (α := F')
  ((Trivialization.continuousLinearMapAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y ∘SL
          ϕ ∘SL Trivialization.symmL 𝕜₁ (E := E) (trivializationAt F E x₀) x :
        (a : F) → F')
      x_1 :
    F')
  (((↑(Trivialization.continuousLinearEquivAt 𝕜₂ (E := E') (trivializationAt F' E' y₀) y hy) : E' y →L[𝕜₂] F') ∘SL
          ϕ ∘SL
            (↑(ContinuousLinearEquiv.symm
                  (Trivialization.continuousLinearEquivAt 𝕜₁ (E := E) (trivializationAt F E x₀) x hx)) :
              F →L[𝕜₁] E x) :
        (a : F) → F')
      x_1 :
    F')
Tactic: simp_rw [inCoordinates, ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe,
    Trivialization.coe_continuousLinearEquivAt_eq, Trivialization.symm_continuousLinearEquivAt_eq]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
B : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : TopologicalSpace B
𝕜₁ : Type u_5
𝕜₂ : Type u_6
inst_2 : NontriviallyNormedField 𝕜₁
inst_3 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst_4 : TopologicalSpace B'
inst_5 : NormedSpace 𝕜₁ F
F' : Type u_8
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace 𝕜₂ F'
ι : Type u_10
ι' : Type u_11
Z : VectorBundleCore 𝕜₁ B F ι
Z' : VectorBundleCore 𝕜₂ B' F' ι'
x₀ x : B
y₀ y : B'
ϕ : F →SL[σ] F'
hx : x ∈ Z.baseSet (Z.indexAt x₀)
hy : y ∈ Z'.baseSet (Z'.indexAt y₀)
⊢ inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ =
    Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y ∘SL ϕ ∘SL Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x
have simp_rw : Trivialization.continuousLinearMapAt 𝕜₂ (E := Z'.Fiber) (trivializationAt F' Z'.Fiber y₀) y ∘SL
    ϕ ∘SL Trivialization.symmL 𝕜₁ (E := Z.Fiber) (trivializationAt F Z.Fiber x₀) x =
  Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y ∘SL ϕ ∘SL Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x
Tactic: simp_rw [inCoordinates, Z'.trivializationAt_continuousLinearMapAt hy,
    Z.trivializationAt_symmL hx]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Basic (goal)
Goal:
B : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : TopologicalSpace B
𝕜₁ : Type u_5
𝕜₂ : Type u_6
inst_2 : NontriviallyNormedField 𝕜₁
inst_3 : NontriviallyNormedField 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
B' : Type u_7
inst_4 : TopologicalSpace B'
inst_5 : NormedSpace 𝕜₁ F
F' : Type u_8
inst_6 : NormedAddCommGroup F'
inst_7 : NormedSpace 𝕜₂ F'
ι : Type u_10
ι' : Type u_11
Z : VectorBundleCore 𝕜₁ B F ι
Z' : VectorBundleCore 𝕜₂ B' F' ι'
x₀ x : B
y₀ y : B'
ϕ : F →SL[σ] F'
hx : x ∈ Z.baseSet (Z.indexAt x₀)
hy : y ∈ Z'.baseSet (Z'.indexAt y₀)
simp_rw :
  Trivialization.continuousLinearMapAt 𝕜₂ (E := Z'.Fiber) (trivializationAt F' Z'.Fiber y₀) y ∘SL
      ϕ ∘SL Trivialization.symmL 𝕜₁ (E := Z.Fiber) (trivializationAt F Z.Fiber x₀) x =
    Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y ∘SL ϕ ∘SL Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x
⊢ inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ =
    Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y ∘SL ϕ ∘SL Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x
have simp_rw₁ : Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y ∘SL
    ϕ ∘SL Trivialization.symmL 𝕜₁ (E := Z.Fiber) (trivializationAt F Z.Fiber x₀) x =
  Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y ∘SL ϕ ∘SL Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x
Tactic: simp_rw [inCoordinates, Z'.trivializationAt_continuousLinearMapAt hy,
    Z.trivializationAt_symmL hx]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
b : B
⊢ Eq (α := F ≃L[𝕜] F) (Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) (trivialization B F) b)
    (ContinuousLinearEquiv.refl 𝕜 F)
have h : ∀ (v : F),
  Eq (α := F)
    ((Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) (trivialization B F) b : (a : F) → F) v : F)
    ((ContinuousLinearEquiv.refl 𝕜 F : (a : F) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
b : B
v : F
⊢ Eq (α := F)
    ((Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) (trivialization B F) b : (a : F) → F) v : F)
    ((ContinuousLinearEquiv.refl 𝕜 F : (a : F) → F) v : F)
have h : ((↑(trivialization B F) : TotalSpace F (Trivial B F) → B × F)
      ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivialization B F))) :
          B × F → TotalSpace F (Trivial B F))
        (b, v))).2 =
  (ContinuousLinearEquiv.refl 𝕜 F : (a : F) → F) v
Tactic: rw [Trivialization.coordChangeL_apply']
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
b : B
v : F
h :
  ((↑(trivialization B F) : TotalSpace F (Trivial B F) → B × F)
        ((↑(OpenPartialHomeomorph.symm (Trivialization.toOpenPartialHomeomorph (trivialization B F))) :
            B × F → TotalSpace F (Trivial B F))
          (b, v))).2 =
    (ContinuousLinearEquiv.refl 𝕜 F : (a : F) → F) v
⊢ Eq (α := F)
    ((Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) (trivialization B F) b : (a : F) → F) v : F)
    ((ContinuousLinearEquiv.refl 𝕜 F : (a : F) → F) v : F)
have h₁ : b ∈ Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F)
Tactic: rw [Trivialization.coordChangeL_apply']
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
e : Trivialization (B := B) F (Z := TotalSpace F (Trivial B F)) (TotalSpace.proj (E := Trivial B F))
he : MemTrivializationAtlas (E := Trivial B F) e
⊢ Trivialization.IsLinear 𝕜 (E := Trivial B F) e
have rw : Trivialization.IsLinear 𝕜 (E := Trivial B F) (trivialization B F)
Tactic: rw [eq_trivialization B F e]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
e e' : Trivialization (B := B) F (Z := TotalSpace F (Trivial B F)) (TotalSpace.proj (E := Trivial B F))
he : MemTrivializationAtlas (E := Trivial B F) e
he' : MemTrivializationAtlas (E := Trivial B F) e'
⊢ ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) e e' b) : F →L[𝕜] F)) (e.baseSet ∩ e'.baseSet)
have obtain : ∀ (he : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)),
  ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) e' b) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ e'.baseSet)
Tactic: obtain rfl := eq_trivialization B F e
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
e' : Trivialization (B := B) F (Z := TotalSpace F (Trivial B F)) (TotalSpace.proj (E := Trivial B F))
he' : MemTrivializationAtlas (E := Trivial B F) e'
he : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)
⊢ ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F)
    (fun (b : B) ↦ (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) e' b) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ e'.baseSet)
have obtain : ∀ (he' : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)),
  ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F)
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) (trivialization B F) b) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))
Tactic: obtain rfl := eq_trivialization B F e'
Cleared hypotheses: e', he'
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
he he' : MemTrivializationAtlas (E := Trivial B F) (trivialization B F)
⊢ ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F)
    (fun (b : B) ↦
      (↑(Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) (trivialization B F) b) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))
have simp : ContinuousOn.{u_2, u_3} (Y := F →L[𝕜] F) (fun (b : B) ↦ (↑(ContinuousLinearEquiv.refl 𝕜 F) : F →L[𝕜] F))
  (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))
Tactic: simp only [trivialization.coordChangeL]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
x : B
⊢ Eq (α := Trivial B F x →ₗ[𝕜] F)
    (Trivialization.linearMapAt 𝕜 (E := Trivial B F) (trivialization B F) x : Trivial B F x →ₗ[𝕜] F)
    (LinearMap.id : Trivial B F x →ₗ[𝕜] Trivial B F x)
have h : ∀ (v : Trivial B F x),
  Eq (α := F)
    (((Trivialization.linearMapAt 𝕜 (E := Trivial B F) (trivialization B F) x : Trivial B F x →ₗ[𝕜] F) :
          (a : Trivial B F x) → F)
        v :
      F)
    ((LinearMap.id : (a : Trivial B F x) → F) v : F)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
x : B
v : Trivial B F x
⊢ Eq (α := F)
    (((Trivialization.linearMapAt 𝕜 (E := Trivial B F) (trivialization B F) x : Trivial B F x →ₗ[𝕜] F) :
          (a : Trivial B F x) → F)
        v :
      F)
    ((LinearMap.id : (a : Trivial B F x) → F) v : F)
have h : Eq (α := F)
  ((fun (y : Trivial B F x) ↦
        ((↑(trivialization B F) : TotalSpace F (Trivial B F) → B × F) (TotalSpace.mk (E := Trivial B F) x y)).2)
      v :
    F)
  ((LinearMap.id : (a : Trivial B F x) → F) v : F)
Tactic: rw [Trivialization.coe_linearMapAt_of_mem _ (by simp)]
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
x : B
⊢ Eq (α := Trivial B F x →L[𝕜] F)
    (Trivialization.continuousLinearMapAt 𝕜 (E := Trivial B F) (trivialization B F) x : Trivial B F x →L[𝕜] F)
    (ContinuousLinearMap.id 𝕜 F : F →L[𝕜] F)
have h : ∀ (x_1 : Trivial B F x),
  Eq (α := F)
    (((Trivialization.continuousLinearMapAt 𝕜 (E := Trivial B F) (trivialization B F) x : Trivial B F x →L[𝕜] F) :
          (a : Trivial B F x) → F)
        x_1 :
      F)
    ((ContinuousLinearMap.id 𝕜 F : (a : Trivial B F x) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
x : B
⊢ Eq (α := F →ₗ[𝕜] Trivial B F x)
    (Trivialization.symmₗ 𝕜 (E := Trivial B F) (trivialization B F) x : F →ₗ[𝕜] Trivial B F x)
    (LinearMap.id : F →ₗ[𝕜] F)
have h : ∀ (x_1 : F),
  Eq (α := Trivial B F x)
    (((Trivialization.symmₗ 𝕜 (E := Trivial B F) (trivialization B F) x : F →ₗ[𝕜] Trivial B F x) :
          (a : F) → Trivial B F x)
        x_1 :
      Trivial B F x)
    ((LinearMap.id : (a : F) → Trivial B F x) x_1 : Trivial B F x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
x : B
⊢ Eq (α := F →L[𝕜] Trivial B F x)
    (Trivialization.symmL 𝕜 (E := Trivial B F) (trivialization B F) x : F →L[𝕜] Trivial B F x)
    (ContinuousLinearMap.id 𝕜 F : F →L[𝕜] F)
have h : ∀ (x_1 : F),
  Eq (α := Trivial B F x)
    (((Trivialization.symmL 𝕜 (E := Trivial B F) (trivialization B F) x : F →L[𝕜] Trivial B F x) :
          (a : F) → Trivial B F x)
        x_1 :
      Trivial B F x)
    ((ContinuousLinearMap.id 𝕜 F : (a : F) → Trivial B F x) x_1 : Trivial B F x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Constructions (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : TopologicalSpace B
x : B
⊢ Eq (α := Trivial B F x ≃L[𝕜] F)
    (Trivialization.continuousLinearEquivAt 𝕜 (E := Trivial B F) (trivialization B F) x ⋯ : Trivial B F x ≃L[𝕜] F)
    (ContinuousLinearEquiv.refl 𝕜 F : F ≃L[𝕜] F)
have h : ∀ (x_1 : Trivial B F x),
  Eq (α := F)
    (((Trivialization.continuousLinearEquivAt 𝕜 (E := Trivial B F) (trivialization B F) x sorry : Trivial B F x ≃L[𝕜] F) :
          (a : Trivial B F x) → F)
        x_1 :
      F)
    ((ContinuousLinearEquiv.refl 𝕜 F : (a : Trivial B F x) → F) x_1 : F)
Tactic: ext
-- 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
⊢ Eq (α := F₁ × F₂ →L[𝕜] 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₂)
    (ContinuousLinearMap.prodMap (↑(coordChangeL 𝕜 (E := E₁) e₁ e₁' b) : F₁ →L[𝕜] F₁)
      (↑(coordChangeL 𝕜 (E := E₂) e₂ e₂' b) : F₂ →L[𝕜] F₂))
have rw : ∀ (x : 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₂)
        x :
      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₂) x :
      F₁ × F₂)
Tactic: rw [ContinuousLinearMap.ext_iff, ContinuousLinearMap.coe_prodMap']