awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : a < 1
b : α
hab : a < b
hb : b < 1
inl : ∀ (k : ℤ) (hab : a < (fun (x : ℤ) ↦ a ^ x) k) (hb : LT.lt.{u_1} (α := α) ((fun (x : ℤ) ↦ a ^ x) k) 1), False
⊢ False

Tactic:
rcases ha b with ⟨k, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun (x : ℤ) ↦ a ^ x) k
hb : LT.lt.{u_1} (α := α) ((fun (x : ℤ) ↦ a ^ x) k) 1
this : 0 < k ∧ k < 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun (x : ℤ) ↦ a ^ x) k
hb : LT.lt.{u_1} (α := α) ((fun (x : ℤ) ↦ a ^ x) k) 1
inl : 0 < k ∧ k < 1
⊢ False

Tactic:
suffices 0 < k ∧ k < 1 by lia
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : a < 1
k : ℤ
hab : a < (fun (x : ℤ) ↦ a ^ x) k
hb : LT.lt.{u_1} (α := α) ((fun (x : ℤ) ↦ a ^ x) k) 1
inl :
  ∀ (hlt : 1 < a⁻¹) (k : ℤ) (hab : a < (fun (x : ℤ) ↦ a ^ x) k) (hb : LT.lt.{u_1} (α := α) ((fun (x : ℤ) ↦ a ^ x) k) 1),
    0 < k ∧ k < 1
⊢ 0 < k ∧ k < 1

Tactic:
rw [← one_lt_inv'] at hlt

Premises used: one_lt_inv'
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun (x : ℤ) ↦ a ^ x) k
hb : LT.lt.{u_1} (α := α) ((fun (x : ℤ) ↦ a ^ x) k) 1
inl : HPow.hPow (β := ℤ) a⁻¹ 0 < a⁻¹ ^ k ∧ a⁻¹ ^ k < HPow.hPow (β := ℤ) a⁻¹ 1
⊢ 0 < k ∧ k < 1

Tactic:
simp_rw [← zpow_lt_zpow_iff_right hlt]

Premises used: zpow_lt_zpow_iff_right
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : 1 < a⁻¹
k : ℤ
hab : a < (fun (x : ℤ) ↦ a ^ x) k
hb : LT.lt.{u_1} (α := α) ((fun (x : ℤ) ↦ a ^ x) k) 1
⊢ HPow.hPow (β := ℤ) a⁻¹ 0 < a⁻¹ ^ k ∧ a⁻¹ ^ k < HPow.hPow (β := ℤ) a⁻¹ 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ HPow.hPow (α := α) 1 x
inr : ∀ (b : α) (hb : b ≠ 1), False
⊢ False

Tactic:
rcases exists_ne (1 : α) with ⟨b, hb⟩

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ HPow.hPow (α := α) 1 x
b : α
hb : b ≠ 1
⊢ False

Tactic:
simpa [hb.symm] using ha b

Premises used: Ne.symm
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : 1 < a
inr : ∀ (b : α) (hb : 1 < b) (hba : b < a), False
⊢ False

Tactic:
rcases exists_between hlt with ⟨b, hb, hba⟩

Premises used: exists_between
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : 1 < a
b : α
hb : 1 < b
hba : b < a
inr : ∀ (k : ℤ) (hb : LT.lt.{u_1} (α := α) 1 ((fun (x : ℤ) ↦ a ^ x) k)) (hba : (fun (x : ℤ) ↦ a ^ x) k < a), False
⊢ False

Tactic:
rcases ha b with ⟨k, rfl⟩

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : LT.lt.{u_1} (α := α) 1 ((fun (x : ℤ) ↦ a ^ x) k)
hba : (fun (x : ℤ) ↦ a ^ x) k < a
this : 0 < k ∧ k < 1
⊢ False

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : LT.lt.{u_1} (α := α) 1 ((fun (x : ℤ) ↦ a ^ x) k)
hba : (fun (x : ℤ) ↦ a ^ x) k < a
inr : 0 < k ∧ k < 1
⊢ False

Tactic:
suffices 0 < k ∧ k < 1 by lia
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : LT.lt.{u_1} (α := α) 1 ((fun (x : ℤ) ↦ a ^ x) k)
hba : (fun (x : ℤ) ↦ a ^ x) k < a
inr : HPow.hPow (β := ℤ) a 0 < a ^ k ∧ a ^ k < HPow.hPow (β := ℤ) a 1
⊢ 0 < k ∧ k < 1

Tactic:
simp_rw [← zpow_lt_zpow_iff_right hlt]

