awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤ
H : Eq (α := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ) (-1 : ℤ)
⊢ LT.lt (α := ℤ) 0 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤ
H : Eq (α := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ) (-1 : ℤ)
⊢ LT.lt (α := ℤ) (0 : ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ)

Tactic:
have h1 : 0 < e 1 := by
        rw [← map_zero e, map_lt_map_iff]
        simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤ
H : Eq (α := ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ) (-1 : ℤ)
h1 : LT.lt (α := ℤ) (0 : ℤ) ((e : (a : ℤ) → ℤ) 1 : ℤ)
⊢ False

Tactic:
simp [H] at h1
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
⊢ ∀ {a b : ℤ},
    (AddEquiv.toEquiv (AddEquiv.trans (AddEquiv.neg ℤ) { toEquiv := toDual, map_add' := ⋯ : ℤ ≃+ ℤᵒᵈ })).toFun a ≤
        (AddEquiv.toEquiv (AddEquiv.trans (AddEquiv.neg ℤ) { toEquiv := toDual, map_add' := ⋯ : ℤ ≃+ ℤᵒᵈ })).toFun b ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤᵒᵈ
simp : Eq (α := ℤ ≃+ ℤᵒᵈ) (↑e : ℤ ≃+ ℤᵒᵈ) (AddEquiv.trans (AddEquiv.neg ℤ) { toEquiv := toDual, map_add' := ⋯ })
⊢ e.toAddEquiv =
    { toAddEquiv := AddEquiv.trans (AddEquiv.neg ℤ) { toEquiv := toDual, map_add' := ⋯ : ℤ ≃+ ℤᵒᵈ },
        map_le_map_iff' := @instUniqueOrderAddMonoidIsoIntOrderDual._proof_1 : ℤ ≃+o ℤᵒᵈ }.toAddEquiv

Tactic:
simp only [OrderAddMonoidIso.toAddEquiv_eq_coe]

Premises used: OrderAddMonoidIso.toAddEquiv_eq_coe
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤᵒᵈ
H : AddEquiv.trans (↑e : ℤ ≃+ ℤᵒᵈ) { toEquiv := toDual, map_add' := ⋯ : ℤᵒᵈ ≃+ ℤ } = AddEquiv.refl ℤ
⊢ Eq (α := ℤᵒᵈ) ((e : (a : ℤ) → ℤᵒᵈ) 1 : ℤᵒᵈ) (1 : ℤᵒᵈ)

Tactic:
replace H : e 1 = 1 := congr($H 1)
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤᵒᵈ
H : Eq (α := ℤᵒᵈ) ((e : (a : ℤ) → ℤᵒᵈ) 1 : ℤᵒᵈ) (1 : ℤᵒᵈ)
rw : LT.lt (α := ℤ) 0 1
⊢ LT.lt (α := ℤᵒᵈ) (0 : ℤᵒᵈ) ((e : (a : ℤ) → ℤᵒᵈ) 1 : ℤᵒᵈ)

Tactic:
rw [← map_zero e, map_lt_map_iff]

Premises used: map_zero, map_lt_map_iff
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤᵒᵈ
H : Eq (α := ℤᵒᵈ) ((e : (a : ℤ) → ℤᵒᵈ) 1 : ℤᵒᵈ) (1 : ℤᵒᵈ)
⊢ LT.lt (α := ℤ) 0 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤᵒᵈ
H : Eq (α := ℤᵒᵈ) ((e : (a : ℤ) → ℤᵒᵈ) 1 : ℤᵒᵈ) (1 : ℤᵒᵈ)
⊢ LT.lt (α := ℤᵒᵈ) (0 : ℤᵒᵈ) ((e : (a : ℤ) → ℤᵒᵈ) 1 : ℤᵒᵈ)

Tactic:
have h1 : 0 < e 1 := by
        rw [← map_zero e, map_lt_map_iff]
        simp
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤᵒᵈ
H : Eq (α := ℤᵒᵈ) ((e : (a : ℤ) → ℤᵒᵈ) 1 : ℤᵒᵈ) (1 : ℤᵒᵈ)
h1 : LT.lt (α := ℤᵒᵈ) (0 : ℤᵒᵈ) ((e : (a : ℤ) → ℤᵒᵈ) 1 : ℤᵒᵈ)
⊢ False

Tactic:
simp [H, ← ofDual_lt_ofDual] at h1

Premises used: OrderDual.ofDual_lt_ofDual
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
e : ℤ ≃+o ℤᵒᵈ
⊢ Eq (α := ℤ ≃+ ℤᵒᵈ) (↑e : ℤ ≃+ ℤᵒᵈ) (AddEquiv.trans (AddEquiv.neg ℤ) { toEquiv := toDual, map_add' := ⋯ })

Tactic:
refine Int.addEquiv_eq_refl_or_neg ((e : ℤ ≃+ ℤᵒᵈ).trans ⟨toDual, toDual_add⟩)
        |>.resolve_left fun H => by
      replace H : e 1 = 1 := congr($H 1)
      have h1 : 0 < e 1 := by
        rw [← map_zero e, map_lt_map_iff]
        simp
      simp [H, ← ofDual_lt_ofDual] at h1

Premises used: OrderDual.toDual, Int.addEquiv_eq_refl_or_neg, Or.resolve_left, AddEquivClass.toAddEquiv, AddEquiv.trans, AddEquiv.mk, toDual_add
-- 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
x_1 : ↥(closure {x})
⊢ Membership.mem (γ := Subgroup G') (closure {y}) 1

Tactic:
simp [hxy.mp hx]

Premises used: Iff.mp
-- 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
x_1 : ↥(closure {y})
⊢ Membership.mem (γ := Subgroup G) (closure {x}) 1

Tactic:
simp [hx]
-- 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
a : G
ha : Membership.mem (γ := Subgroup G) (closure {x}) a
⊢ (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 ⋯)
        (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) a ha)) =
    Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) a ha

Tactic:
simpa [hx, closure_singleton_one, eq_comm] using ha

Premises used: Subgroup.closure_singleton_one, eq_comm
-- 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
a : G'
ha : Membership.mem (γ := Subgroup G') (closure {y}) a
⊢ (fun (x_1 : ↥(closure {x})) ↦ Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) 1 ⋯)
      ((fun (x_1 : ↥(closure {y})) ↦
          Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) 1 ⋯)
        (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) a ha)) =
    Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) a ha

Tactic:
simpa [hxy.mp hx, closure_singleton_one, eq_comm] using ha

Premises used: Subgroup.closure_singleton_one, eq_comm, Iff.mp
-- 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
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)

Tactic:
simp
-- 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
a : G
ha : Membership.mem (γ := Subgroup G) (closure {x}) a
refine_4 :
  ∀ (b : G) (hb : Membership.mem (γ := Subgroup G) (closure {x}) b),
    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' := ⋯ })
          (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) a ha))
        (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' := ⋯ })
          (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) b hb)) ↔
      Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) a ha ≤
        Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) b hb
⊢ ∀ {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' := ⋯ })
          (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) a ha))
        (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) ↔
      Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) a ha ≤ b

