∀ {G : Type u_1} {G' : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedMonoid G]
  [inst_3 : CommGroup G'] [inst_4 : LinearOrder G'] [inst_5 : IsOrderedMonoid G'] (x : G) (y : G')
  (hxy : x = 1 ↔ y = 1),
  LinearOrderedCommGroup.closure_equiv_closure x y hxy =
    if hx : x = 1 then
      { toFun := fun x_1 => ⟨1, ⋯⟩, invFun := fun x_1 => ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
        map_le_map_iff' := ⋯ }
    else
      let x' := max x x⁻¹;
      have hx' := ⋯;
      have xpos := ⋯;
      let y' := max y y⁻¹;
      have hy' := ⋯;
      have ypos := ⋯;
      have hxc := ⋯;
      have hyc := ⋯;
      { toFun := fun a => ⟨y' ^ ⋯.choose, ⋯⟩, invFun := fun a => ⟨x' ^ ⋯.choose, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯, map_le_map_iff' := ⋯ }