Premises used: zpow_lt_zpow_iff_right
-- Module: Mathlib.Algebra.Order.Group.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
h : IsCyclic α
a : α
ha : Surjective.{1, u_1 + 1} (β := α) fun (x : ℤ) ↦ a ^ x
hlt : 1 < a
k : ℤ
hb : LT.lt.{u_1} (α := α) 1 ((fun (x : ℤ) ↦ a ^ x) k)
hba : (fun (x : ℤ) ↦ a ^ x) k < a
⊢ HPow.hPow (β := ℤ) a 0 < a ^ k ∧ a ^ k < HPow.hPow (β := ℤ) a 1

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Group.Bounds
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
s : Set α
a ε : α
h : IsGLB s a
hε : 0 < ε
⊢ ∃ b ∈ s, a ≤ b ∧ b < a + ε

Tactic:
h.exists_between <| lt_add_of_pos_right _ hε

Premises used: lt_add_of_pos_right, IsGLB.exists_between
-- Module: Mathlib.Algebra.Order.Group.Bounds
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
s : Set α
a ε : α
h : IsGLB s a
h₂ : a ∉ s
hε : 0 < ε
⊢ ∃ b ∈ s, a < b ∧ b < a + ε

Tactic:
h.exists_between' h₂ <| lt_add_of_pos_right _ hε

Premises used: lt_add_of_pos_right, IsGLB.exists_between'
-- Module: Mathlib.Algebra.Order.Group.Bounds
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
s : Set α
a ε : α
h : IsLUB s a
hε : 0 < ε
⊢ ∃ b ∈ s, a - ε < b ∧ b ≤ a

Tactic:
h.exists_between <| sub_lt_self _ hε

Premises used: sub_lt_self, IsLUB.exists_between
-- Module: Mathlib.Algebra.Order.Group.Bounds
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
s : Set α
a ε : α
h : IsLUB s a
h₂ : a ∉ s
hε : 0 < ε
⊢ ∃ b ∈ s, a - ε < b ∧ b < a

Tactic:
h.exists_between' h₂ <| sub_lt_self _ hε

Premises used: IsLUB.exists_between', sub_lt_self
-- Module: Mathlib.Algebra.Order.Group.CompleteLattice
Goal:
ι : Type u_1
G : Type u_2
inst : Group G
inst_1 : ConditionallyCompleteLattice G
inst_2 : Nonempty ι
f : ι → G
inst_3 : MulRightMono G
hf : BddAbove (range f)
a : G
⊢ (⨆ (i : ι), f i) * a = ⨆ (i : ι), f i * a

Tactic:
(OrderIso.mulRight a).map_ciSup hf

Premises used: OrderIso.map_ciSup, OrderIso.mulRight
-- Module: Mathlib.Algebra.Order.Group.CompleteLattice
Goal:
ι : Type u_1
G : Type u_2
inst : Group G
inst_1 : ConditionallyCompleteLattice G
inst_2 : Nonempty ι
f : ι → G
inst_3 : MulRightMono G
hf : BddAbove (range f)
a : G
⊢ (⨆ (i : ι), f i) / a = ⨆ (i : ι), f i / a

Tactic:
simp only [div_eq_mul_inv, ciSup_mul hf]

Premises used: ciSup_mul, div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.CompleteLattice
Goal:
ι : Type u_1
G : Type u_2
inst : Group G
inst_1 : ConditionallyCompleteLattice G
inst_2 : Nonempty ι
f : ι → G
inst_3 : MulRightMono G
hf : BddBelow (range f)
a : G
⊢ (⨅ (i : ι), f i) * a = ⨅ (i : ι), f i * a

Tactic:
(OrderIso.mulRight a).map_ciInf hf

Premises used: OrderIso.map_ciInf, OrderIso.mulRight
-- Module: Mathlib.Algebra.Order.Group.CompleteLattice
Goal:
ι : Type u_1
G : Type u_2
inst : Group G
inst_1 : ConditionallyCompleteLattice G
inst_2 : Nonempty ι
f : ι → G
inst_3 : MulRightMono G
hf : BddBelow (range f)
a : G
⊢ (⨅ (i : ι), f i) / a = ⨅ (i : ι), f i / a

Tactic:
simp only [div_eq_mul_inv, ciInf_mul hf]

Premises used: ciInf_mul, div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.CompleteLattice
Goal:
ι : Type u_1
G : Type u_2
inst : Group G
inst_1 : ConditionallyCompleteLattice G
inst_2 : Nonempty ι
f : ι → G
inst_3 : MulLeftMono G
hf : BddAbove (range f)
a : G
⊢ a * ⨆ (i : ι), f i = ⨆ (i : ι), a * f i