Tactic:
⟨b, hb⟩
-- 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
a : G
ha : Membership.mem (γ := Subgroup G) (closure {x}) a
b : G
hb : Membership.mem (γ := Subgroup G) (closure {x}) b
⊢ a = 1

Tactic:
simp only [hx, closure_singleton_one, mem_bot] at ha hb

Premises used: Subgroup.closure_singleton_one, Subgroup.mem_bot
-- 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
a : G
ha : Membership.mem (γ := Subgroup G) (closure {x}) a
b : G
hb : Membership.mem (γ := Subgroup G) (closure {x}) b
ha₁ : a = 1
⊢ b = 1

Tactic:
simp only [hx, closure_singleton_one, mem_bot] at ha hb

Premises used: Subgroup.closure_singleton_one, Subgroup.mem_bot
-- 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
a : G
ha_1 : Membership.mem (γ := Subgroup G) (closure {x}) a
b : G
hb_1 : Membership.mem (γ := Subgroup G) (closure {x}) b
ha : a = 1
hb : b = 1
⊢ 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' := ⋯ })
        (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) a ha_1))
      (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' := ⋯ })
        (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) b hb_1)) ↔
    Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) a ha_1 ≤
      Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) b hb_1

Tactic:
simp [ha, hb]
-- 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
⊢ let x' := max x x⁻¹;
  x' = max x x⁻¹

Tactic:
set x' := max x x⁻¹ with hx'

Premises used: Inv.inv, Max.max
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
⊢ 1 < x'

