chore: mark some lemmas as simp

grunweg · grunweg · commit 53426fc6a4e4 · 2025-02-04T13:59:10.000+01:00
diff --git a/Mathlib/Geometry/Manifold/ChartedSpace.lean b/Mathlib/Geometry/Manifold/ChartedSpace.lean
@@ -889,11 +889,13 @@ lemma ChartedSpace.sum_chartAt_inr (x' : M') :
     chartAt H (Sum.inr x') = (chartAt H x').lift_openEmbedding (X' := M ⊕ M') IsOpenEmbedding.inr :=
   rfl
 
+@[simp]
 lemma sum_chartAt_inl_apply {x : M} :
     ((chartAt H (.inl x : M ⊕ M')) (Sum.inl x)) = (chartAt H x) x := by
   rw [ChartedSpace.sum_chartAt_inl]
   exact PartialHomeomorph.lift_openEmbedding_apply _ _
 
+@[simp]
 lemma sum_chartAt_inr_apply {x : M'} :
     ((chartAt H (.inr x : M ⊕ M')) (Sum.inr x)) = (chartAt H x) x := by
   rw [ChartedSpace.sum_chartAt_inr]
diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Product.lean b/Mathlib/Geometry/Manifold/ContMDiff/Product.lean
@@ -395,10 +395,12 @@ lemma ContMDiff.inr : ContMDiff I I n (@Sum.inr M M') := by
   rw [← I.image_eq (chartAt H x).target]
   exact (chartAt H x).extend_image_target_mem_nhds (mem_chart_source _ x)
 
+@[simp]
 lemma extChartAt_inl_apply {x : M} :
     ((extChartAt I (.inl x : M ⊕ M')) (Sum.inl x)) = (extChartAt I x) x := by
   simp [sum_chartAt_inl_apply]
 
+@[simp]
 lemma extChartAt_inr_apply {x : M'} :
     ((extChartAt I (.inr x : M ⊕ M')) (Sum.inr x)) = (extChartAt I x) x := by
   simp [sum_chartAt_inr_apply]
diff --git a/Mathlib/Topology/PartialHomeomorph.lean b/Mathlib/Topology/PartialHomeomorph.lean
@@ -1371,6 +1371,7 @@ noncomputable def lift_openEmbedding (e : PartialHomeomorph X Z) (hf : IsOpenEmb
 lemma lift_openEmbedding_toFun (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) :
     (e.lift_openEmbedding hf) = extend f e (fun _ ↦ (Classical.arbitrary Z)) := rfl
 
+@[simp]
 lemma lift_openEmbedding_apply (e : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) {x : X} :
     (lift_openEmbedding e hf) (f x) = e x := by
   simp_rw [e.lift_openEmbedding_toFun]
@@ -1397,6 +1398,7 @@ lemma lift_openEmbedding_symm_target (e : PartialHomeomorph X Z) (hf : IsOpenEmb
     (e.lift_openEmbedding hf).symm.target = f '' e.source := by
   rw [PartialHomeomorph.symm_target, e.lift_openEmbedding_source]
 
+@[simp]
 lemma lift_openEmbedding_trans_apply
     (e e' : PartialHomeomorph X Z) (hf : IsOpenEmbedding f) (z : Z) :
     (e.lift_openEmbedding hf).symm.trans (e'.lift_openEmbedding hf) z = (e.symm.trans e') z := by
