import deps open classical precedence `◆`: 55 structure my_group (G : Type*) := (mul : G → G → G) (infix `◆` := mul) (inv : G → G) (postfix `⁻¹` := inv) (e : G) (assoc : ∀ g h k : G, g ◆ (h ◆ k) = (g ◆ h) ◆ k) (e_mul : ∀ g, e ◆ g = g) (mul_e : ∀ g, g ◆ e = g) (mul_inv : ∀ g, g ◆ g⁻¹ = e) (inv_mul : ∀ g, g⁻¹ ◆ g = e) run_cmd print_name `my_group structure my_other_group (G : Type*) := (mul : G → G → G) (infix `◆` := mul) (assoc : ∀ g h k, g ◆ (h ◆ k) = (g ◆ h) ◆ k) (neutral : ∃ e, ∀ g, e ◆ g = g ∧ g ◆ e = g) (inv : let e := some neutral in ∀ g, ∃ h, g ◆ h = e ∧ h ◆ g = e)