Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ Function.LeftInverse (fun x_1 ↦ ⟨1, ⋯⟩) fun x_1 ↦ ⟨1, ⋯⟩

pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ Function.RightInverse (fun x_1 ↦ ⟨1, ⋯⟩) fun x_1 ↦ ⟨1, ⋯⟩

pp: case refine_3
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ ∀ (x_1 y_1 : ↥(closure {x})),
    { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ?refine_1, right_inv := ?refine_2 }.toFun
        (x_1 * y_1) =
      { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ?refine_1, right_inv := ?refine_2 }.toFun
          x_1 *
        { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ?refine_1, right_inv := ?refine_2 }.toFun
          y_1

pp: case refine_4
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ ∀ {a b : ↥(closure {x})},
    { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ?refine_1, right_inv := ?refine_2,
              map_mul' := ?refine_3 }.toFun
          a ≤
        { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ?refine_1, right_inv := ?refine_2,
              map_mul' := ?refine_3 }.toFun
          b ↔
      a ≤ b

Tactic:
· intro ⟨a, ha⟩
      simpa [hx, closure_singleton_one, eq_comm] using ha

Goal state after:
case refine_2
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ Function.RightInverse (fun x_1 ↦ ⟨1, ⋯⟩) fun x_1 ↦ ⟨1, ⋯⟩

case refine_3
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ ∀ (x_1 y_1 : ↥(closure {x})),
    { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ?refine_2 }.toFun (x_1 * y_1) =
      { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ?refine_2 }.toFun x_1 *
        { toFun := fun x_2 ↦ ⟨1, ⋯⟩, invFun := fun x_2 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ?refine_2 }.toFun y_1

case refine_4
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ ∀ {a b : ↥(closure {x})},
    { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ?refine_2,
              map_mul' := ?refine_3 }.toFun
          a ≤
        { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ?refine_2,
              map_mul' := ?refine_3 }.toFun
          b ↔
      a ≤ b