bump to nightly-2023-05-29-03

mathlib commit leanprover-community/mathlib@88a563b

Mathbin/Analysis/Calculus/Deriv/Slope.lean

@@ -81,12 +81,14 @@ theorem hasDerivWithinAt_iff_tendsto_slope :
   exact hasDerivAtFilter_iff_tendsto_slope
 #align has_deriv_within_at_iff_tendsto_slope hasDerivWithinAt_iff_tendsto_slope
 
+#print hasDerivWithinAt_iff_tendsto_slope' /-
 theorem hasDerivWithinAt_iff_tendsto_slope' (hs : x ∉ s) :
     HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s] x) (𝓝 f') :=
   by
   convert← hasDerivWithinAt_iff_tendsto_slope
   exact diff_singleton_eq_self hs
 #align has_deriv_within_at_iff_tendsto_slope' hasDerivWithinAt_iff_tendsto_slope'
+-/
 
 theorem hasDerivAt_iff_tendsto_slope : HasDerivAt f f' x ↔ Tendsto (slope f x) (𝓝[≠] x) (𝓝 f') :=
   hasDerivAtFilter_iff_tendsto_slope

Mathbin/Analysis/Convolution.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 
 ! This file was ported from Lean 3 source module analysis.convolution
-! leanprover-community/mathlib commit fd5edc43dc4f10b85abfe544b88f82cf13c5f844
+! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1665,7 +1665,8 @@ theorem contDiffOn_convolution_right_with_param {f : G → E} {n : ℕ∞} (L :
     simp only [ef, eg, comp_app, ContinuousLinearEquiv.apply_symm_apply, coe_comp',
       ContinuousLinearEquiv.prod_apply, ContinuousLinearEquiv.map_sub,
       ContinuousLinearEquiv.arrowCongr, ContinuousLinearEquiv.arrowCongrSL_symm_apply,
-      ContinuousLinearEquiv.coe_coe, comp_app, ContinuousLinearEquiv.apply_symm_apply]
+      ContinuousLinearEquiv.coe_coe, comp_app, ContinuousLinearEquiv.apply_symm_apply,
+      LinearEquiv.invFun_eq_symm, ContinuousLinearEquiv.arrowCongrₛₗ_symm_apply, eq_self_iff_true]
   simp_rw [this] at A
   exact A
 #align cont_diff_on_convolution_right_with_param contDiffOn_convolution_right_with_param

Mathbin/Analysis/NormedSpace/OperatorNorm.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
 
 ! This file was ported from Lean 3 source module analysis.normed_space.operator_norm
-! leanprover-community/mathlib commit 50251fd6309cca5ca2e747882ffecd2729f38c5d
+! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -2023,62 +2023,6 @@ theorem coord_norm (x : E) (h : x ≠ 0) : ‖coord 𝕜 x h‖ = ‖x‖⁻¹ :
       homothety_inverse _ hx _ (to_span_nonzero_singleton_homothety 𝕜 x h) _
 #align continuous_linear_equiv.coord_norm ContinuousLinearEquiv.coord_norm
 
