chore: mark coordinateChange_apply_snd simp

grunweg · grunweg · commit 1c1f6dc0c6c4 · 2026-04-02T13:52:39.000+02:00
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean b/Mathlib/Geometry/Manifold/VectorBundle/Basic.lean
@@ -405,10 +405,9 @@ theorem ContMDiffWithinAt.change_section_trivialization {f : M → TotalSpace F
     (he : f x ∈ e.source) (he' : f x ∈ e'.source) :
     ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun y ↦ (e' (f y)).2) s x := by
   rw [Trivialization.mem_source] at he he'
-  refine (hp.coordChange hf he he').congr_of_eventuallyEq ?_ ?_
-  · filter_upwards [hp.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy
-    rw [Function.comp_apply, e.coordChange_apply_snd _ hy]
-  · rw [Function.comp_apply, e.coordChange_apply_snd _ he]
+  refine (hp.coordChange hf he he').congr_of_eventuallyEq ?_ (by simp [he])
+  filter_upwards [hp.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy
+  simp_all
 
 theorem Bundle.Trivialization.contMDiffWithinAt_snd_comp_iff₂ {f : M → TotalSpace F E}
     (hp : ContMDiffWithinAt IM IB n (π F E ∘ f) s x)
diff --git a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean
@@ -212,10 +212,9 @@ lemma MDifferentiableWithinAt.change_section_trivialization
     (he : f x₀ ∈ e.source) (he' : f x₀ ∈ e'.source) :
     MDiffAt[s] (fun x ↦ (e' (f x)).2) x₀ := by
   rw [Trivialization.mem_source] at he he'
-  refine (hf.coordChange he'f he he').congr_of_eventuallyEq ?_ ?_
-  · filter_upwards [hf.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy
-    rw [Function.comp_apply, e.coordChange_apply_snd e' hy]
-  · rw [Function.comp_apply, e.coordChange_apply_snd _ he]
+  refine (hf.coordChange he'f he he').congr_of_eventuallyEq ?_ (by simp [he])
+  filter_upwards [hf.continuousWithinAt (e.open_baseSet.mem_nhds he)] with y hy
+  simp_all
 
 namespace Bundle.Trivialization
 
diff --git a/Mathlib/Topology/FiberBundle/Trivialization.lean b/Mathlib/Topology/FiberBundle/Trivialization.lean
@@ -739,6 +739,7 @@ theorem mk_coordChange (e₁ e₂ : Trivialization F proj) {b : B} (h₁ : b ∈
   · rwa [e₁.proj_symm_apply' h₁]
   · rwa [e₁.proj_symm_apply' h₁]
 
+@[simp]
 theorem coordChange_apply_snd (e₁ e₂ : Trivialization F proj) {p : Z} (h : proj p ∈ e₁.baseSet) :
     e₁.coordChange e₂ (proj p) (e₁ p).snd = (e₂ p).snd := by
   rw [coordChange, e₁.symm_apply_mk_proj (e₁.mem_source.2 h)]
@@ -902,7 +903,7 @@ noncomputable def piecewiseLe [LinearOrder B] [OrderTopology B] (e e' : Triviali
     rintro p rfl
     ext1
     · simp [*]
-    · simp [coordChange_apply_snd, *]
+    · simp [*]
 
 open Classical in
 /-- Given two bundle trivializations `e`, `e'` over disjoint sets, `e.disjoint_union e' H` is the
