feat: forward-port 19107 (#4470)

Forward-port leanprover-community/mathlib#19107

Mathlib/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 91862a6001a8b6ae3f261cdd8eea42f6ac596886
+! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1991,52 +1991,6 @@ theorem coord_norm (x : E) (h : x ≠ 0) : ‖coord 𝕜 x h‖ = ‖x‖⁻¹ :
     homothety_inverse _ hx _ (toSpanNonzeroSingleton_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 σ₃₄]
-
-/-- 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 :=
-  {e₁₂.arrowCongrEquiv e₄₃ with -- given explicitly to help `simps`
-    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 simp only [add_comp, comp_add]
-    map_smul' := fun t f => by simp only [smul_comp, comp_smulₛₗ]
-    continuous_toFun := (continuous_id.clm_comp_const _).const_clm_comp _
-    continuous_invFun := (continuous_id.clm_comp_const _).const_clm_comp _ }
-set_option linter.uppercaseLean3 false in
-#align continuous_linear_equiv.arrow_congrSL ContinuousLinearEquiv.arrowCongrSL
-
-/-- 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

Mathlib/Analysis/NormedSpace/PiLp.lean

@@ -945,19 +945,13 @@ protected def linearEquiv : PiLp p β ≃ₗ[𝕜] ∀ i, β i :=
 #align pi_Lp.linear_equiv PiLp.linearEquiv
 
 /-- `PiLp.equiv` as a continuous linear equivalence. -/
-@[simps! (config := { fullyApplied := false }) toFun apply symm_apply]
+@[simps! (config := { fullyApplied := false }) apply symm_apply]
 protected def continuousLinearEquiv : PiLp p β ≃L[𝕜] ∀ i, β i where
   toLinearEquiv := PiLp.linearEquiv _ _ _
   continuous_toFun := continuous_equiv _ _
   continuous_invFun := continuous_equiv_symm _ _
 #align pi_Lp.continuous_linear_equiv PiLp.continuousLinearEquiv
 
--- Porting note: defined separately to appease simpNF linter
-@[simp high]
-theorem continuousLinearEquiv_invFun :
-    (PiLp.continuousLinearEquiv p 𝕜 β).toLinearEquiv.invFun = ↑(PiLp.equiv p fun i ↦ β i).symm  :=
-  rfl
-
 section Basis
 
 variable (ι)

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -1992,8 +1992,7 @@ def Simps.symm_apply (h : M₁ ≃SL[σ₁₂] M₂) : M₂ → M₁ :=
   h.symm
 #align continuous_linear_equiv.simps.symm_apply ContinuousLinearEquiv.Simps.symm_apply
 
-initialize_simps_projections ContinuousLinearEquiv
-  (toLinearEquiv_toFun → apply, toLinearEquiv_invFun → symm_apply)
+initialize_simps_projections ContinuousLinearEquiv (toFun → apply, invFun → symm_apply)
 
 theorem symm_map_nhds_eq (e : M₁ ≃SL[σ₁₂] M₂) (x : M₁) : map e.symm (𝓝 (e x)) = 𝓝 x :=
   e.toHomeomorph.symm_map_nhds_eq x

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 
 ! This file was ported from Lean 3 source module topology.algebra.module.strong_topology
-! leanprover-community/mathlib commit b8627dbac120a9ad6267a75575ae1e070d5bff5b
+! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -230,3 +230,82 @@ protected theorem hasBasis_nhds_zero [TopologicalSpace F] [TopologicalAddGroup F
 end BoundedSets
 
 end ContinuousLinearMap
+
+open ContinuousLinearMap
+
+namespace ContinuousLinearEquiv
+
+section Semilinear
+
+variable {𝕜 : Type _} {𝕜₂ : Type _} {𝕜₃ : Type _} {𝕜₄ : Type _} {E : Type _} {F : Type _}
+  {G : Type _} {H : Type _} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] [AddCommGroup H]
+  [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] [NontriviallyNormedField 𝕜₃]
+  [NontriviallyNormedField 𝕜₄] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜₃ G] [Module 𝕜₄ H]
+  [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [TopologicalSpace H]
+  [TopologicalAddGroup G] [TopologicalAddGroup H] [ContinuousConstSMul 𝕜₃ G]
+  [ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
+  {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄} [RingHomInvPair σ₁₂ σ₂₁]
+  [RingHomInvPair σ₂₁ σ₁₂] [RingHomInvPair σ₃₄ σ₄₃] [RingHomInvPair σ₄₃ σ₃₄]
+  [RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
+  [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
+
+/-- A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the
+spaces of continuous (semi)linear maps. -/
+@[simps]
+def arrowCongrₛₗ (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E →SL[σ₁₄] H) ≃ₛₗ[σ₄₃] F →SL[σ₂₃] G :=
+  { e₁₂.arrowCongrEquiv e₄₃ with
+    -- given explicitly to help `simps`
+    toFun := fun L => (e₄₃ : H →SL[σ₄₃] G).comp (L.comp (e₁₂.symm : F →SL[σ₂₁] E))
+    -- given explicitly to help `simps`
+    invFun := fun L => (e₄₃.symm : G →SL[σ₃₄] H).comp (L.comp (e₁₂ : E →SL[σ₁₂] F))
+    map_add' := fun f g => by simp only [add_comp, comp_add]
+    map_smul' := fun t f => by simp only [smul_comp, comp_smulₛₗ] }
+#align continuous_linear_equiv.arrow_congrₛₗ ContinuousLinearEquiv.arrowCongrₛₗ
+
+variable [RingHomIsometric σ₂₁]
+
+theorem arrowCongrₛₗ_continuous (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) :
+    Continuous (id (e₁₂.arrowCongrₛₗ e₄₃ : (E →SL[σ₁₄] H) ≃ₛₗ[σ₄₃] F →SL[σ₂₃] G)) := by
+  apply continuous_of_continuousAt_zero
+  show Filter.Tendsto _ _ _
+  simp_rw [(arrowCongrₛₗ e₁₂ e₄₃).map_zero]
+  rw [ContinuousLinearMap.hasBasis_nhds_zero.tendsto_iff ContinuousLinearMap.hasBasis_nhds_zero]
+  rintro ⟨sF, sG⟩ ⟨h1 : Bornology.IsVonNBounded 𝕜₂ sF, h2 : sG ∈ nhds (0 : G)⟩
+  dsimp
+  refine' ⟨(e₁₂.symm '' sF, e₄₃ ⁻¹' sG), ⟨h1.image (e₁₂.symm : F →SL[σ₂₁] E), _⟩, fun _ h _ hx =>
+    h _ (Set.mem_image_of_mem _ hx)⟩
+  apply e₄₃.continuous.continuousAt
+  simpa using h2
+#align continuous_linear_equiv.arrow_congrₛₗ_continuous ContinuousLinearEquiv.arrowCongrₛₗ_continuous
+
+variable [RingHomIsometric σ₁₂]
+
+/-- A pair of continuous (semi)linear equivalences generates an continuous (semi)linear equivalence
+between the spaces of continuous (semi)linear maps. -/
+@[simps!]
+def arrowCongrSL (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) : (E →SL[σ₁₄] H) ≃SL[σ₄₃] F →SL[σ₂₃] G :=
+  { e₁₂.arrowCongrₛₗ e₄₃ with
+    continuous_toFun := e₁₂.arrowCongrₛₗ_continuous e₄₃
+    continuous_invFun := e₁₂.symm.arrowCongrₛₗ_continuous e₄₃.symm }
+set_option linter.uppercaseLean3 false in
+#align continuous_linear_equiv.arrow_congrSL ContinuousLinearEquiv.arrowCongrSL
+
+end Semilinear
+
+section Linear
+
+variable {𝕜 : Type _} {E : Type _} {F : Type _} {G : Type _} {H : Type _} [AddCommGroup E]
+  [AddCommGroup F] [AddCommGroup G] [AddCommGroup H] [NontriviallyNormedField 𝕜] [Module 𝕜 E]
+  [Module 𝕜 F] [Module 𝕜 G] [Module 𝕜 H] [TopologicalSpace E] [TopologicalSpace F]
+  [TopologicalSpace G] [TopologicalSpace H] [TopologicalAddGroup G] [TopologicalAddGroup H]
+  [ContinuousConstSMul 𝕜 G] [ContinuousConstSMul 𝕜 H]
+
+/-- A pair of continuous linear equivalences generates an continuous linear equivalence between
+the spaces of continuous linear maps. -/
+def arrowCongr (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) : (E →L[𝕜] H) ≃L[𝕜] F →L[𝕜] G :=
+  e₁.arrowCongrSL e₂
+#align continuous_linear_equiv.arrow_congr ContinuousLinearEquiv.arrowCongr
+
+end Linear
+
+end ContinuousLinearEquiv

Mathlib/Topology/Constructions.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Patrick Massot
 
 ! This file was ported from Lean 3 source module topology.constructions
-! leanprover-community/mathlib commit 76f9c990d4b7c3dd26b87c4c4b51759e249d9e66
+! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -807,6 +807,18 @@ theorem Inducing.prod_map {f : α → β} {g : γ → δ} (hf : Inducing f) (hg
     hg.nhds_eq_comap, prod_comap_comap_eq]
 #align inducing.prod_mk Inducing.prod_map
 
+@[simp]
+theorem inducing_const_prod {a : α} {f : β → γ} : (Inducing fun x => (a, f x)) ↔ Inducing f := by
+  simp_rw [inducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose, Function.comp,
+    induced_const, top_inf_eq]
+#align inducing_const_prod inducing_const_prod
+
+@[simp]
+theorem inducing_prod_const {b : β} {f : α → γ} : (Inducing fun x => (f x, b)) ↔ Inducing f := by
+  simp_rw [inducing_iff, instTopologicalSpaceProd, induced_inf, induced_compose, Function.comp,
+    induced_const, inf_top_eq]
+#align inducing_prod_const inducing_prod_const
+
 theorem Embedding.prod_map {f : α → β} {g : γ → δ} (hf : Embedding f) (hg : Embedding g) :
     Embedding (Prod.map f g) :=
   { hf.toInducing.prod_map hg.toInducing with

Mathlib/Topology/FiberBundle/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Floris van Doorn, Heather Macbeth
 
 ! This file was ported from Lean 3 source module topology.fiber_bundle.basic
-! leanprover-community/mathlib commit 0187644979f2d3e10a06e916a869c994facd9a87
+! leanprover-community/mathlib commit f7ebde7ee0d1505dfccac8644ae12371aa3c1c9f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -779,6 +779,7 @@ end FiberBundleCore
 /-! ### Prebundle construction for constructing fiber bundles -/
 
 variable (F) (E : B → Type _) [TopologicalSpace B] [TopologicalSpace F]
+  [∀ x, TopologicalSpace (E x)]
 
 /-- This structure permits to define a fiber bundle when trivializations are given as local
 equivalences but there is not yet a topology on the total space. The total space is hence given a
@@ -792,6 +793,7 @@ structure FiberPrebundle where
   pretrivialization_mem_atlas : ∀ x : B, pretrivializationAt x ∈ pretrivializationAtlas
   continuous_trivChange : ∀ e, e ∈ pretrivializationAtlas → ∀ e', e' ∈ pretrivializationAtlas →
     ContinuousOn (e ∘ e'.toLocalEquiv.symm) (e'.target ∩ e'.toLocalEquiv.symm ⁻¹' e.source)
+  totalSpaceMk_inducing : ∀ b : B, Inducing (pretrivializationAt b ∘ totalSpaceMk b)
 #align fiber_prebundle FiberPrebundle
 
 namespace FiberPrebundle
@@ -862,35 +864,38 @@ theorem totalSpaceMk_preimage_source (b : B) :
   eq_univ_of_forall (a.mem_pretrivializationAt_source b)
 #align fiber_prebundle.total_space_mk_preimage_source FiberPrebundle.totalSpaceMk_preimage_source
 
-/-- Topology on the fibers `E b` induced by the map `E b → E.TotalSpace`. -/
-def fiberTopology (b : B) : TopologicalSpace (E b) :=
-  TopologicalSpace.induced (totalSpaceMk b) a.totalSpaceTopology
-#align fiber_prebundle.fiber_topology FiberPrebundle.fiberTopology
-
-@[continuity]
-theorem inducing_totalSpaceMk (b : B) :
-    @Inducing _ _ (a.fiberTopology b) a.totalSpaceTopology (totalSpaceMk b) := by
-  letI := a.totalSpaceTopology
-  letI := a.fiberTopology b
-  exact ⟨rfl⟩
-#align fiber_prebundle.inducing_total_space_mk FiberPrebundle.inducing_totalSpaceMk
-
 @[continuity]
 theorem continuous_totalSpaceMk (b : B) :
-    Continuous[a.fiberTopology b, a.totalSpaceTopology] (totalSpaceMk b) := by
-  letI := a.totalSpaceTopology; letI := a.fiberTopology b
-  exact (a.inducing_totalSpaceMk b).continuous
+  Continuous[_, a.totalSpaceTopology] (totalSpaceMk b) := by
+  letI := a.totalSpaceTopology
+  let e := a.trivializationOfMemPretrivializationAtlas (a.pretrivialization_mem_atlas b)
+  rw [e.toLocalHomeomorph.continuous_iff_continuous_comp_left
+      (a.totalSpaceMk_preimage_source b)]
+  exact continuous_iff_le_induced.mpr (le_antisymm_iff.mp (a.totalSpaceMk_inducing b).induced).1
 #align fiber_prebundle.continuous_total_space_mk FiberPrebundle.continuous_totalSpaceMk
 
+theorem inducing_totalSpaceMk_of_inducing_comp (b : B)
+    (h : Inducing (a.pretrivializationAt b ∘ totalSpaceMk b)) :
+    @Inducing _ _ _ a.totalSpaceTopology (totalSpaceMk b) := by
+  letI := a.totalSpaceTopology
+  rw [← restrict_comp_codRestrict (a.mem_pretrivializationAt_source b)] at h
+  apply Inducing.of_codRestrict (a.mem_pretrivializationAt_source b)
+  refine inducing_of_inducing_compose ?_ (continuousOn_iff_continuous_restrict.mp
+    (a.trivializationOfMemPretrivializationAtlas
+      (a.pretrivialization_mem_atlas b)).continuous_toFun) h
+  exact (a.continuous_totalSpaceMk b).codRestrict (a.mem_pretrivializationAt_source b)
+#align fiber_prebundle.inducing_total_space_mk_of_inducing_comp FiberPrebundle.inducing_totalSpaceMk_of_inducing_comp
+
 /-- Make a `FiberBundle` from a `FiberPrebundle`.  Concretely this means
 that, given a `FiberPrebundle` structure for a sigma-type `E` -- which consists of a
 number of "pretrivializations" identifying parts of `E` with product spaces `U × F` -- one
 establishes that for the topology constructed on the sigma-type using
 `FiberPrebundle.totalSpaceTopology`, these "pretrivializations" are actually
 "trivializations" (i.e., homeomorphisms with respect to the constructed topology). -/
-def toFiberBundle : @FiberBundle B F _ _ E a.totalSpaceTopology a.fiberTopology :=
-  let _ := a.totalSpaceTopology; let _ := a.fiberTopology
-  { totalSpaceMk_inducing' := a.inducing_totalSpaceMk,
+def toFiberBundle : @FiberBundle B F _ _ E a.totalSpaceTopology _ :=
+  let _ := a.totalSpaceTopology
+  { totalSpaceMk_inducing' := fun b ↦ a.inducing_totalSpaceMk_of_inducing_comp b
+      (a.totalSpaceMk_inducing b)
     trivializationAtlas' :=
       { e | ∃ (e₀ : _) (he₀ : e₀ ∈ a.pretrivializationAtlas),
         e = a.trivializationOfMemPretrivializationAtlas he₀ },
@@ -902,7 +907,6 @@ def toFiberBundle : @FiberBundle B F _ _ E a.totalSpaceTopology a.fiberTopology
 
 theorem continuous_proj : @Continuous _ _ a.totalSpaceTopology _ (π E) := by
   letI := a.totalSpaceTopology
-  letI := a.fiberTopology
   letI := a.toFiberBundle
   exact FiberBundle.continuous_proj F E
 #align fiber_prebundle.continuous_proj FiberPrebundle.continuous_proj