How can I get a more natural way to write right cosets?

Stream: mathlib4

[ZHAO Jinxiang]

Suppose that $H$ is a normal subgroup of the group $G$. Prove that $H ⊆ g⁻¹ H g$.

import Mathlib.Algebra.Group.Basic
import Mathlib.Tactic

open scoped Pointwise

example {G : Type*} [Group G] (H : Subgroup G) (h : H.Normal) (g : G):
    (↑H : Set G) ⊆ (MulOpposite.op g • (g⁻¹ • H)) := by
  intro x hx
  -- by definition of normal subgroup, we have $g * x * g⁻¹ ∈ H$.
  replace h := h.conj_mem _ hx g
  use x * g⁻¹
  apply And.intro
  · show x * g⁻¹ ∈ (g⁻¹ • ↑H : Set G)
    rw [mem_leftCoset_iff]
    simpa [←mul_assoc] using h
  · simp

In this example, we need to write MulOpposite.op, but in math we write g⁻¹ H g. Is there a way to write this while keeping the order of the elements in math?

Also, does $g⁻¹ H g$ have any special meaning? Is this called the conjugation of $H$ with respect to $g$?

[ZHAO Jinxiang]

It seems that mathlib3 has same element order in right coset, but mathlib4 not

https://leanprover-community.github.io/mathlib_docs/group_theory/coset.html
https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Coset/Basic.html

[Eric Wieser]

You can use open scope RightActions and then H <• g