Tactic:
(OrderIso.mulLeft a).map_ciSup hf

Premises used: OrderIso.mulLeft, OrderIso.map_ciSup
-- Module: Mathlib.Algebra.Order.Group.CompleteLattice
Goal:
ι : Type u_1
G : Type u_2
inst : Group G
inst_1 : ConditionallyCompleteLattice G
inst_2 : Nonempty ι
f : ι → G
inst_3 : MulLeftMono G
hf : BddBelow (range f)
a : G
⊢ a * ⨅ (i : ι), f i = ⨅ (i : ι), a * f i

Tactic:
(OrderIso.mulLeft a).map_ciInf hf

Premises used: OrderIso.mulLeft, OrderIso.map_ciInf
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
G : Type u_1
inst : CommGroup G
p q : GroupCone G
h : Eq.{u_1 + 1} (α := Set G) ((fun (C : GroupCone G) ↦ C.carrier) p) ((fun (C : GroupCone G) ↦ C.carrier) q)
mk :
  ∀ (toSubmonoid : Submonoid G)
    (eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1)
    (h :
      Eq.{u_1 + 1} (α := Set G)
        ((fun (C : GroupCone G) ↦ C.carrier)
          { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' })
        ((fun (C : GroupCone G) ↦ C.carrier) q)),
    { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' : GroupCone G } = q
⊢ p = q

Tactic:
cases p
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
G : Type u_1
inst : CommGroup G
q : GroupCone G
toSubmonoid : Submonoid G
eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1
h :
  Eq.{u_1 + 1} (α := Set G)
    ((fun (C : GroupCone G) ↦ C.carrier)
      { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' })
    ((fun (C : GroupCone G) ↦ C.carrier) q)
mk :
  ∀ (toSubmonoid_1 : Submonoid G)
    (eq_one_of_mem_of_inv_mem'_1 : ∀ {a : G}, a ∈ toSubmonoid_1.carrier → a⁻¹ ∈ toSubmonoid_1.carrier → a = 1)
    (h :
      Eq.{u_1 + 1} (α := Set G)
        ((fun (C : GroupCone G) ↦ C.carrier)
          { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' })
        ((fun (C : GroupCone G) ↦ C.carrier)
          { toSubmonoid := toSubmonoid_1, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem'_1 })),
    { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' : GroupCone G } =
      { toSubmonoid := toSubmonoid_1, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem'_1 }
⊢ { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' : GroupCone G } = q

Tactic:
cases q
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
G : Type u_1
inst : CommGroup G
toSubmonoid : Submonoid G
eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1
toSubmonoid_1 : Submonoid G
eq_one_of_mem_of_inv_mem'_1 : ∀ {a : G}, a ∈ toSubmonoid_1.carrier → a⁻¹ ∈ toSubmonoid_1.carrier → a = 1
h :
  Eq.{u_1 + 1} (α := Set G)
    ((fun (C : GroupCone G) ↦ C.carrier)
      { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' })
    ((fun (C : GroupCone G) ↦ C.carrier)
      { toSubmonoid := toSubmonoid_1, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem'_1 })
mk : toSubmonoid = toSubmonoid_1
⊢ { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' : GroupCone G } =
    { toSubmonoid := toSubmonoid_1, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
G : Type u_1
inst : CommGroup G
toSubmonoid : Submonoid G
eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1
toSubmonoid_1 : Submonoid G
eq_one_of_mem_of_inv_mem'_1 : ∀ {a : G}, a ∈ toSubmonoid_1.carrier → a⁻¹ ∈ toSubmonoid_1.carrier → a = 1
h :
  Eq.{u_1 + 1} (α := Set G)
    ((fun (C : GroupCone G) ↦ C.carrier)
      { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' })
    ((fun (C : GroupCone G) ↦ C.carrier)
      { toSubmonoid := toSubmonoid_1, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem'_1 })
⊢ toSubmonoid = toSubmonoid_1

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
G : Type u_1
inst : CommGroup G
toSubmonoid : Submonoid G
eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1
toSubmonoid_1 : Submonoid G
eq_one_of_mem_of_inv_mem'_1 : ∀ {a : G}, a ∈ toSubmonoid_1.carrier → a⁻¹ ∈ toSubmonoid_1.carrier → a = 1
h :
  Eq.{u_1 + 1} (α := Set G)
    ((fun (C : GroupCone G) ↦ C.carrier)
      { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' })
    ((fun (C : GroupCone G) ↦ C.carrier)
      { toSubmonoid := toSubmonoid_1, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem'_1 })
⊢ toSubmonoid = toSubmonoid_1

Tactic:
exact SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
H : Type u_1
inst : CommGroup H
inst_1 : PartialOrder H
inst_2 : IsOrderedMonoid H
a_1 a : H
⊢ a ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (Submonoid.oneLE H)) →
    a⁻¹ ∈ Subsemigroup.carrier (Submonoid.toSubsemigroup (Submonoid.oneLE H)) → a = 1

Tactic:
simpa using ge_antisymm

Premises used: ge_antisymm
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
H : Type u_1
inst : CommGroup H
inst_1 : PartialOrder H
inst_2 : IsOrderedMonoid H
⊢ Eq (α := Submonoid H) (toSubmonoid (oneLE H)) (Submonoid.oneLE H)

Tactic:
rfl

Premises used: Submonoid.oneLE, rfl
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
H : Type u_1
inst : CommGroup H
inst_1 : PartialOrder H
inst_2 : IsOrderedMonoid H
a : H
⊢ Membership.mem (γ := GroupCone H) (oneLE H) a ↔ 1 ≤ a

Tactic:
Iff.rfl

Premises used: Set.Ici, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
H : Type u_1
inst : CommGroup H
inst_1 : PartialOrder H
inst_2 : IsOrderedMonoid H
⊢ (↑(oneLE H) : Set H) = {x : H | 1 ≤ x}

Tactic:
rfl

Premises used: Set.Ici, setOf, rfl
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
H_1 : Type u_1
inst : CommGroup H_1
inst_1 : PartialOrder H_1
inst_2 : IsOrderedMonoid H_1
a : H_1
H : Type u_2
inst_3 : CommGroup H
inst_4 : LinearOrder H
inst_5 : IsOrderedMonoid H
⊢ ∀ (a : H), Membership.mem (γ := GroupCone H) (oneLE H) a ∨ Membership.mem (γ := GroupCone H) (oneLE H) a⁻¹

Tactic:
simpa using le_total 1

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
S : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : SetLike S G
C : S
inst_2 : GroupConeClass S G
a : G
⊢ a / a ∈ C

Tactic:
simp [one_mem]

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
S : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : SetLike S G
C : S
inst_2 : GroupConeClass S G
a b c : G
nab : b / a ∈ C
nbc : c / b ∈ C
⊢ c / a ∈ C

Tactic:
simpa using mul_mem nbc nab

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
S : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : SetLike S G
C : S
inst_2 : GroupConeClass S G
a b : G
nab : b / a ∈ C
nba : a / b ∈ C
⊢ (b / a)⁻¹ ∈ C

Tactic:
simpa using nba
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
S : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : SetLike S G
C : S
inst_2 : GroupConeClass S G
a b : G
nab : b / a ∈ C
nba : a / b ∈ C
⊢ a = b

Tactic:
simpa [div_eq_one, eq_comm] using eq_one_of_mem_of_inv_mem nab (by simpa using nba)

Premises used: eq_comm, div_eq_one, GroupConeClass.eq_one_of_mem_of_inv_mem
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
S : Type u_3
G : Type u_4
inst : CommGroup G
inst_1 : SetLike S G
inst_2 : GroupConeClass S G
C : S
a b : G
⊢ a ≤ b ↔ b / a ∈ C

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
S : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : SetLike S G
C : S
inst_2 : GroupConeClass S G
inst_3 : HasMemOrInvMem C
inst_4 : DecidablePred fun (x : G) ↦ x ∈ C
a b : G
⊢ a ≤ b ∨ b ≤ a

Tactic:
simpa using mem_or_inv_mem C (b / a)

Premises used: HasMemOrInvMem.mem_or_inv_mem, HDiv.hDiv
-- Module: Mathlib.Algebra.Order.Group.Cone
Goal:
S : Type u_1
G : Type u_2
inst : CommGroup G
inst_1 : SetLike S G
C : S
inst_2 : GroupConeClass S G
x : PartialOrder G := PartialOrder.mkOfGroupCone C
a b : G
nab : a ≤ b
c : G
⊢ a * c ≤ b * c

Tactic:
simpa [· ≤ ·] using nab
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
obtain : ∀ (a : G) (ha : Subgroup.zpowers a = H), ∃ a < 1, Subgroup.zpowers a = H
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
obtain ⟨a, ha⟩ := H.isCyclic_iff_exists_zpowers_eq_top.mp hH

Premises used: Iff.mp, Subgroup.isCyclic_iff_exists_zpowers_eq_top
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
a : G
ha : Subgroup.zpowers a = H
inl : ∀ (ha1 : a < 1), ∃ a < 1, Subgroup.zpowers a = H
inr : ∀ (ha : Subgroup.zpowers 1 = H), ∃ a < 1, Subgroup.zpowers a = H
inr₁ : ∀ (ha1 : 1 < a), ∃ a < 1, Subgroup.zpowers a = H
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
obtain ha1 | rfl | ha1 := lt_trichotomy a 1

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
a : G
ha : Subgroup.zpowers a = H
ha1 : a < 1
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
⟨a, ha1, ha⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
a : G
ha : Subgroup.zpowers a = H
ha1 : a < 1
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
exact ⟨a, ha1, ha⟩
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
ha : Subgroup.zpowers 1 = H
⊢ ⊥ = H

Tactic:
rw [Subgroup.zpowers_one_eq_bot] at ha

Premises used: Subgroup.zpowers_one_eq_bot
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
ha : ⊥ = H
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
absurd ha.symm <| (H.nontrivial_iff_ne_bot).mp inferInstance

Premises used: inferInstance, absurd, Iff.mp, Eq.symm, Subgroup.nontrivial_iff_ne_bot
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
ha : ⊥ = H
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
exact absurd ha.symm <| (H.nontrivial_iff_ne_bot).mp inferInstance

Premises used: inferInstance, absurd, Iff.mp, Eq.symm, Subgroup.nontrivial_iff_ne_bot
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
a : G
ha : Subgroup.zpowers a = H
ha1 : 1 < a
right : Subgroup.zpowers a⁻¹ = H
⊢ ∃ a < 1, Subgroup.zpowers a = H

Tactic:
use a⁻¹, Left.inv_lt_one_iff.mpr ha1

Premises used: Iff.mpr, Left.inv_lt_one_iff
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
a : G
ha : Subgroup.zpowers a = H
ha1 : 1 < a
right : Subgroup.zpowers a = H
right₁ right₂ : H = H
⊢ Subgroup.zpowers a⁻¹ = H

Tactic:
rw [Subgroup.zpowers_inv, ha]

Premises used: Subgroup.zpowers_inv
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
⊢ Subgroup.genLTOne H < 1

Tactic:
H.exists_generator_lt_one.choose_spec.1

Premises used: Exists.choose_spec, LinearOrderedCommGroup.Subgroup.genLTOne, And.left, LinearOrderedCommGroup.Subgroup.exists_generator_lt_one
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
⊢ Subgroup.zpowers (Subgroup.genLTOne H) = H

Tactic:
H.exists_generator_lt_one.choose_spec.2

Premises used: Exists.choose_spec, LinearOrderedCommGroup.Subgroup.genLTOne, And.right, LinearOrderedCommGroup.Subgroup.exists_generator_lt_one
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
nth_rewrite : Membership.mem (γ := Subgroup G) (Subgroup.zpowers (Subgroup.genLTOne H)) (Subgroup.genLTOne H)
⊢ Subgroup.genLTOne H ∈ H

Tactic:
nth_rewrite 1 [← H.genLTOne_zpowers_eq_top]

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_eq_top
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
⊢ Membership.mem (γ := Subgroup G) (Subgroup.zpowers (Subgroup.genLTOne H)) (Subgroup.genLTOne H)

Tactic:
Subgroup.mem_zpowers (Subgroup.genLTOne H)

Premises used: Subgroup.mem_zpowers, LinearOrderedCommGroup.Subgroup.genLTOne
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH : IsCyclic.{u_1} ↥H
⊢ Membership.mem (γ := Subgroup G) (Subgroup.zpowers (Subgroup.genLTOne H)) (Subgroup.genLTOne H)

Tactic:
exact Subgroup.mem_zpowers (Subgroup.genLTOne H)

Premises used: Subgroup.mem_zpowers, LinearOrderedCommGroup.Subgroup.genLTOne
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH_1 : IsCyclic.{u_1} ↥H
g : G
hg : g < 1
hH : Subgroup.zpowers g = H
⊢ ¬IsOfFinOrder g

Tactic:
have hg' : ¬ IsOfFinOrder g := not_isOfFinOrder_of_isMulTorsionFree (ne_of_lt hg)
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
H : Subgroup G
inst_3 : Nontrivial.{u_1} ↥H
hH_1 : IsCyclic.{u_1} ↥H
g : G
hg : g < 1
hH : Subgroup.zpowers g = H
hg' : ¬IsOfFinOrder g
⊢ Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))

Tactic:
rw [← H.genLTOne_zpowers_eq_top] at hH

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne_zpowers_eq_top