awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.VectorBundle.Basic
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')
⊢ b ∈
    (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he).baseSet ∩
      (a.toFiberPrebundle (E := E).trivializationOfMemPretrivializationAtlas (E := E) he').baseSet

Tactic:
hb

Premises used: Set.Mem
-- Module: Mathlib.Topology.VectorBundle.Basic
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')
⊢ ((↑(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:
exacts [rfl, hb]

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Basic
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₀)
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')
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Topology.VectorBundle.Basic
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
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
⊢ 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

Tactic:
simp_rw [inCoordinates, Z'.trivializationAt_continuousLinearMapAt hy,
    Z.trivializationAt_symmL hx]

Premises used: VectorBundleCore.trivializationAt_symmL, ContinuousLinearMap.inCoordinates, VectorBundleCore.trivializationAt_continuousLinearMapAt
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
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)
⊢ Eq (α := F ≃L[𝕜] F) (Trivialization.coordChangeL 𝕜 (E := Trivial B F) (trivialization B F) (trivialization B F) b)
    (ContinuousLinearEquiv.refl 𝕜 F)

Tactic:
ext v
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
h₁ : b ∈ Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B 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:
rw [Trivialization.coordChangeL_apply']

Premises used: Bundle.Trivialization.coordChangeL_apply'
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
⊢ ((↑(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:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
⊢ b ∈ Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F)

Tactic:
⟨mem_univ _, mem_univ _⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, Set.mem_univ
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
⊢ ((↑(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:
exacts [rfl, ⟨mem_univ _, mem_univ _⟩]

Premises used: rfl
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
rw : Trivialization.IsLinear 𝕜 (E := Trivial B F) (trivialization B F)
⊢ Trivialization.IsLinear 𝕜 (E := Trivial B F) e

Tactic:
rw [eq_trivialization B F e]

Premises used: Bundle.Trivial.eq_trivialization
-- Module: Mathlib.Topology.VectorBundle.Constructions
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) (trivialization B F)

Tactic:
infer_instance
-- Module: Mathlib.Topology.VectorBundle.Constructions
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'
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)
⊢ 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)

Tactic:
obtain rfl := eq_trivialization B F e

Premises used: Bundle.Trivial.eq_trivialization, rfl
-- Module: Mathlib.Topology.VectorBundle.Constructions
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)
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))
⊢ 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'

Premises used: Bundle.Trivial.eq_trivialization, rfl
-- Module: Mathlib.Topology.VectorBundle.Constructions
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)
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))
⊢ 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:
simp only [trivialization.coordChangeL]

Premises used: Bundle.Trivial.trivialization.coordChangeL
-- Module: Mathlib.Topology.VectorBundle.Constructions
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) ↦ (↑(ContinuousLinearEquiv.refl 𝕜 F) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))

Tactic:
continuous_const.continuousOn

Premises used: Continuous.continuousOn, continuous_const
-- Module: Mathlib.Topology.VectorBundle.Constructions
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) ↦ (↑(ContinuousLinearEquiv.refl 𝕜 F) : F →L[𝕜] F))
    (Trivialization.baseSet (trivialization B F) ∩ Trivialization.baseSet (trivialization B F))

Tactic:
exact continuous_const.continuousOn

Premises used: Continuous.continuousOn, continuous_const
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
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)
⊢ 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)

Tactic:
ext v
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
⊢ x ∈ Trivialization.baseSet (trivialization B F)

Tactic:
simp
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
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)
⊢ 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:
rw [Trivialization.coe_linearMapAt_of_mem _ (by simp)]

Premises used: Bundle.Trivialization.coe_linearMapAt_of_mem
-- Module: Mathlib.Topology.VectorBundle.Constructions
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)
    ((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:
rfl
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
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:
simp
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
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:
simp [Trivialization.coe_symmₗ, trivialization_symm_apply B F]

Premises used: Bundle.Trivialization.coe_symmₗ, Bundle.Trivial.trivialization_symm_apply
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
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:
simp [trivialization_symm_apply B F]

Premises used: Bundle.Trivial.trivialization_symm_apply
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
h :
  ∀ (x_1 : Trivial B F x),
    Eq (α := F)
      (((Trivialization.continuousLinearEquivAt 𝕜 (E := Trivial B F) (trivialization B F) x ⋯ : 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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Topology.VectorBundle.Constructions
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
x_1 : Trivial B F x
⊢ Eq (α := F)
    (((Trivialization.continuousLinearEquivAt 𝕜 (E := Trivial B F) (trivialization B F) x ⋯ : 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:
simp
-- 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
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₂)
⊢ 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₂))

Tactic:
rw [ContinuousLinearMap.ext_iff, ContinuousLinearMap.coe_prodMap']

Premises used: ContinuousLinearMap.ext_iff, ContinuousLinearMap.coe_prodMap'