feat: add some missing simp lemmas (#6028)

Author: urkud

Mathlib/Logic/Equiv/LocalEquiv.lean

@@ -654,6 +654,7 @@ theorem ofSet_symm (s : Set α) : (LocalEquiv.ofSet s).symm = LocalEquiv.ofSet s
 
 /-- Composing two local equivs if the target of the first coincides with the source of the
 second. -/
+@[simps]
 protected def trans' (e' : LocalEquiv β γ) (h : e.target = e'.source) : LocalEquiv α γ where
   toFun := e' ∘ e
   invFun := e.symm ∘ e'.symm

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -319,10 +319,16 @@ theorem continuous_const_smul_iff₀ (hc : c ≠ 0) : (Continuous fun x => c •
 
 /-- Scalar multiplication by a non-zero element of a group with zero acting on `α` is a
 homeomorphism from `α` onto itself. -/
+@[simps! (config := .asFn) apply]
 protected def Homeomorph.smulOfNeZero (c : G₀) (hc : c ≠ 0) : α ≃ₜ α :=
   Homeomorph.smul (Units.mk0 c hc)
 #align homeomorph.smul_of_ne_zero Homeomorph.smulOfNeZero
 
+@[simp]
+theorem Homeomorph.smulOfNeZero_symm_apply {c : G₀} (hc : c ≠ 0) :
+    ⇑(Homeomorph.smulOfNeZero c hc).symm = (c⁻¹ • · : α → α) :=
+  rfl
+
 theorem isOpenMap_smul₀ {c : G₀} (hc : c ≠ 0) : IsOpenMap fun x : α => c • x :=
   (Homeomorph.smulOfNeZero c hc).isOpenMap
 #align is_open_map_smul₀ isOpenMap_smul₀

Mathlib/Topology/Homeomorph.lean

@@ -121,6 +121,9 @@ theorem trans_apply (h₁ : α ≃ₜ β) (h₂ : β ≃ₜ γ) (a : α) : h₁.
   rfl
 #align homeomorph.trans_apply Homeomorph.trans_apply
 
+@[simp] theorem symm_trans_apply (f : α ≃ₜ β) (g : β ≃ₜ γ) (a : γ) :
+    (f.trans g).symm a = f.symm (g.symm a) := rfl
+
 @[simp]
 theorem homeomorph_mk_coe_symm (a : Equiv α β) (b c) :
     ((Homeomorph.mk a b c).symm : β → α) = a.symm :=

Mathlib/Topology/LocalHomeomorph.lean

@@ -411,10 +411,8 @@ theorem eventually_nhdsWithin (e : LocalHomeomorph α β) {x : α} (p : β → P
 theorem eventually_nhdsWithin' (e : LocalHomeomorph α β) {x : α} (p : α → Prop) {s : Set α}
     (hx : x ∈ e.source) : (∀ᶠ y in 𝓝[e.symm ⁻¹' s] e x, p (e.symm y)) ↔ ∀ᶠ x in 𝓝[s] x, p x := by
   rw [e.eventually_nhdsWithin _ hx]
-  refine'
-    eventually_congr
-      ((eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy =>
-        _)
+  refine eventually_congr <|
+    (eventually_nhdsWithin_of_eventually_nhds <| e.eventually_left_inverse hx).mono fun y hy => ?_
   rw [hy]
 #align local_homeomorph.eventually_nhds_within' LocalHomeomorph.eventually_nhdsWithin'
 
@@ -776,6 +774,7 @@ end
 
 /-- Composition of two local homeomorphisms when the target of the first and the source of
 the second coincide. -/
+@[simps! apply symm_apply toLocalEquiv, simps! (config := .lemmasOnly) source target]
 protected def trans' (h : e.target = e'.source) : LocalHomeomorph α γ where
   toLocalEquiv := LocalEquiv.trans' e.toLocalEquiv e'.toLocalEquiv h
   open_source := e.open_source