Tactic:
simp [hx', eq_comm, hx]

Premises used: eq_comm
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
⊢ 1 < x'

Tactic:
have xpos : 1 < x' := by
      simp [hx', eq_comm, hx]
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
⊢ let y' := max y y⁻¹;
  y' = max y y⁻¹

Tactic:
set y' := max y y⁻¹ with hy'

Premises used: Inv.inv, Max.max
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
⊢ 1 < y'

Tactic:
simp [hy', eq_comm, ← hxy, hx]

Premises used: eq_comm
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
⊢ 1 < y'

Tactic:
have ypos : 1 < y' := by
      simp [hy', eq_comm, ← hxy, hx]
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
inl : max x x⁻¹ = x ∧ x⁻¹ ≤ x → Eq (α := Subgroup G) (closure {x}) (closure {x'})
inr : max x x⁻¹ = x⁻¹ ∧ x < x⁻¹ → Eq (α := Subgroup G) (closure {x}) (closure {x'})
⊢ Eq (α := Subgroup G) (closure {x}) (closure {x'})

Tactic:
rcases max_cases x x⁻¹

Premises used: Inv.inv, max_cases
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
h : max x x⁻¹ = x ∧ x⁻¹ ≤ x
⊢ Eq (α := Subgroup G) (closure {x}) (closure {x'})

Tactic:
simp_all
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
h : max x x⁻¹ = x⁻¹ ∧ x < x⁻¹
⊢ Eq (α := Subgroup G) (closure {x}) (closure {x'})

Tactic:
simp_all
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
⊢ Eq (α := Subgroup G) (closure {x}) (closure {x'})

Tactic:
have hxc : closure {x} = closure {x'} := by rcases max_cases x x⁻¹ <;> simp_all
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : Eq (α := Subgroup G) (closure {x}) (closure {x'})
inl : max y y⁻¹ = y ∧ y⁻¹ ≤ y → Eq (α := Subgroup G') (closure {y}) (closure {y'})
inr : max y y⁻¹ = y⁻¹ ∧ y < y⁻¹ → Eq (α := Subgroup G') (closure {y}) (closure {y'})
⊢ Eq (α := Subgroup G') (closure {y}) (closure {y'})

Tactic:
rcases max_cases y y⁻¹

Premises used: Inv.inv, max_cases
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : Eq (α := Subgroup G) (closure {x}) (closure {x'})
h : max y y⁻¹ = y ∧ y⁻¹ ≤ y
⊢ Eq (α := Subgroup G') (closure {y}) (closure {y'})

Tactic:
simp_all
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : Eq (α := Subgroup G) (closure {x}) (closure {x'})
h : max y y⁻¹ = y⁻¹ ∧ y < y⁻¹
⊢ Eq (α := Subgroup G') (closure {y}) (closure {y'})

Tactic:
simp_all
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : Eq (α := Subgroup G) (closure {x}) (closure {x'})
⊢ Eq (α := Subgroup G') (closure {y}) (closure {y'})

Tactic:
have hyc : closure {y} = closure {y'} := by rcases max_cases y y⁻¹ <;> simp_all
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : Eq (α := Subgroup G) (closure {x}) (closure {x'})
hyc : Eq (α := Subgroup G') (closure {y}) (closure {y'})
z : ↥(closure {x})
⊢ Membership.mem (γ := Subgroup G) (closure {x}) x'

Tactic:
simp [hxc]
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : Eq (α := Subgroup G) (closure {x}) (closure {x'})
hyc : Eq (α := Subgroup G') (closure {y}) (closure {y'})
simp_rw :
  ∀ (a : G) (b : Membership.mem (γ := Subgroup G) (closure {x}) a),
    Membership.mem (γ := Subgroup ↥(closure {x}))
      (zpowers (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯))
      (Subtype.mk (p := fun (a : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) a) a b)
simp_rw₁ :
  ∀ (a : G) (b : Membership.mem (γ := Subgroup G) (closure {x'}) a),
    Membership.mem (γ := Subgroup ↥(closure {x}))
      (zpowers (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯))
      (Subtype.mk (p := fun (a : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) a) a ⋯)
simp_rw₂ :
  ∀ (a : G) (b : Membership.mem (γ := Subgroup G) (zpowers x') a),
    Membership.mem (γ := Subgroup ↥(closure {x}))
      (zpowers (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯))
      (Subtype.mk (p := fun (a : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) a) a ⋯)
simp_rw₃ :
  ∀ (a : G) (b : ∃ (k : ℤ), x' ^ k = a),
    ∃ (k : ℤ),
      Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯ ^ k =
        Subtype.mk (p := fun (a : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) a) a ⋯
simp_rw₄ :
  ∀ (a : G) (b : ∃ (k : ℤ), x' ^ k = a),
    ∃ (k : ℤ),
      (↑(Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯ ^ k) : G) = a
simp_rw₅ : ∀ (a : G) (b : ∃ (k : ℤ), x' ^ k = a), ∃ (k : ℤ), x' ^ k = a
simp_rw₆ : ∀ (a : G), True
⊢ ∀ (z : ↥(closure {x})),
    Membership.mem (γ := Subgroup ↥(closure {x}))
      (zpowers (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯)) z

Tactic:
simp_rw [Subtype.forall, hxc, ← zpowers_eq_closure, mem_zpowers_iff, Subtype.ext_iff,
        SubgroupClass.coe_zpow, imp_self, implies_true]

Premises used: SubgroupClass.coe_zpow, Subtype.forall, Subtype.ext_iff, imp_self, implies_true, Subgroup.mem_zpowers_iff, Subgroup.zpowers_eq_closure
-- 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
x' : G := max x x⁻¹
hx' : x' = max x x⁻¹
xpos : 1 < x'
y' : G' := max y y⁻¹
hy' : y' = max y y⁻¹
ypos : 1 < y'
hxc : Eq (α := Subgroup G) (closure {x}) (closure {x'})
hyc : Eq (α := Subgroup G') (closure {y}) (closure {y'})
⊢ ∀ (z : ↥(closure {x})),
    Membership.mem (γ := Subgroup ↥(closure {x}))
      (zpowers (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯)) z

Tactic:
have Hx : ∀ (z : closure {x}), z ∈ zpowers ⟨x', by simp [hxc]⟩ := by
      simp_rw [Subtype.forall, hxc, ← zpowers_eq_closure, mem_zpowers_iff, Subtype.ext_iff,
        SubgroupClass.coe_zpow, imp_self, implies_true]