feat(Topology): generalise Trivialization.symm (leanprover-community#40903)

Change `Bundle.Trivialisation.symm` to get its junk values via `Classical.arbitrary` from a `Nonempty` instance, instead of requiring using `0` as the junk value and requiring `Zero` instances for that. This in particular allows us to generalise `FiberBundle.pullback` to bundles with nonempty fibres, which previously also required the bundle fibres to have zeroes. This is motivated by future work on principal bundles, whose fibres are always nonempty but have no preferred elements and hence no instances like `Zero` or `Inhabited`.

`Bundle.Trivialisation.symmₗ` and `Bundle.Trivialisation.symmL` use `0` as the junk value as before; so while their definition got slightly more complicated and their underlying function no longer definitionally equal to `.symm`, all statements that were true about them previously continue to be true now. In particular, I've tested this PR against the sphere eversion project and ran into minimal breakage there.

Author: peabrainiac

Mathlib/Topology/FiberBundle/Constructions.lean

@@ -301,7 +301,7 @@ theorem Pullback.continuous_totalSpaceMk [∀ x, TopologicalSpace (E x)] [FiberB
   exact (FiberBundle.totalSpaceMk_isInducing F E (f x)).eq_induced.le
 
 variable {E F}
-variable [∀ _b, Zero (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B]
+variable [∀ _b, Nonempty (E _b)] {K : Type U} [FunLike K B' B] [ContinuousMapClass K B' B]
 
 /-- A fiber bundle trivialization can be pulled back to a trivialization on the pullback bundle. -/
 @[simps]

Mathlib/Topology/FiberBundle/Trivialization.lean

@@ -223,29 +223,38 @@ theorem symm_coe_proj {x : B} {y : F} (e' : Pretrivialization F (π F E)) (h : x
     (e'.toPartialEquiv.symm (x, y)).1 = x :=
   e'.proj_symm_apply' h
 
-section Zero
+section Nonempty
 
-variable [∀ x, Zero (E x)]
+variable [∀ x, Nonempty (E x)]
 
 open Classical in
 /-- A fiberwise inverse to `e`. This is the function `F → E b` that induces a local inverse
-`B × F → TotalSpace F E` of `e` on `e.baseSet`. It is defined to be `0` outside `e.baseSet`. -/
+`B × F → TotalSpace F E` of `e` on `e.baseSet`. Outside of `e.baseSet` it takes on arbitrarily
+chosen junk values. -/
 protected noncomputable def symm (e : Pretrivialization F (π F E)) (b : B) (y : F) : E b :=
   if hb : b ∈ e.baseSet then
     cast (congr_arg E (e.proj_symm_apply' hb)) (e.toPartialEquiv.symm (b, y)).2
-  else 0
+  else Classical.arbitrary _
 
 theorem symm_apply (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) :
     e.symm b y = cast (congr_arg E (e.symm_coe_proj hb)) (e.toPartialEquiv.symm (b, y)).2 :=
   dif_pos hb
 
+@[deprecated "The junk values of `Pretrivialization.symm` were changed from `0` to
+`Classical.arbitrary` and should not be relied on; this lemma will be removed soon. Note that this
+change does not affect the linear versions `symmₗ` and `symmL`, which still retain `0` as the junk
+values." (since := "2026-06-23")]
 theorem symm_apply_of_notMem (e : Pretrivialization F (π F E)) {b : B} (hb : b ∉ e.baseSet)
-    (y : F) : e.symm b y = 0 :=
-  dif_neg hb
+    (y : F) : e.symm b y = Classical.arbitrary _ := by
+  simp [Pretrivialization.symm, hb]
 
+@[deprecated "The junk values of `Pretrivialization.symm` were changed from `0` to
+`Classical.arbitrary` and should not be relied on; this lemma will be removed soon. Note that this
+change does not affect the linear versions `symmₗ` and `symmL`, which still retain `0` as the junk
+values." (since := "2026-06-23")]
 theorem coe_symm_of_notMem (e : Pretrivialization F (π F E)) {b : B} (hb : b ∉ e.baseSet) :
-    (e.symm b : F → E b) = 0 :=
-  funext fun _ => dif_neg hb
+    e.symm b = fun _ ↦ Classical.arbitrary _ := by
+  ext; exact symm_apply_of_notMem e hb _
 
 theorem mk_symm (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) :
     TotalSpace.mk b (e.symm b y) = e.toPartialEquiv.symm (b, y) := by
@@ -266,7 +275,7 @@ theorem apply_mk_symm (e : Pretrivialization F (π F E)) {b : B} (hb : b ∈ e.b
     e ⟨b, e.symm b y⟩ = (b, y) := by
   rw [e.mk_symm hb, e.apply_symm_apply (e.mk_mem_target.mpr hb)]
 
-end Zero
+end Nonempty
 
 /-- The restriction of a pretrivialization to a subset of the base. -/
 @[simps toFun source target baseSet]
@@ -668,12 +677,13 @@ theorem symm_coe_proj {x : B} {y : F} (e : Trivialization F (π F E)) (h : x ∈
     (e.toOpenPartialHomeomorph.symm (x, y)).1 = x :=
   e.proj_symm_apply' h
 
-section Zero
+section Nonempty
 
-variable [∀ x, Zero (E x)]
+variable [∀ x, Nonempty (E x)]
 
 /-- A fiberwise inverse to `e'`. The function `F → E x` that induces a local inverse
-`B × F → TotalSpace F E` of `e'` on `e'.baseSet`. It is defined to be `0` outside `e'.baseSet`. -/
+`B × F → TotalSpace F E` of `e'` on `e'.baseSet`. It takes on junk values chosen using
+`Classical.arbitrary` outside `e'.baseSet`. -/
 protected noncomputable def symm (e : Trivialization F (π F E)) (b : B) (y : F) : E b :=
   e.toPretrivialization.symm b y
 
@@ -682,9 +692,13 @@ theorem symm_apply (e : Trivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet
       cast (congr_arg E (e.symm_coe_proj hb)) (e.toOpenPartialHomeomorph.symm (b, y)).2 :=
   dif_pos hb
 
+@[deprecated "The junk values of `Trivialization.symm` were changed from `0` to
+`Classical.arbitrary` and should not be relied on; this lemma will be removed soon. Note that this
+change does not affect the linear versions `symmₗ` and `symmL`, which still retain `0` as the junk
+values." (since := "2026-06-23")]
 theorem symm_apply_of_notMem (e : Trivialization F (π F E)) {b : B} (hb : b ∉ e.baseSet) (y : F) :
-    e.symm b y = 0 :=
-  dif_neg hb
+    e.symm b y = Classical.arbitrary _ :=
+  e.toPretrivialization.symm_apply_of_notMem hb y
 
 theorem mk_symm (e : Trivialization F (π F E)) {b : B} (hb : b ∈ e.baseSet) (y : F) :
     TotalSpace.mk b (e.symm b y) = e.toOpenPartialHomeomorph.symm (b, y) :=
@@ -715,7 +729,7 @@ theorem continuousOn_symm (e : Trivialization F (π F E)) :
   rw [← e.target_eq]
   exact e.toOpenPartialHomeomorph.continuousOn_symm
 
-end Zero
+end Nonempty
 
 /-- If `e` is a `Trivialization` of `proj : Z → B` with fiber `F` and `h` is a homeomorphism
 `F ≃ₜ F'`, then `e.trans_fiber_homeomorph h` is the trivialization of `proj` with the fiber `F'`

Mathlib/Topology/VectorBundle/Basic.lean

@@ -86,15 +86,22 @@ theorem linear [AddCommMonoid F] [Module R F] [∀ x, AddCommMonoid (E x)] [∀
 
 variable [AddCommMonoid F] [Module R F] [∀ x, AddCommMonoid (E x)] [∀ x, Module R (E x)]
 
+open Classical in
 /-- A fiberwise linear inverse to `e`. -/
-@[simps!]
 protected def symmₗ (e : Pretrivialization F (π F E)) [e.IsLinear R] (b : B) : F →ₗ[R] E b := by
-  refine IsLinearMap.mk' (e.symm b) ?_
-  by_cases hb : b ∈ e.baseSet
-  · exact (((e.linear R hb).mk' _).inverse (e.symm b) (e.symm_apply_apply_mk hb) fun v ↦
-      congr_arg Prod.snd <| e.apply_mk_symm hb v).isLinear
-  · rw [e.coe_symm_of_notMem hb]
-    exact (0 : F →ₗ[R] E b).isLinear
+  refine if hb : b ∈ e.baseSet then IsLinearMap.mk' (e.symm b) ?_ else 0
+  exact (((e.linear R hb).mk' _).inverse (e.symm b) (e.symm_apply_apply_mk hb) fun v ↦
+    congr_arg Prod.snd <| e.apply_mk_symm hb v).isLinear
+
+@[simp]
+lemma symmₗ_apply (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet)
+    (y : F) : e.symmₗ R b y = e.symm b y := by
+  simp [Pretrivialization.symmₗ, hb]
+
+@[simp]
+lemma symmₗ_apply_of_notMem (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B}
+    (hb : b ∉ e.baseSet) (y : F) : e.symmₗ R b y = 0 := by
+  simp [Pretrivialization.symmₗ, hb]
 
 /-- A pretrivialization for a vector bundle defines linear equivalences between the
 fibers and the model space. -/
@@ -197,9 +204,19 @@ variable (R) in
 protected def symmₗ (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) : F →ₗ[R] E b :=
   e.toPretrivialization.symmₗ R b
 
-theorem coe_symmₗ (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) :
-    ⇑(e.symmₗ R b) = e.symm b :=
-  rfl
+theorem coe_symmₗ (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet) :
+    ⇑(e.symmₗ R b) = e.symm b := by
+  ext y; exact e.toPretrivialization.symmₗ_apply R hb y
+
+@[simp]
+theorem symmₗ_apply (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet)
+    (y : F) : e.symmₗ R b y = e.symm b y :=
+  e.toPretrivialization.symmₗ_apply R hb y
+
+@[simp]
+theorem symmₗ_apply_of_notMem (e : Trivialization F (π F E)) [e.IsLinear R] {b : B}
+    (hb : b ∉ e.baseSet) (y : F) : e.symmₗ R b y = 0 :=
+  e.toPretrivialization.symmₗ_apply_of_notMem R hb y
 
 variable (R) in
 /-- A fiberwise linear map equal to `e` on `e.baseSet`. -/
@@ -230,17 +247,17 @@ theorem linearMapAt_def_of_notMem (e : Trivialization F (π F E)) [e.IsLinear R]
   dif_neg hb
 
 theorem symm_linearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet)
-    (y : E b) : e.symm b (e.linearMapAt R b y) = y :=
-  e.toPretrivialization.symmₗ_linearMapAt hb y
+    (y : E b) : e.symm b (e.linearMapAt R b y) = y := by
+  simp [hb]
 
 theorem symmₗ_linearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet)
     (y : E b) : e.symmₗ R b (e.linearMapAt R b y) = y :=
   e.toPretrivialization.symmₗ_linearMapAt hb y
 
 @[simp]
 theorem linearMapAt_symm (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet)
-    (y : F) : e.linearMapAt R b (e.symm b y) = y :=
-  e.toPretrivialization.linearMapAt_symmₗ hb y
+    (y : F) : e.linearMapAt R b (e.symm b y) = y := by
+  simp [hb]
 
 theorem linearMapAt_symmₗ (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet)
     (y : F) : e.linearMapAt R b (e.symmₗ R b y) = y :=
@@ -395,19 +412,28 @@ lemma continuousLinearMapAt_apply_of_mem (e : Trivialization F TotalSpace.proj)
   simp [coe_linearMapAt_of_mem e hb]
 
 /-- Backwards map of `Bundle.Trivialization.continuousLinearEquivAt`, defined everywhere. -/
-@[simps -fullyApplied apply]
 def symmL (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) : F →L[R] E b :=
   { e.symmₗ R b with
-    toFun := e.symm b -- given explicitly to help `simps`
     cont := by
       by_cases hb : b ∈ e.baseSet
       · rw [(FiberBundle.totalSpaceMk_isInducing F E b).continuous_iff]
+        refine .congr (f := TotalSpace.mk b ∘ e.symm b) ?_ (by simp [hb])
         exact e.continuousOn_symm.comp_continuous (.prodMk_right _) fun x ↦
           mk_mem_prod hb (mem_univ x)
-      · refine continuous_zero.congr fun x => (e.symm_apply_of_notMem hb x).symm }
+      · exact continuous_zero.congr fun x => (e.symmₗ_apply_of_notMem hb x).symm }
 
 variable {R}
 
+@[simp]
+theorem symmL_apply (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet)
+    (y : F) : e.symmL R b y = e.symm b y :=
+  e.toPretrivialization.symmₗ_apply R hb y
+
+@[simp]
+lemma symmL_apply_of_notMem (e : Trivialization F (π F E)) [e.IsLinear R] {b : B}
+    (hb : b ∉ e.baseSet) (y : F) : e.symmL R b y = 0 :=
+  e.toPretrivialization.symmₗ_apply_of_notMem _ hb _
+
 theorem symmL_continuousLinearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] {b : B}
     (hb : b ∈ e.baseSet) (y : E b) : e.symmL R b (e.continuousLinearMapAt R b y) = y :=
   e.symmₗ_linearMapAt hb y
@@ -427,7 +453,7 @@ def continuousLinearEquivAt (e : Trivialization F (π F E)) [e.IsLinear R] (b :
     invFun := e.symm b -- given explicitly to help `simps`
     continuous_toFun := (e.continuousOn.comp_continuous
       (FiberBundle.totalSpaceMk_isInducing F E b).continuous fun _ => e.mem_source.mpr hb).snd
-    continuous_invFun := (e.symmL R b).continuous }
+    continuous_invFun := by convert (e.symmL R b).continuous; ext; simp [hb] }
 
 theorem coe_continuousLinearEquivAt_eq (e : Trivialization F (π F E)) [e.IsLinear R] {b : B}
     (hb : b ∈ e.baseSet) :
@@ -440,12 +466,13 @@ theorem coe_continuousLinearEquivAt_eq' (e : Trivialization F (π F E)) [e.IsLin
   DFunLike.coe_injective (e.coe_linearMapAt_of_mem hb).symm
 
 theorem symm_continuousLinearEquivAt_eq (e : Trivialization F (π F E)) [e.IsLinear R] {b : B}
-    (hb : b ∈ e.baseSet) : ((e.continuousLinearEquivAt R b hb).symm : F → E b) = e.symmL R b :=
-  rfl
+    (hb : b ∈ e.baseSet) : ((e.continuousLinearEquivAt R b hb).symm : F → E b) = e.symmL R b := by
+  ext; simp [hb]
 
 theorem symm_continuousLinearEquivAt_eq' (e : Trivialization F (π F E)) [e.IsLinear R] {b : B}
-    (hb : b ∈ e.baseSet) : ((e.continuousLinearEquivAt R b hb).symm : F →L[R] E b) = e.symmL R b :=
-  rfl
+    (hb : b ∈ e.baseSet) :
+    ((e.continuousLinearEquivAt R b hb).symm : F →L[R] E b) = e.symmL R b := by
+  ext; simp [hb]
 
 @[simp]
 theorem continuousLinearEquivAt_apply' (e : Trivialization F (π F E)) [e.IsLinear R]
@@ -745,7 +772,7 @@ theorem trivializationAt_continuousLinearMapAt {b₀ b : B}
 theorem localTriv_symmL {b : B} (hb : b ∈ (Z.localTriv i).baseSet) :
     (Z.localTriv i).symmL R b = Z.coordChange i (Z.indexAt b) b := by
   ext1 v
-  rw [(Z.localTriv i).symmL_apply R, (Z.localTriv i).symm_apply]
+  rw [(Z.localTriv i).symmL_apply hb, (Z.localTriv i).symm_apply]
   exacts [rfl, hb]
 
 @[simp, mfld_simps]

Mathlib/Topology/VectorBundle/Constructions.lean

@@ -74,7 +74,7 @@ instance vectorBundle : VectorBundle 𝕜 F (Bundle.Trivial B F) where
 
 @[simp] lemma symmₗ_trivialization (x : B) :
     (trivialization B F).symmₗ 𝕜 x = LinearMap.id := by
-  ext; simp [Trivialization.coe_symmₗ, trivialization_symm_apply B F]
+  ext; simp [trivialization_symm_apply B F]
 
 @[simp] lemma symmL_trivialization (x : B) :
     (trivialization B F).symmL 𝕜 x = ContinuousLinearMap.id 𝕜 F := by

Mathlib/Topology/VectorBundle/ContinuousAlternatingMap.lean

@@ -87,7 +87,7 @@ theorem inCoordinates_eq {x₀ x : B₁} {y₀ y : B₂} {ϕ : E₁ x [⋀^ι]
         |>.compContinuousAlternatingMap ϕ |>.compContinuousLinearMap
           (((trivializationAt F₁ E₁ x₀).continuousLinearEquivAt 𝕜 x hx).symm : F₁ →L[𝕜] E₁ x)) := by
   ext
-  simp [inCoordinates, *]
+  simp [inCoordinates, *, Function.comp_def]
 
 end ContinuousAlternatingMap
 
@@ -277,7 +277,8 @@ def vectorPrebundle :
         (mem_baseSet_trivializationAt _ _ _)
     convert! (L₁.continuousAlternatingMapCongr L₂).toHomeomorph.isInducing
     ext f
-    simp [Trivialization.linearMapAt_def_of_mem _ (mem_baseSet_trivializationAt _ _ _), L₁, L₂]
+    simp [Trivialization.linearMapAt_def_of_mem _ (mem_baseSet_trivializationAt _ _ _), L₁, L₂,
+      Function.comp_def, mem_baseSet_trivializationAt]
 
 /-- Topology on the total space of the continuous `σ`-semilinear maps between two "normable" vector
 bundles over the same base. -/

Mathlib/Topology/VectorBundle/Hom.lean

@@ -154,10 +154,9 @@ theorem continuousLinearMapCoordChange_apply (b : B)
   simp_rw [continuousLinearMapCoordChange, ContinuousLinearEquiv.coe_coe,
     ContinuousLinearEquiv.arrowCongrSL_apply, continuousLinearMap_apply,
     continuousLinearMap_symm_apply' σ e₁ e₂ hb.1, comp_apply, ContinuousLinearEquiv.coe_coe,
-    ContinuousLinearEquiv.symm_symm, Trivialization.continuousLinearMapAt_apply,
-    Trivialization.symmL_apply]
-  rw [e₂.coordChangeL_apply e₂', e₁'.coordChangeL_apply e₁, e₁.coe_linearMapAt_of_mem hb.1.1,
-    e₂'.coe_linearMapAt_of_mem hb.2.2]
+    ContinuousLinearEquiv.symm_symm, Trivialization.continuousLinearMapAt_apply]
+  rw [e₂.symmL_apply hb.1.2, e₁'.symmL_apply hb.2.1, e₂.coordChangeL_apply e₂',
+    e₁'.coordChangeL_apply e₁, e₁.coe_linearMapAt_of_mem hb.1.1, e₂'.coe_linearMapAt_of_mem hb.2.2]
   exacts [⟨hb.2.1, hb.1.1⟩, ⟨hb.1.2, hb.2.2⟩]
 
 end Bundle.Pretrivialization
@@ -208,7 +207,8 @@ def Bundle.ContinuousLinearMap.vectorPrebundle :
     convert! this
     ext f
     dsimp [Pretrivialization.continuousLinearMap_apply]
-    rw [Trivialization.linearMapAt_def_of_mem _ (mem_baseSet_trivializationAt _ _ _)]
+    simp only [Trivialization.symmL_apply, mem_baseSet_trivializationAt,
+      Trivialization.linearMapAt_def_of_mem]
     rfl
 
 /-- Topology on the total space of the continuous `σ`-semilinear maps between two "normable" vector
@@ -520,7 +520,7 @@ theorem inCoordinates_apply_eq₂
     (trivializationAt F₃ E₃ x₀).linearMapAt 𝕜 x
       (ϕ ((trivializationAt F₁ E₁ x₀).symm x v) ((trivializationAt F₂ E₂ x₀).symm x w)) := by
   rw [inCoordinates_eq h₁x (by simp [h₂x, h₃x])]
-  simp [hom_trivializationAt, Trivialization.continuousLinearMap_apply]
+  simp [hom_trivializationAt, Trivialization.continuousLinearMap_apply, h₂x]
 
 end TwoVariables
 

Mathlib/Topology/VectorBundle/Riemannian.lean

@@ -183,7 +183,8 @@ lemma eventually_norm_symmL_trivializationAt_self_comp_lt (x : B) {r : ℝ} (hr
   let w := (trivializationAt F E x).continuousLinearMapAt ℝ y v
   suffices ‖((trivializationAt F E x).symmL ℝ x) w‖ ^ 2 ≤ r' ^ 2 * ‖v‖ ^ 2 from
     le_of_sq_le_sq (by simpa [mul_pow]) (by positivity)
-  simp only [Trivialization.symmL_apply, ← real_inner_self_eq_norm_sq, hg]
+  simp only [Trivialization.symmL_apply, mem_baseSet_trivializationAt,
+    ← real_inner_self_eq_norm_sq, hg]
   have hgy : g y v v = g' y w w := by
     rw [inCoordinates_apply_eq₂ h'y h'y (Set.mem_univ _)]
     have A : ((trivializationAt F E x).symm y)
@@ -228,8 +229,8 @@ lemma eventually_norm_trivializationAt_lt (x : B) :
       ((trivializationAt F E x).symmL ℝ x) = ContinuousLinearMap.id _ _ := by
     ext v
     have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
-    simp only [Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply, comp_apply,
-      id_apply]
+    simp only [Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
+      mem_baseSet_trivializationAt, comp_apply, id_apply]
     convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
     simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
   have : (trivializationAt F E x).continuousLinearMapAt ℝ y =
@@ -286,7 +287,7 @@ lemma eventually_norm_symmL_trivializationAt_comp_self_lt (x : B) {r : ℝ} (hr
   let w := (trivializationAt F E x).continuousLinearMapAt ℝ x v
   suffices ‖((trivializationAt F E x).symmL ℝ y) w‖ ^ 2 ≤ r' ^ 2 * ‖v‖ ^ 2 from
     le_of_sq_le_sq (by simpa [mul_pow]) (by positivity)
-  simp only [Trivialization.symmL_apply, ← real_inner_self_eq_norm_sq, hg]
+  simp only [Trivialization.symmL_apply, h'y, ← real_inner_self_eq_norm_sq, hg]
   have hgx : g x v v = g' x w w := by
     rw [inCoordinates_apply_eq₂ h'x h'x (Set.mem_univ _)]
     have A : ((trivializationAt F E x).symm x)
@@ -333,8 +334,8 @@ lemma eventually_norm_symmL_trivializationAt_lt (x : B) :
       ((trivializationAt F E x).symmL ℝ x) = ContinuousLinearMap.id _ _ := by
     ext v
     have h'x : x ∈ (trivializationAt F E x).baseSet := FiberBundle.mem_baseSet_trivializationAt' x
-    simp only [Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply, comp_apply,
-      id_apply]
+    simp only [Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
+      mem_baseSet_trivializationAt, comp_apply, id_apply]
     convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
     simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
   have : (trivializationAt F E x).symmL ℝ y =