-variable {𝕜} {𝕜₄ : Type _} [NontriviallyNormedField 𝕜₄]
-
-variable {H : Type _} [NormedAddCommGroup H] [NormedSpace 𝕜₄ H] [NormedSpace 𝕜₃ G]
-
-variable {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
-
-variable {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃}
-
-variable {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
-
-variable [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄]
-
-variable [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
-
-variable [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
-
-variable [RingHomIsometric σ₁₄] [RingHomIsometric σ₂₃]
-
-variable [RingHomIsometric σ₄₃] [RingHomIsometric σ₂₄]
-
-variable [RingHomIsometric σ₁₃] [RingHomIsometric σ₁₂]
-
-variable [RingHomIsometric σ₃₄]
-
-include σ₂₁ σ₃₄ σ₁₃ σ₂₄
-
-#print ContinuousLinearEquiv.arrowCongrSL /-
-/-- A pair of continuous (semi)linear equivalences generates an continuous (semi)linear equivalence
-between the spaces of continuous (semi)linear maps. -/
-@[simps apply symm_apply]
-def arrowCongrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G :=
-  {-- given explicitly to help `simps`
-        -- given explicitly to help `simps`
-        e₁₂.arrowCongrEquiv
-      e₄₃ with
-    toFun := fun L => (e₄₃ : H →SL[σ₄₃] G).comp (L.comp (e₁₂.symm : F →SL[σ₂₁] E))
-    invFun := fun L => (e₄₃.symm : G →SL[σ₃₄] H).comp (L.comp (e₁₂ : E →SL[σ₁₂] F))
-    map_add' := fun f g => by rw [add_comp, comp_add]
-    map_smul' := fun t f => by rw [smul_comp, comp_smulₛₗ]
-    continuous_toFun := (continuous_id.clm_comp_const _).const_clm_comp _
-    continuous_invFun := (continuous_id.clm_comp_const _).const_clm_comp _ }
-#align continuous_linear_equiv.arrow_congrSL ContinuousLinearEquiv.arrowCongrSL
--/
-
-omit σ₂₁ σ₃₄ σ₁₃ σ₂₄
-
-#print ContinuousLinearEquiv.arrowCongr /-
-/-- A pair of continuous linear equivalences generates an continuous linear equivalence between
-the spaces of continuous linear maps. -/
-def arrowCongr {F H : Type _} [NormedAddCommGroup F] [NormedAddCommGroup H] [NormedSpace 𝕜 F]
-    [NormedSpace 𝕜 G] [NormedSpace 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) :
-    (E →L[𝕜] H) ≃L[𝕜] F →L[𝕜] G :=
-  arrowCongrSL e₁ e₂
-#align continuous_linear_equiv.arrow_congr ContinuousLinearEquiv.arrowCongr
--/
-
 end
 
 end ContinuousLinearEquiv

Mathbin/Analysis/NormedSpace/TrivSqZeroExt.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 
 ! This file was ported from Lean 3 source module analysis.normed_space.triv_sq_zero_ext
-! leanprover-community/mathlib commit b8d2eaa69d69ce8f03179a5cda774fc0cde984e4
+! leanprover-community/mathlib commit 88a563b158f59f2983cfad685664da95502e8cdd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -25,9 +25,14 @@ For now, this file contains results about `exp` for this type.
 * `triv_sq_zero_ext.exp_inr`
 
 ## TODO
+
 * Actually define a sensible norm on `triv_sq_zero_ext R M`, so that we have access to lemmas
   like `exp_add`.
-* Generalize some of these results to non-commutative `R`.
+* Generalize more of these results to non-commutative `R`. In principle, under sufficient conditions
+  we should expect
+ `(exp 𝕜 x).snd = ∫ t in 0..1, exp 𝕜 (t • x.fst) • op (exp 𝕜 ((1 - t) • x.fst)) • x.snd`
+  ([Physics.SE](https://physics.stackexchange.com/a/41671/185147), and
+  https://link.springer.com/chapter/10.1007/978-3-540-44953-9_2).
 
 -/
 
@@ -43,20 +48,31 @@ section Topology
 
 variable [TopologicalSpace R] [TopologicalSpace M]
 
-/-- If `exp R x.fst` converges to `e` then `exp R x` converges to `inl e + inr (e • x.snd)`. -/
-theorem hasSum_expSeries [Field 𝕜] [CharZero 𝕜] [CommRing R] [AddCommGroup M] [Algebra 𝕜 R]
-    [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [Module 𝕜 M] [IsScalarTower 𝕜 R M]
-    [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] (x : tsze R M) {e : R}
+/-- If `exp R x.fst` converges to `e` then `(exp R x).fst` converges to `e`. -/
+theorem hasSum_fst_expSeries [Field 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module R M]
+    [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [Module 𝕜 M] [IsScalarTower 𝕜 R M]
+    [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M]
+    [ContinuousSMul Rᵐᵒᵖ M] (x : tsze R M) {e : R}
+    (h : HasSum (fun n => expSeries 𝕜 R n fun _ => x.fst) e) :
+    HasSum (fun n => fst (expSeries 𝕜 (tsze R M) n fun _ => x)) e := by
+  simpa [expSeries_apply_eq] using h
+#align triv_sq_zero_ext.has_sum_fst_exp_series TrivSqZeroExt.hasSum_fst_expSeries
+
+/-- If `exp R x.fst` converges to `e` then `(exp R x).snd` converges to `e • x.snd`. -/
+theorem hasSum_snd_expSeries_of_smul_comm [Field 𝕜] [CharZero 𝕜] [Ring R] [AddCommGroup M]
+    [Algebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [Module 𝕜 M]
+    [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalRing R] [TopologicalAddGroup M]
+    [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] (x : tsze R M)
+    (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) {e : R}
     (h : HasSum (fun n => expSeries 𝕜 R n fun _ => x.fst) e) :
-    HasSum (fun n => expSeries 𝕜 (tsze R M) n fun _ => x) (inl e + inr (e • x.snd)) :=
+    HasSum (fun n => snd (expSeries 𝕜 (tsze R M) n fun _ => x)) (e • x.snd) :=
   by
   simp_rw [expSeries_apply_eq] at *
   conv =>
     congr
     ext
-    rw [← inl_fst_add_inr_snd_eq (x ^ _), fst_pow, snd_pow, smul_add, ← inr_smul, ← inl_smul,
-      nsmul_eq_smul_cast 𝕜 n, smul_smul, inv_mul_eq_div, ← inv_div, ← smul_assoc]
-  refine' (has_sum_inl M h).add (has_sum_inr M _)
+    rw [snd_smul, snd_pow_of_smul_comm _ _ hx, nsmul_eq_smul_cast 𝕜 n, smul_smul, inv_mul_eq_div, ←
+      inv_div, ← smul_assoc]
   apply HasSum.smul_const
   rw [← hasSum_nat_add_iff' 1]; swap; infer_instance
   rw [Finset.range_one, Finset.sum_singleton, Nat.cast_zero, div_zero, inv_zero, zero_smul,
@@ -65,12 +81,62 @@ theorem hasSum_expSeries [Field 𝕜] [CharZero 𝕜] [CommRing R] [AddCommGroup
     Nat.succ_eq_add_one,
     mul_div_cancel_left _ ((@Nat.cast_ne_zero 𝕜 _ _ _).mpr <| Nat.succ_ne_zero _)]
   exact h
-#align triv_sq_zero_ext.has_sum_exp_series TrivSqZeroExt.hasSum_expSeries
+#align triv_sq_zero_ext.has_sum_snd_exp_series_of_smul_comm TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm
+
+/-- If `exp R x.fst` converges to `e` then `exp R x` converges to `inl e + inr (e • x.snd)`. -/
+theorem hasSum_expSeries_of_smul_comm [Field 𝕜] [CharZero 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R]
+    [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [Module 𝕜 M] [IsScalarTower 𝕜 R M]
+    [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M]
+    [ContinuousSMul Rᵐᵒᵖ M] (x : tsze R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd)
+    {e : R} (h : HasSum (fun n => expSeries 𝕜 R n fun _ => x.fst) e) :
+    HasSum (fun n => expSeries 𝕜 (tsze R M) n fun _ => x) (inl e + inr (e • x.snd)) := by
+  simpa only [inl_fst_add_inr_snd_eq] using
+    (has_sum_inl _ <| has_sum_fst_exp_series 𝕜 x h).add
+      (has_sum_inr _ <| has_sum_snd_exp_series_of_smul_comm 𝕜 x hx h)
+#align triv_sq_zero_ext.has_sum_exp_series_of_smul_comm TrivSqZeroExt.hasSum_expSeries_of_smul_comm
 
 end Topology
 
 section NormedRing
 
+variable [IsROrC 𝕜] [NormedRing R] [AddCommGroup M]
+
+variable [NormedAlgebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M]
+
+variable [Module 𝕜 M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M]
+
+variable [TopologicalSpace M] [TopologicalRing R]
+
+variable [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M]
+
+variable [CompleteSpace R] [T2Space R] [T2Space M]
+
+theorem exp_def_of_smul_comm (x : tsze R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) :
+    exp 𝕜 x = inl (exp 𝕜 x.fst) + inr (exp 𝕜 x.fst • x.snd) :=
+  by
+  simp_rw [exp, FormalMultilinearSeries.sum]
+  refine' (has_sum_exp_series_of_smul_comm 𝕜 x hx _).tsum_eq
+  exact expSeries_hasSum_exp _
+#align triv_sq_zero_ext.exp_def_of_smul_comm TrivSqZeroExt.exp_def_of_smul_comm
+
+@[simp]
+theorem exp_inl (x : R) : exp 𝕜 (inl x : tsze R M) = inl (exp 𝕜 x) :=
+  by
+  rw [exp_def_of_smul_comm, snd_inl, fst_inl, smul_zero, inr_zero, add_zero]
+  · rw [snd_inl, fst_inl, smul_zero, smul_zero]
+#align triv_sq_zero_ext.exp_inl TrivSqZeroExt.exp_inl
+
+@[simp]
+theorem exp_inr (m : M) : exp 𝕜 (inr m : tsze R M) = 1 + inr m :=
+  by
+  rw [exp_def_of_smul_comm, snd_inr, fst_inr, exp_zero, one_smul, inl_one]
+  · rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]
+#align triv_sq_zero_ext.exp_inr TrivSqZeroExt.exp_inr
+
+end NormedRing
+
+section NormedCommRing
+
 variable [IsROrC 𝕜] [NormedCommRing R] [AddCommGroup M]
 
 variable [NormedAlgebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M]
@@ -84,10 +150,7 @@ variable [TopologicalAddGroup M] [ContinuousSMul R M]
 variable [CompleteSpace R] [T2Space R] [T2Space M]
 
 theorem exp_def (x : tsze R M) : exp 𝕜 x = inl (exp 𝕜 x.fst) + inr (exp 𝕜 x.fst • x.snd) :=
-  by
-  simp_rw [exp, FormalMultilinearSeries.sum]
-  refine' (has_sum_exp_series 𝕜 x _).tsum_eq
-  exact expSeries_hasSum_exp _
+  exp_def_of_smul_comm 𝕜 x (op_smul_eq_smul _ _)
 #align triv_sq_zero_ext.exp_def TrivSqZeroExt.exp_def
 
 @[simp]
@@ -100,24 +163,14 @@ theorem snd_exp (x : tsze R M) : snd (exp 𝕜 x) = exp 𝕜 x.fst • x.snd :=
   rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]
 #align triv_sq_zero_ext.snd_exp TrivSqZeroExt.snd_exp
 
-@[simp]
-theorem exp_inl (x : R) : exp 𝕜 (inl x : tsze R M) = inl (exp 𝕜 x) := by
-  rw [exp_def, fst_inl, snd_inl, smul_zero, inr_zero, add_zero]
-#align triv_sq_zero_ext.exp_inl TrivSqZeroExt.exp_inl
-
-@[simp]
-theorem exp_inr (m : M) : exp 𝕜 (inr m : tsze R M) = 1 + inr m := by
-  rw [exp_def, fst_inr, exp_zero, snd_inr, one_smul, inl_one]
-#align triv_sq_zero_ext.exp_inr TrivSqZeroExt.exp_inr
-
 /-- Polar form of trivial-square-zero extension. -/
 theorem eq_smul_exp_of_invertible (x : tsze R M) [Invertible x.fst] :
     x = x.fst • exp 𝕜 (⅟ x.fst • inr x.snd) := by
   rw [← inr_smul, exp_inr, smul_add, ← inl_one, ← inl_smul, ← inr_smul, smul_eq_mul, mul_one,
     smul_smul, mul_invOf_self, one_smul, inl_fst_add_inr_snd_eq]
 #align triv_sq_zero_ext.eq_smul_exp_of_invertible TrivSqZeroExt.eq_smul_exp_of_invertible
 
-end NormedRing
+end NormedCommRing
 
 section NormedField
 

Mathbin/Geometry/Manifold/VectorBundle/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Heather Macbeth
 
 ! This file was ported from Lean 3 source module geometry.manifold.vector_bundle.basic
-! leanprover-community/mathlib commit c89fe2d59ae06402c3f55f978016d1ada444f57e
+! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -415,7 +415,7 @@ end WithTopology
 
 namespace VectorPrebundle
 
-variable {F E}
+variable [∀ x, TopologicalSpace (E x)] {F E}
 
 /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (e e' «expr ∈ » a.pretrivialization_atlas) -/
 /-- Mixin for a `vector_prebundle` stating smoothness of coordinate changes. -/
@@ -468,8 +468,8 @@ variable (IB)
 
 /-- Make a `smooth_vector_bundle` from a `smooth_vector_prebundle`.  -/
 theorem smoothVectorBundle :
-    @SmoothVectorBundle _ _ F E _ _ _ _ _ _ IB _ _ _ _ _ _ _ a.totalSpaceTopology a.fiberTopology
-      a.toFiberBundle a.to_vectorBundle :=
+    @SmoothVectorBundle _ _ F E _ _ _ _ _ _ IB _ _ _ _ _ _ _ a.totalSpaceTopology _ a.toFiberBundle
+      a.to_vectorBundle :=
   {
     smoothOn_coord_change := by
       rintro _ _ ⟨e, he, rfl⟩ ⟨e', he', rfl⟩

Mathbin/Geometry/Manifold/VectorBundle/Hom.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 
 ! This file was ported from Lean 3 source module geometry.manifold.vector_bundle.hom
-! leanprover-community/mathlib commit c89fe2d59ae06402c3f55f978016d1ada444f57e
+! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -28,16 +28,17 @@ open Bundle Set LocalHomeomorph ContinuousLinearMap Pretrivialization
 open scoped Manifold Bundle
 
 variable {𝕜 B F F₁ F₂ M M₁ M₂ : Type _} {E : B → Type _} {E₁ : B → Type _} {E₂ : B → Type _}
-  [NontriviallyNormedField 𝕜] [∀ x, AddCommMonoid (E x)] [∀ x, Module 𝕜 (E x)]
-  [NormedAddCommGroup F] [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace E)]
-  [∀ x, TopologicalSpace (E x)] [∀ x, AddCommMonoid (E₁ x)] [∀ x, Module 𝕜 (E₁ x)]
-  [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (TotalSpace E₁)]
-  [∀ x, TopologicalSpace (E₁ x)] [∀ x, AddCommMonoid (E₂ x)] [∀ x, Module 𝕜 (E₂ x)]
-  [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂] [TopologicalSpace (TotalSpace E₂)]
-  [∀ x, TopologicalSpace (E₂ x)] {EB : Type _} [NormedAddCommGroup EB] [NormedSpace 𝕜 EB]
-  {HB : Type _} [TopologicalSpace HB] (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B]
-  [ChartedSpace HB B] {EM : Type _} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type _}
-  [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M]
+  [NontriviallyNormedField 𝕜] [∀ x, AddCommGroup (E x)] [∀ x, Module 𝕜 (E x)] [NormedAddCommGroup F]
+  [NormedSpace 𝕜 F] [TopologicalSpace (TotalSpace E)] [∀ x, TopologicalSpace (E x)]
+  [∀ x, AddCommGroup (E₁ x)] [∀ x, Module 𝕜 (E₁ x)] [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁]
+  [TopologicalSpace (TotalSpace E₁)] [∀ x, TopologicalSpace (E₁ x)] [∀ x, AddCommGroup (E₂ x)]
+  [∀ x, Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂]
+  [TopologicalSpace (TotalSpace E₂)] [∀ x, TopologicalSpace (E₂ x)]
+  [_i₁ : ∀ x, TopologicalAddGroup (E₂ x)] [_i₂ : ∀ x, ContinuousSMul 𝕜 (E₂ x)] {EB : Type _}
+  [NormedAddCommGroup EB] [NormedSpace 𝕜 EB] {HB : Type _} [TopologicalSpace HB]
+  (IB : ModelWithCorners 𝕜 EB HB) [TopologicalSpace B] [ChartedSpace HB B] {EM : Type _}
+  [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type _} [TopologicalSpace HM]
+  {IM : ModelWithCorners 𝕜 EM HM} [TopologicalSpace M] [ChartedSpace HM M]
   [Is : SmoothManifoldWithCorners IM M] {n : ℕ∞} [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁]
   [FiberBundle F₂ E₂] [VectorBundle 𝕜 F₂ E₂] {e₁ e₁' : Trivialization F₁ (π E₁)}
   {e₂ e₂' : Trivialization F₂ (π E₂)}
@@ -64,10 +65,11 @@ theorem smoothOn_continuousLinearMapCoordChange [SmoothManifoldWithCorners IB B]
   · intro b hb; ext (L v)
     simp only [continuous_linear_map_coord_change, ContinuousLinearEquiv.coe_coe,
       ContinuousLinearEquiv.arrowCongrSL_apply, comp_apply, Function.comp, compL_apply, flip_apply,
-      ContinuousLinearEquiv.symm_symm]
+      ContinuousLinearEquiv.symm_symm, LinearEquiv.toFun_eq_coe,
+      ContinuousLinearEquiv.arrowCongrₛₗ_apply, ContinuousLinearMap.coe_comp']
 #align smooth_on_continuous_linear_map_coord_change smoothOn_continuousLinearMapCoordChange
 
-variable [∀ x, ContinuousAdd (E₂ x)] [∀ x, ContinuousSMul 𝕜 (E₂ x)]
+include _i₁ _i₂
 
 theorem hom_chart (y₀ y : LE₁E₂) :
     chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀ y =
@@ -110,16 +112,6 @@ instance Bundle.ContinuousLinearMap.vectorPrebundle.isSmooth :
         continuous_linear_map_coord_change_apply (RingHom.id 𝕜) e₁ e₁' e₂ e₂'⟩
 #align bundle.continuous_linear_map.vector_prebundle.is_smooth Bundle.ContinuousLinearMap.vectorPrebundle.isSmooth
 
-/-- Todo: remove this definition. It is probably needed because of the type-class pi bug
-https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/vector.20bundles.20--.20typeclass.20inference.20issue
--/
-@[reducible]
-def SmoothVectorBundle.ContinuousLinearMap.aux (x) :
-    TopologicalSpace (Bundle.ContinuousLinearMap (RingHom.id 𝕜) F₁ E₁ F₂ E₂ x) := by infer_instance
-#align smooth_vector_bundle.continuous_linear_map.aux SmoothVectorBundle.ContinuousLinearMap.aux
-
-attribute [local instance 1] SmoothVectorBundle.ContinuousLinearMap.aux
-
 instance SmoothVectorBundle.continuousLinearMap :
     SmoothVectorBundle (F₁ →L[𝕜] F₂) (Bundle.ContinuousLinearMap (RingHom.id 𝕜) F₁ E₁ F₂ E₂) IB :=
   (Bundle.ContinuousLinearMap.vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂).SmoothVectorBundle IB