feat: more uses of simps in fiber bundles and vector bundles (leanprover-community#26121)

Author: sgouezel

Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

@@ -614,10 +614,10 @@ instance Bundle.Prod.contMDiffVectorBundle : ContMDiffVectorBundle n (F₁ × F
     refine ContMDiffOn.congr ?_ (e₁.coordChangeL_prod 𝕜 e₁' e₂ e₂')
     refine ContMDiffOn.clm_prodMap ?_ ?_
     · refine (contMDiffOn_coordChangeL e₁ e₁').mono ?_
-      simp only [Trivialization.baseSet_prod, mfld_simps]
+      simp only [Trivialization.prod_baseSet, mfld_simps]
       mfld_set_tac
     · refine (contMDiffOn_coordChangeL e₂ e₂').mono ?_
-      simp only [Trivialization.baseSet_prod, mfld_simps]
+      simp only [Trivialization.prod_baseSet, mfld_simps]
       mfld_set_tac
 
 end Prod

Mathlib/Topology/FiberBundle/Constructions.lean

@@ -48,10 +48,12 @@ theorem isInducing_toProd : IsInducing (TotalSpace.toProd B F) :=
 @[deprecated (since := "2024-10-28")] alias inducing_toProd := isInducing_toProd
 
 /-- Homeomorphism between the total space of the trivial bundle and the Cartesian product. -/
+@[simps!]
 def homeomorphProd : TotalSpace F (Trivial B F) ≃ₜ B × F :=
   (TotalSpace.toProd _ _).toHomeomorphOfIsInducing (isInducing_toProd B F)
 
 /-- Local trivialization for trivial bundle. -/
+@[simps!]
 def trivialization : Trivialization F (π F (Bundle.Trivial B F)) where
   toPartialHomeomorph := (homeomorphProd B F).toPartialHomeomorph
   baseSet := univ
@@ -60,14 +62,16 @@ def trivialization : Trivialization F (π F (Bundle.Trivial B F)) where
   target_eq := univ_prod_univ.symm
   proj_toFun _ _ := rfl
 
-@[simp]
-theorem trivialization_source : (trivialization B F).source = univ := rfl
+@[simp] lemma trivialization_symm_apply [Zero F] (b : B) (f : F) :
+    (trivialization B F).symm b f = f := by
+  simp [trivialization, homeomorphProd, TotalSpace.toProd, Trivialization.symm,
+    Pretrivialization.symm, Trivialization.toPretrivialization]
 
-@[simp]
-theorem trivialization_target : (trivialization B F).target = univ := rfl
+@[simp] lemma toPartialHomeomorph_trivialization_symm_apply (v : B × F) :
+    (trivialization B F).toPartialHomeomorph.symm v = ⟨v.1, v.2⟩ := rfl
 
 /-- Fiber bundle instance on the trivial bundle. -/
-instance fiberBundle : FiberBundle F (Bundle.Trivial B F) where
+@[simps] instance fiberBundle : FiberBundle F (Bundle.Trivial B F) where
   trivializationAtlas' := {trivialization B F}
   trivializationAt' _ := trivialization B F
   mem_baseSet_trivializationAt' := mem_univ
@@ -187,6 +191,7 @@ variable (e₁ e₂)
 /-- Given trivializations `e₁`, `e₂` for bundle types `E₁`, `E₂` over a base `B`, the induced
 trivialization for the fiberwise product of `E₁` and `E₂`, whose base set is
 `e₁.baseSet ∩ e₂.baseSet`. -/
+@[simps!]
 noncomputable def prod : Trivialization (F₁ × F₂) (π (F₁ × F₂) (E₁ ×ᵇ E₂)) where
   toFun := Prod.toFun' e₁ e₂
   invFun := Prod.invFun' e₁ e₂
@@ -210,8 +215,7 @@ noncomputable def prod : Trivialization (F₁ × F₂) (π (F₁ × F₂) (E₁
   target_eq := rfl
   proj_toFun _ _ := rfl
 
-@[simp]
-theorem baseSet_prod : (prod e₁ e₂).baseSet = e₁.baseSet ∩ e₂.baseSet := rfl
+@[deprecated (since := "2025-0619")] alias baseSet_prod := prod_baseSet
 
 theorem prod_symm_apply (x : B) (w₁ : F₁) (w₂ : F₂) :
     (prod e₁ e₂).toPartialEquiv.symm (x, w₁, w₂) = ⟨x, e₁.symm x w₁, e₂.symm x w₂⟩ := rfl
@@ -224,7 +228,7 @@ variable [∀ x, Zero (E₁ x)] [∀ x, Zero (E₂ x)] [∀ x : B, TopologicalSp
   [∀ x : B, TopologicalSpace (E₂ x)] [FiberBundle F₁ E₁] [FiberBundle F₂ E₂]
 
 /-- The product of two fiber bundles is a fiber bundle. -/
-noncomputable instance FiberBundle.prod : FiberBundle (F₁ × F₂) (E₁ ×ᵇ E₂) where
+@[simps] noncomputable instance FiberBundle.prod : FiberBundle (F₁ × F₂) (E₁ ×ᵇ E₂) where
   totalSpaceMk_isInducing' b := by
     rw [← (Prod.isInducing_diag F₁ E₁ F₂ E₂).of_comp_iff]
     exact (totalSpaceMk_isInducing F₁ E₁ b).prodMap (totalSpaceMk_isInducing F₂ E₂ b)
@@ -297,6 +301,7 @@ variable {E F}
 variable [∀ _b, Zero (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]
 noncomputable def Trivialization.pullback (e : Trivialization F (π F E)) (f : K) :
     Trivialization F (π F ((f : B' → B) *ᵖ E)) where
   toFun z := (z.proj, (e (Pullback.lift f z)).2)
@@ -336,6 +341,7 @@ noncomputable def Trivialization.pullback (e : Trivialization F (π F E)) (f : K
   target_eq := rfl
   proj_toFun _ _ := rfl
 
+@[simps]
 noncomputable instance FiberBundle.pullback [∀ x, TopologicalSpace (E x)] [FiberBundle F E]
     (f : K) : FiberBundle F ((f : B' → B) *ᵖ E) where
   totalSpaceMk_isInducing' x :=

Mathlib/Topology/FiberBundle/Trivialization.lean

@@ -298,6 +298,15 @@ instance : CoeFun (Trivialization F proj) fun _ => Z → B × F := ⟨toFun'⟩
 instance : Coe (Trivialization F proj) (Pretrivialization F proj) :=
   ⟨toPretrivialization⟩
 
+/-- See Note [custom simps projection] -/
+def Simps.apply (proj : Z → B) (e : Trivialization F proj) : Z → B × F := e
+
+/-- See Note [custom simps projection] -/
+noncomputable def Simps.symm_apply (proj : Z → B) (e : Trivialization F proj) : B × F → Z :=
+  e.toPartialHomeomorph.symm
+
+initialize_simps_projections Trivialization (toFun → apply, invFun → symm_apply)
+
 theorem toPretrivialization_injective :
     Function.Injective fun e : Trivialization F proj => e.toPretrivialization := fun e e' h => by
   ext1

Mathlib/Topology/Homeomorph/Defs.lean

@@ -366,6 +366,12 @@ def toHomeomorphOfIsInducing (f : X ≃ Y) (hf : IsInducing f) : X ≃ₜ Y :=
 
 @[deprecated (since := "2024-10-28")] alias toHomeomorphOfInducing := toHomeomorphOfIsInducing
 
+@[simp] lemma toHomeomorphOfIsInducing_apply (f : X ≃ Y) (hf : IsInducing f) :
+    ⇑(f.toHomeomorphOfIsInducing hf) = f := rfl
+
+@[simp] lemma toHomeomorphOfIsInducing_symm_apply (f : X ≃ Y) (hf : IsInducing f) :
+    ⇑(f.toHomeomorphOfIsInducing hf).symm = f.symm := rfl
+
 /-- If a bijective map `e : X ≃ Y` is continuous and open, then it is a homeomorphism. -/
 @[simps! toEquiv]
 def toHomeomorphOfContinuousOpen (e : X ≃ Y) (h₁ : Continuous e) (h₂ : IsOpenMap e) : X ≃ₜ Y :=

Mathlib/Topology/VectorBundle/Basic.lean

@@ -655,6 +655,8 @@ theorem mem_localTrivAt_baseSet : b ∈ (Z.localTrivAt b).baseSet :=
 instance fiberBundle : FiberBundle F Z.Fiber :=
   Z.toFiberBundleCore.fiberBundle
 
+protected lemma trivializationAt : trivializationAt F Z.Fiber b = Z.localTrivAt b := rfl
+
 instance vectorBundle : VectorBundle R F Z.Fiber where
   trivialization_linear' := by
     rintro _ ⟨i, rfl⟩

Mathlib/Topology/VectorBundle/Constructions.lean

@@ -96,7 +96,7 @@ theorem coordChangeL_prod [e₁.IsLinear 𝕜] [e₁'.IsLinear 𝕜] [e₂.IsLin
 variable {e₁ e₂} [∀ x : B, TopologicalSpace (E₁ x)] [∀ x : B, TopologicalSpace (E₂ x)]
   [FiberBundle F₁ E₁] [FiberBundle F₂ E₂]
 
-theorem prod_apply [e₁.IsLinear 𝕜] [e₂.IsLinear 𝕜] {x : B} (hx₁ : x ∈ e₁.baseSet)
+theorem prod_apply' [e₁.IsLinear 𝕜] [e₂.IsLinear 𝕜] {x : B} (hx₁ : x ∈ e₁.baseSet)
     (hx₂ : x ∈ e₂.baseSet) (v₁ : E₁ x) (v₂ : E₂ x) :
     prod e₁ e₂ ⟨x, (v₁, v₂)⟩ =
       ⟨x, e₁.continuousLinearEquivAt 𝕜 x hx₁ v₁, e₂.continuousLinearEquivAt 𝕜 x hx₂ v₂⟩ :=
@@ -120,7 +120,7 @@ instance VectorBundle.prod [VectorBundle 𝕜 F₁ E₁] [VectorBundle 𝕜 F₂
     rintro _ _ ⟨e₁, e₂, he₁, he₂, rfl⟩ ⟨e₁', e₂', he₁', he₂', rfl⟩
     refine (((continuousOn_coordChange 𝕜 e₁ e₁').mono ?_).prod_mapL 𝕜
       ((continuousOn_coordChange 𝕜 e₂ e₂').mono ?_)).congr ?_ <;>
-      dsimp only [baseSet_prod, mfld_simps]
+      dsimp only [prod_baseSet, mfld_simps]
     · mfld_set_tac
     · mfld_set_tac
     · rintro b hb
@@ -142,7 +142,7 @@ theorem Trivialization.continuousLinearEquivAt_prod {e₁ : Trivialization F₁
   ext v : 2
   obtain ⟨v₁, v₂⟩ := v
   rw [(e₁.prod e₂).continuousLinearEquivAt_apply 𝕜, Trivialization.prod]
-  exact (congr_arg Prod.snd (prod_apply 𝕜 hx.1 hx.2 v₁ v₂) :)
+  exact (congr_arg Prod.snd (prod_apply' 𝕜 hx.1 hx.2 v₁ v₂) :)
 
 end