awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'})
Hx :
  ∀ (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
z : ↥(closure {y})
⊢ Membership.mem (γ := Subgroup G') (closure {y}) y'

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

Tactic:
simp_rw [Subtype.forall, hyc, ← 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'})
Hx :
  ∀ (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
⊢ ∀ (z : ↥(closure {y})),
    Membership.mem (γ := Subgroup ↥(closure {y}))
      (zpowers (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯)) z

Tactic:
have Hy : ∀ (z : closure {y}), z ∈ zpowers ⟨y', by simp [hyc]⟩ := by
      simp_rw [Subtype.forall, hyc, ← zpowers_eq_closure, mem_zpowers_iff, Subtype.ext_iff,
        SubgroupClass.coe_zpow, imp_self, implies_true]
-- 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'})
Hx :
  ∀ (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
Hy :
  ∀ (z : ↥(closure {y})),
    Membership.mem (γ := Subgroup ↥(closure {y}))
      (zpowers (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯)) z
refine_1 :
  orderOf (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯) =
    orderOf (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯)
refine_2 :
  ∀ {a b : ↥(closure {x})}, (mulEquivOfOrderOfEq Hx Hy ⋯).toFun a ≤ (mulEquivOfOrderOfEq Hx Hy ⋯).toFun b ↔ a ≤ b
⊢ OrderMonoidIso.{u_1, u_2} ↥(closure {x}) ↥(closure {y})

Tactic:
refine OrderMonoidIso.mk (mulEquivOfOrderOfEq Hx Hy ?_) ?_

Premises used: mulEquivOfOrderOfEq, OrderMonoidIso.mk
-- 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'})
Hx :
  ∀ (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
Hy :
  ∀ (z : ↥(closure {y})),
    Membership.mem (γ := Subgroup ↥(closure {y}))
      (zpowers (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯)) z
refine_1 : orderOf x' = orderOf y'
⊢ orderOf (Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯) =
    orderOf (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯)

Tactic:
rw [orderOf_mk, orderOf_mk]

Premises used: Subgroup.orderOf_mk
-- 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'})
Hx :
  ∀ (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
Hy :
  ∀ (z : ↥(closure {y})),
    Membership.mem (γ := Subgroup ↥(closure {y}))
      (zpowers (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯)) z
⊢ orderOf x' = orderOf y'

Tactic:
grind [orderOf_eq_one_iff, IsMulTorsionFree.orderOf_le_one]

Premises used: IsMulTorsionFree.orderOf_le_one, orderOf_eq_one_iff
-- 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'})
Hx :
  ∀ (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
Hy :
  ∀ (z : ↥(closure {y})),
    Membership.mem (γ := Subgroup ↥(closure {y}))
      (zpowers (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯)) z
a b : ↥(closure {x})
refine_2 :
  ∀ (m : ℤ),
    (mulEquivOfOrderOfEq Hx Hy ⋯).toFun
          ((fun (x_1 : ℤ) ↦
              Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
            m) ≤
        (mulEquivOfOrderOfEq Hx Hy ⋯).toFun b ↔
      (fun (x_1 : ℤ) ↦ Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
          m ≤
        b
⊢ (mulEquivOfOrderOfEq Hx Hy ⋯).toFun a ≤ (mulEquivOfOrderOfEq Hx Hy ⋯).toFun b ↔ a ≤ b

Tactic:
obtain ⟨m, rfl⟩ := Hx a

Premises used: rfl
-- 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'})
Hx :
  ∀ (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
Hy :
  ∀ (z : ↥(closure {y})),
    Membership.mem (γ := Subgroup ↥(closure {y}))
      (zpowers (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯)) z
b : ↥(closure {x})
m : ℤ
refine_2 :
  ∀ (n : ℤ),
    (mulEquivOfOrderOfEq Hx Hy ⋯).toFun
          ((fun (x_1 : ℤ) ↦
              Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
            m) ≤
        (mulEquivOfOrderOfEq Hx Hy ⋯).toFun
          ((fun (x_1 : ℤ) ↦
              Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
            n) ↔
      LE.le.{u_1} (α := ↥(closure {x}))
        ((fun (x_1 : ℤ) ↦
            Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
          m)
        ((fun (x_1 : ℤ) ↦
            Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
          n)
⊢ (mulEquivOfOrderOfEq Hx Hy ⋯).toFun
        ((fun (x_1 : ℤ) ↦
            Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
          m) ≤
      (mulEquivOfOrderOfEq Hx Hy ⋯).toFun b ↔
    (fun (x_1 : ℤ) ↦ Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
        m ≤
      b

Tactic:
obtain ⟨n, rfl⟩ := Hx b

Premises used: rfl
-- 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'})
Hx :
  ∀ (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
Hy :
  ∀ (z : ↥(closure {y})),
    Membership.mem (γ := Subgroup ↥(closure {y}))
      (zpowers (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯)) z
m n : ℤ
refine_2 :
  Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯ ^ m ≤
      Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯ ^ n ↔
    Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯ ^ m ≤
      Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯ ^ n
⊢ (mulEquivOfOrderOfEq Hx Hy ⋯).toFun
        ((fun (x_1 : ℤ) ↦
            Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
          m) ≤
      (mulEquivOfOrderOfEq Hx Hy ⋯).toFun
        ((fun (x_1 : ℤ) ↦
            Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
          n) ↔
    LE.le.{u_1} (α := ↥(closure {x}))
      ((fun (x_1 : ℤ) ↦ Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
        m)
      ((fun (x_1 : ℤ) ↦ Subtype.mk (p := fun (x_2 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_2) x' ⋯ ^ x_1)
        n)

Tactic:
simp only [MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, map_zpow,
        mulEquivOfOrderOfEq_apply_gen]

Premises used: Equiv.toFun_as_coe, map_zpow, MulEquiv.toEquiv_eq_coe, mulEquivOfOrderOfEq_apply_gen, EquivLike.coe_coe
-- 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'})
Hx :
  ∀ (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
Hy :
  ∀ (z : ↥(closure {y})),
    Membership.mem (γ := Subgroup ↥(closure {y}))
      (zpowers (Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯)) z
m n : ℤ
⊢ Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯ ^ m ≤
      Subtype.mk (p := fun (x : G') ↦ Membership.mem (γ := Subgroup G') (closure {y}) x) y' ⋯ ^ n ↔
    Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯ ^ m ≤
      Subtype.mk (p := fun (x_1 : G) ↦ Membership.mem (γ := Subgroup G) (closure {x}) x_1) x' ⋯ ^ n

Tactic:
simp_all [zpow_le_zpow_iff_right, ← Subtype.coe_lt_coe]

Premises used: Subtype.coe_lt_coe, zpow_le_zpow_iff_right
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a b : G
mp : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b → b = |a|ₘ ∧ 1 < b
mpr : b = |a|ₘ ∧ 1 < b → IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
⊢ IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b ↔ b = |a|ₘ ∧ 1 < b

Tactic:
constructor
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a b : G
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
⊢ Eq (α := Subgroup G) (closure {a}) (closure {b})

Tactic:
have := Subgroup.cyclic_of_min h
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a b : G
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
this : Eq (α := Subgroup G) (closure {a}) (closure {b})
⊢ Membership.mem (γ := Subgroup G) (closure {b}) a

Tactic:
simp [← this]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a b : G
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
this : Eq (α := Subgroup G) (closure {a}) (closure {b})
⊢ Membership.mem (γ := Subgroup G) (closure {b}) a

Tactic:
have ha : a ∈ closure ({b} : Set G) := by
      simp [← this]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a b : G
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
this : Eq (α := Subgroup G) (closure {a}) (closure {b})
ha : Membership.mem (γ := Subgroup G) (closure {b}) a
⊢ ∃ (n : ℤ), b ^ n = a

Tactic:
rw [mem_closure_singleton] at ha

Premises used: Subgroup.mem_closure_singleton
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a b : G
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {a}) y ∧ 1 < y} b
this : Eq (α := Subgroup G) (closure {a}) (closure {b})
ha : ∃ (n : ℤ), b ^ n = a
mp :
  ∀ (n : ℤ) (h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b)
    (this : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})), b = |b ^ n|ₘ ∧ 1 < b
⊢ b = |a|ₘ ∧ 1 < b

Tactic:
obtain ⟨n, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
⊢ Membership.mem (γ := Set G) {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b

Tactic:
have := h.left
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : Membership.mem (γ := Set G) {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
⊢ (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b

Tactic:
simp only [mem_closure_singleton, mem_setOf_eq] at this

Premises used: Subgroup.mem_closure_singleton, Set.mem_setOf_eq
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
mp : ∀ (m : ℤ) (hm : (b ^ n) ^ m = b), b = |b ^ n|ₘ ∧ 1 < b
⊢ b = |b ^ n|ₘ ∧ 1 < b

Tactic:
obtain ⟨m, hm⟩ := this.left

Premises used: And.left
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
rw : b ^ (m * n) = HPow.hPow (β := ℤ) b 1
rw₁ : (b ^ n) ^ m = HPow.hPow (β := ℤ) b 1
rw₂ : b = HPow.hPow (β := ℤ) b 1
rw₃ rw₄ : b = b
⊢ m * n = 1

Tactic:
rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]

Premises used: zpow_right_inj, zpow_mul', zpow_one, And.right
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
⊢ m * n = 1

Tactic:
have key : m * n = 1 := by
      rw [← zpow_right_inj this.right, zpow_mul', hm, zpow_one]
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
key : m * n = 1
⊢ m = 1 ∧ n = 1 ∨ m = -1 ∧ n = -1

Tactic:
rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at key

Premises used: Int.mul_eq_one_iff_eq_one_or_neg_one
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
key : m = 1 ∧ n = 1 ∨ m = -1 ∧ n = -1
mp : |b ^ n|ₘ = b ∧ 1 < b
⊢ b = |b ^ n|ₘ ∧ 1 < b

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
n : ℤ
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {b ^ n}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {b ^ n}) (closure {b})
this : (∃ (n_1 : ℤ), (b ^ n) ^ n_1 = b) ∧ 1 < b
m : ℤ
hm : (b ^ n) ^ m = b
key : m = 1 ∧ n = 1 ∨ m = -1 ∧ n = -1
mp :
  ∀ (h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {HPow.hPow (β := ℤ) b 1}) y ∧ 1 < y} b)
    (this : Eq (α := Subgroup G) (closure {HPow.hPow (β := ℤ) b 1}) (closure {b}))
    (this : (∃ (n : ℤ), HPow.hPow (β := ℤ) b 1 ^ n = b) ∧ 1 < b)
    (hm : HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) b 1) 1 = b), |HPow.hPow (β := ℤ) b 1|ₘ = b ∧ 1 < b
mp₁ :
  ∀ (h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {HPow.hPow (β := ℤ) b (-1)}) y ∧ 1 < y} b)
    (this : Eq (α := Subgroup G) (closure {HPow.hPow (β := ℤ) b (-1)}) (closure {b}))
    (this : (∃ (n : ℤ), HPow.hPow (β := ℤ) b (-1) ^ n = b) ∧ 1 < b)
    (hm : HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) b (-1)) (-1) = b), |HPow.hPow (β := ℤ) b (-1)|ₘ = b ∧ 1 < b
⊢ |b ^ n|ₘ = b ∧ 1 < b

Tactic:
rcases key with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {HPow.hPow (β := ℤ) b 1}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {HPow.hPow (β := ℤ) b 1}) (closure {b})
this : (∃ (n : ℤ), HPow.hPow (β := ℤ) b 1 ^ n = b) ∧ 1 < b
hm : HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) b 1) 1 = b
⊢ |HPow.hPow (β := ℤ) b 1|ₘ = b ∧ 1 < b

Tactic:
simp [this.right.le, this.right, mabs]

Premises used: LT.lt.le, And.right, mabs
-- Module: Mathlib.GroupTheory.ArchimedeanDensely
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
b : G
h : IsLeast {y : G | Membership.mem (γ := Subgroup G) (closure {HPow.hPow (β := ℤ) b (-1)}) y ∧ 1 < y} b
this_1 : Eq (α := Subgroup G) (closure {HPow.hPow (β := ℤ) b (-1)}) (closure {b})
this : (∃ (n : ℤ), HPow.hPow (β := ℤ) b (-1) ^ n = b) ∧ 1 < b
hm : HPow.hPow (β := ℤ) (HPow.hPow (β := ℤ) b (-1)) (-1) = b
⊢ |HPow.hPow (β := ℤ) b (-1)|ₘ = b ∧ 1 < b

Tactic:
simp [this.right.le, this.right, mabs]

Premises used: LT.lt.le, And.right, mabs