-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
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
hx : x = 1
refine_1 :
  Function.LeftInverse
    (fun (x_1 : ↥(closure {y})) ↦
      Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) 1 ⋯)
    fun (x_1 : ↥(closure {x})) ↦ Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) 1 ⋯
refine_2 :
  Function.RightInverse
    (fun (x_1 : ↥(closure {y})) ↦
      Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) 1 ⋯)
    fun (x_1 : ↥(closure {x})) ↦ Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) 1 ⋯
refine_3 :
  ∀ (x_1 y_1 : ↥(closure {x})),
    Equiv.toFun
        {
          toFun := fun (x_2 : ↥(closure {x})) ↦
            Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) 1 ⋯,
          invFun := fun (x_2 : ↥(closure {y})) ↦
            Subtype.mk (p := fun (x_3 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_3) 1 ⋯,
          left_inv := ⋯, right_inv := ⋯ }
        (x_1 * y_1) =
      HMul.hMul (α := ↥(closure {y}))
        (Equiv.toFun
          {
            toFun := fun (x_2 : ↥(closure {x})) ↦
              Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) 1 ⋯,
            invFun := fun (x_2 : ↥(closure {y})) ↦
              Subtype.mk (p := fun (x_3 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_3) 1 ⋯,
            left_inv := ⋯, right_inv := ⋯ : Equiv.{u_1 + 1, u_2 + 1} ↥(closure {x}) ↥(closure {y}) }
          x_1)
        (Equiv.toFun
          {
            toFun := fun (x_2 : ↥(closure {x})) ↦
              Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) 1 ⋯,
            invFun := fun (x_2 : ↥(closure {y})) ↦
              Subtype.mk (p := fun (x_3 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_3) 1 ⋯,
            left_inv := ⋯, right_inv := ⋯ : Equiv.{u_1 + 1, u_2 + 1} ↥(closure {x}) ↥(closure {y}) }
          y_1)
refine_4 :
  ∀ {a b : ↥(closure {x})},
    LE.le.{u_2} (α := ↥(closure {y}))
        (Equiv.toFun
          (MulEquiv.toEquiv
            {
              toFun := fun (x_1 : ↥(closure {x})) ↦
                Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) 1 ⋯,
              invFun := fun (x_1 : ↥(closure {y})) ↦
                Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) 1 ⋯,
              left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          a)
        (Equiv.toFun
          (MulEquiv.toEquiv
            {
              toFun := fun (x_1 : ↥(closure {x})) ↦
                Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) 1 ⋯,
              invFun := fun (x_1 : ↥(closure {y})) ↦
                Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) 1 ⋯,
              left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
          b) ↔
      a ≤ b
⊢ OrderMonoidIso.{u_1, u_2} ↥(closure {x}) ↥(closure {y})

Tactic:
refine ⟨⟨⟨fun _ ↦ ⟨1, by simp [hxy.mp hx]⟩, fun _ ↦ ⟨1, by simp [hx]⟩, ?_, ?_⟩, ?_⟩, ?_⟩