awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hH₁ : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
⊢ ¬IsOfFinOrder g

Tactic:
rw [← H.genLTOne_zpowers_eq_top] at hH

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_1 : IsCyclic.{u_1} ↥H
g : G
hg : g < 1
hH : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
hg' : ¬IsOfFinOrder g
inl : g = Subgroup.genLTOne H → g = Subgroup.genLTOne H
inr : ∀ (h : g⁻¹ = Subgroup.genLTOne H), g = Subgroup.genLTOne H
⊢ g = Subgroup.genLTOne H

Tactic:
rcases (Subgroup.zpowers_eq_zpowers_iff hg').mp hH with _ | h

Premises used: Iff.mp, Subgroup.zpowers_eq_zpowers_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_1 : IsCyclic.{u_1} ↥H
g : G
hg : g < 1
hH : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
hg' : ¬IsOfFinOrder g
h : g = Subgroup.genLTOne H
⊢ g = Subgroup.genLTOne H

Tactic:
assumption
-- 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 : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
hg' : ¬IsOfFinOrder g
h : g⁻¹ = Subgroup.genLTOne H
⊢ 1 < Subgroup.genLTOne H

Tactic:
rw [← one_lt_inv', h] at hg

Premises used: one_lt_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_1 : IsCyclic.{u_1} ↥H
g : G
hg : g < 1
hH : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
hg' : ¬IsOfFinOrder g
h : g⁻¹ = Subgroup.genLTOne H
hg₁ : 1 < Subgroup.genLTOne H
⊢ Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))

Tactic:
rw [← one_lt_inv', h] at hg

Premises used: one_lt_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_1 : IsCyclic.{u_1} ↥H
g : G
hg : g < 1
hH : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
hg' : ¬IsOfFinOrder g
h : g⁻¹ = Subgroup.genLTOne H
hg₁ : 1 < Subgroup.genLTOne H
hH₁ : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
⊢ ¬IsOfFinOrder g

Tactic:
rw [← one_lt_inv', h] at hg

Premises used: one_lt_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_1 : IsCyclic.{u_1} ↥H
g : G
hg : g < 1
hH : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
hg' : ¬IsOfFinOrder g
h : g⁻¹ = Subgroup.genLTOne H
hg₁ : 1 < Subgroup.genLTOne H
hH₁ : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
hg'₁ : ¬IsOfFinOrder g
⊢ g⁻¹ = Subgroup.genLTOne H

Tactic:
rw [← one_lt_inv', h] at hg

Premises used: one_lt_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_1 : IsCyclic.{u_1} ↥H
g : G
hg : 1 < Subgroup.genLTOne H
hH : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
hg' : ¬IsOfFinOrder g
h : g⁻¹ = Subgroup.genLTOne H
⊢ g = Subgroup.genLTOne H

Tactic:
(not_lt_of_gt hg <| Subgroup.genLTOne_lt_one _).elim

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne_lt_one, False.elim, not_lt_of_gt
-- 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 : 1 < Subgroup.genLTOne H
hH : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
hg' : ¬IsOfFinOrder g
h : g⁻¹ = Subgroup.genLTOne H
⊢ g = Subgroup.genLTOne H

Tactic:
exact (not_lt_of_gt hg <| Subgroup.genLTOne_lt_one _).elim

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne_lt_one, False.elim, not_lt_of_gt
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
inl : ∀ (h' : Eq (α := Subgroup G) (Subgroup.zpowers g2) ⊥), g1 = g2
inr : ∀ (h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)), g1 = g2
⊢ g1 = g2

Tactic:
rcases (Subgroup.zpowers g2).bot_or_nontrivial with (h' | h')

Premises used: Subgroup.bot_or_nontrivial, Subgroup.zpowers
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Eq (α := Subgroup G) (Subgroup.zpowers g2) ⊥
⊢ Eq (α := Subgroup G) (Subgroup.zpowers g1) ⊥

Tactic:
rw [h'] at h
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Eq (α := Subgroup G) (Subgroup.zpowers g2) ⊥
h₁ : Eq (α := Subgroup G) (Subgroup.zpowers g1) ⊥
⊢ Eq (α := Subgroup G) (Subgroup.zpowers g2) ⊥

Tactic:
rw [h'] at h
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) ⊥
h' : Eq (α := Subgroup G) (Subgroup.zpowers g2) ⊥
⊢ g1 = g2

Tactic:
simp_all only [Subgroup.zpowers_eq_bot]

Premises used: Subgroup.zpowers_eq_bot
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
rw : ∃ (g : G), Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers g2)
⊢ IsCyclic.{u_1} ↥(Subgroup.zpowers g2)

Tactic:
rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]

Premises used: 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
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
w : G
h₁ : Eq (α := Subgroup G) (Subgroup.zpowers g2) (Subgroup.zpowers g2)
⊢ ∃ (g : G), Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers g2)

Tactic:
use g2
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
⊢ IsCyclic.{u_1} ↥(Subgroup.zpowers g2)

Tactic:
have h1 : IsCyclic ↥(Subgroup.zpowers g2) := by
      rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]; use g2
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
rw : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
⊢ Nontrivial.{u_1} ↥(Subgroup.zpowers g1)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
⊢ Nontrivial.{u_1} ↥(Subgroup.zpowers g2)

Tactic:
h'
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
⊢ Nontrivial.{u_1} ↥(Subgroup.zpowers g2)

Tactic:
exact h'
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
⊢ Nontrivial.{u_1} ↥(Subgroup.zpowers g1)

Tactic:
have h2 : Nontrivial ↥(Subgroup.zpowers g1) := by rw [h]; exact h'
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
h2 : Nontrivial.{u_1} ↥(Subgroup.zpowers g1)
rw : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
⊢ IsCyclic.{u_1} ↥(Subgroup.zpowers g1)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
h2 : Nontrivial.{u_1} ↥(Subgroup.zpowers g1)
⊢ IsCyclic.{u_1} ↥(Subgroup.zpowers g2)

Tactic:
h1
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
h2 : Nontrivial.{u_1} ↥(Subgroup.zpowers g1)
⊢ IsCyclic.{u_1} ↥(Subgroup.zpowers g2)

Tactic:
exact h1
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
h2 : Nontrivial.{u_1} ↥(Subgroup.zpowers g1)
⊢ IsCyclic.{u_1} ↥(Subgroup.zpowers g1)

Tactic:
have h3 : IsCyclic ↥(Subgroup.zpowers g1) := by rw [h]; exact h1
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
h2 : Nontrivial.{u_1} ↥(Subgroup.zpowers g1)
h3 : IsCyclic.{u_1} ↥(Subgroup.zpowers g1)
inr : Subgroup.genLTOne (Subgroup.zpowers g2) = g2
⊢ g1 = g2

Tactic:
simp only [(Subgroup.zpowers g2).genLTOne_unique hg1 h]

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne_unique, Subgroup.zpowers
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
h2 : Nontrivial.{u_1} ↥(Subgroup.zpowers g1)
h3 : IsCyclic.{u_1} ↥(Subgroup.zpowers g1)
inr : Subgroup.genLTOne (Subgroup.zpowers g1) = g2
⊢ Subgroup.genLTOne (Subgroup.zpowers g2) = g2

Tactic:
simp only [← h]
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
g1 g2 : G
hg1 : g1 < 1
hg2 : g2 < 1
h : Eq (α := Subgroup G) (Subgroup.zpowers g1) (Subgroup.zpowers g2)
h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)
h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
h2 : Nontrivial.{u_1} ↥(Subgroup.zpowers g1)
h3 : IsCyclic.{u_1} ↥(Subgroup.zpowers g1)
⊢ Subgroup.genLTOne (Subgroup.zpowers g1) = g2

Tactic:
simp only [(Subgroup.zpowers g1).genLTOne_unique hg2 h.symm]

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne_unique, Subgroup.zpowers, Eq.symm
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
inst_4 : IsCyclic G
⊢ genLTOne G = Subgroup.genLTOne ⊤

Tactic:
rfl

Premises used: LinearOrderedCommGroup.genLTOne, rfl
-- Module: Mathlib.Algebra.Order.Group.Cyclic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : Nontrivial G
inst_4 : IsCyclic G
g : G
hg : g < 1
htop : Eq (α := Subgroup G) (Subgroup.zpowers g) ⊤
⊢ g = genLTOne G

Tactic:
(⊤ : Subgroup G).genLTOne_unique hg htop

Premises used: LinearOrderedCommGroup.Subgroup.genLTOne_unique, LinearOrderedCommGroup.genLTOne, Top.top
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
a b c : α
bc : a * b ≤ a * c
⊢ b ≤ c

Tactic:
simpa using mul_le_mul_right bc a⁻¹

Premises used: mul_le_mul_right, Inv.inv
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
a b c : α
bc : b * a ≤ c * a
⊢ b ≤ c

Tactic:
simpa using mul_le_mul_right bc a⁻¹

Premises used: mul_le_mul_right, Inv.inv
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
h : a⁻¹ = a
⊢ a = 1

Tactic:
match lt_trichotomy a 1 with
  | Or.inl h₁ =>
    have : 1 < a := h ▸ one_lt_inv_of_inv h₁
    absurd h₁ this.asymm
  | Or.inr (Or.inl h₁) => h₁
  | Or.inr (Or.inr h₁) =>
    have : a < 1 := h ▸ inv_lt_one'.mpr h₁
    absurd h₁ this.asymm

Premises used: Iff.mpr, one_lt_inv_of_inv, inv_lt_one', Eq.rec, LT.lt.asymm, absurd, _private.0.eq_one_of_inv_eq'.match_1, OfNat.ofNat, Eq, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : Nontrivial α
obtain : ∀ (y : α) (hy : y ≠ 1), ∃ (a : α), 1 < a
⊢ ∃ (a : α), 1 < a

Tactic:
obtain ⟨y, hy⟩ := Decidable.exists_ne (1 : α)

Premises used: Decidable.exists_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : Nontrivial α
y : α
hy : y ≠ 1
inl : ∀ (h : y < 1), ∃ (a : α), 1 < a
inr : ∀ (h : 1 < y), ∃ (a : α), 1 < a
⊢ ∃ (a : α), 1 < a

Tactic:
obtain h | h := hy.lt_or_gt

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : Nontrivial α
y : α
hy : y ≠ 1
h : y < 1
⊢ ∃ (a : α), 1 < a

Tactic:
⟨y⁻¹, one_lt_inv'.mpr h⟩

Premises used: Iff.mpr, one_lt_inv', Inv.inv, Exists.intro
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : Nontrivial α
y : α
hy : y ≠ 1
h : y < 1
⊢ ∃ (a : α), 1 < a

Tactic:
exact ⟨y⁻¹, one_lt_inv'.mpr h⟩
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : Nontrivial α
y : α
hy : y ≠ 1
h : 1 < y
⊢ ∃ (a : α), 1 < a

Tactic:
⟨y, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : Nontrivial α
y : α
hy : y ≠ 1
h : 1 < y
⊢ ∃ (a : α), 1 < a

Tactic:
exact ⟨y, h⟩
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
inst_3 : Nontrivial α
⊢ ∃ (a : α), 1 < a

Tactic:
exists_one_lt'

Premises used: exists_one_lt'
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
inst_3 : Nontrivial α
obtain : ∀ (y : α) (hy : 1 < y) (a : α), ∃ (b : α), a < b
⊢ ∀ (a : α), ∃ (b : α), a < b

Tactic:
obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'

Premises used: exists_one_lt'
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
inst_3 : Nontrivial α
y : α
hy : 1 < y
⊢ ∀ (a : α), ∃ (b : α), a < b

Tactic:
fun a => ⟨a * y, lt_mul_of_one_lt_right' a hy⟩

Premises used: HMul.hMul, lt_mul_of_one_lt_right', Exists.intro
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
inst_3 : Nontrivial α
y : α
hy : 1 < y
⊢ ∀ (a : α), ∃ (b : α), a < b

Tactic:
exact fun a => ⟨a * y, lt_mul_of_one_lt_right' a hy⟩
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
inst_3 : Nontrivial α
obtain : ∀ (y : α) (hy : 1 < y) (a : α), ∃ (b : α), b < a
⊢ ∀ (a : α), ∃ (b : α), b < a

Tactic:
obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'

Premises used: exists_one_lt'
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
inst_3 : Nontrivial α
y : α
hy : 1 < y
⊢ ∀ (a : α), ∃ (b : α), b < a

Tactic:
fun a => ⟨a / y, (div_lt_self_iff a).mpr hy⟩

Premises used: Iff.mpr, div_lt_self_iff, HDiv.hDiv, Exists.intro
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
inst_3 : Nontrivial α
y : α
hy : 1 < y
⊢ ∀ (a : α), ∃ (b : α), b < a

Tactic:
exact fun a => ⟨a / y, (div_lt_self_iff a).mpr hy⟩
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a⁻¹ ≤ a ↔ 1 ≤ a

Tactic:
simp [inv_le_iff_one_le_mul']

Premises used: inv_le_iff_one_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a⁻¹ < a ↔ 1 < a

Tactic:
simp [inv_lt_iff_one_lt_mul]

Premises used: inv_lt_iff_one_lt_mul
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
contrapose! : a⁻¹ < a ↔ 1 < a
⊢ a ≤ a⁻¹ ↔ a ≤ 1

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a⁻¹ < a ↔ 1 < a

Tactic:
inv_lt_self_iff

Premises used: inv_lt_self_iff
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a⁻¹ < a ↔ 1 < a

Tactic:
exact inv_lt_self_iff

Premises used: inv_lt_self_iff
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
contrapose! : a⁻¹ ≤ a ↔ 1 ≤ a
⊢ a < a⁻¹ ↔ a < 1

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a⁻¹ ≤ a ↔ 1 ≤ a

Tactic:
inv_le_self_iff

Premises used: inv_le_self_iff
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a⁻¹ ≤ a ↔ 1 ≤ a

Tactic:
exact inv_le_self_iff

Premises used: inv_le_self_iff
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ a ≤ b → b⁻¹ ≤ a⁻¹

Tactic:
inv_le_inv_iff.mpr

Premises used: Iff.mpr, inv_le_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ a < b → b⁻¹ < a⁻¹

Tactic:
inv_lt_inv_iff.mpr

Premises used: Iff.mpr, inv_lt_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ 1 < a → a⁻¹ < 1

Tactic:
inv_lt_one_iff_one_lt.mpr

Premises used: Iff.mpr, inv_lt_one_iff_one_lt
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ 1 ≤ a → a⁻¹ ≤ 1

Tactic:
inv_le_one'.mpr

Premises used: Iff.mpr, inv_le_one'
-- Module: Mathlib.Algebra.Order.Group.Defs
Goal:
α : Type u
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a ≤ 1 → 1 ≤ a⁻¹

Tactic:
one_le_inv'.mpr

Premises used: Iff.mpr, one_le_inv'
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b : α
h : ∀ (ε : α), ε < 1 → a * ε ≤ b
⊢ a ≤ b

Tactic:
le_of_forall_one_lt_le_mul (α := αᵒᵈ) h

Premises used: le_of_forall_one_lt_le_mul
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b : α
h : ∀ (ε : α), 1 < ε → a / ε ≤ b
ε : α
ε1 : ε < 1
⊢ a * ε ≤ b

Tactic:
simpa only [div_eq_mul_inv, inv_inv] using h ε⁻¹ (Left.one_lt_inv_iff.2 ε1)

Premises used: Iff.mpr, div_eq_mul_inv, Inv.inv, inv_inv, Left.one_lt_inv_iff
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b : α
⊢ a ≤ b ↔ ∀ (ε : α), ε < 1 → a * ε ≤ b

Tactic:
le_iff_forall_one_lt_le_mul (α := αᵒᵈ)

Premises used: OrderDual, le_iff_forall_one_lt_le_mul
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : Group α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulRightStrictMono α
a b c : α
hc : c < a * b
obtain : ∀ (a' : α) (hc' : c / b < a') (ha' : a' < a), ∃ (a' : α), a' < a ∧ c < a' * b
⊢ ∃ (a' : α), a' < a ∧ c < a' * b

Tactic:
obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul.2 hc)

Premises used: Iff.mpr, exists_between, div_lt_iff_lt_mul
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : Group α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulRightStrictMono α
a b c : α
hc : c < a * b
a' : α
hc' : c / b < a'
ha' : a' < a
⊢ ∃ (a' : α), a' < a ∧ c < a' * b

Tactic:
⟨a', ha', div_lt_iff_lt_mul.1 hc'⟩

Premises used: And.intro, Exists.intro, Iff.mp, div_lt_iff_lt_mul
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : Group α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulRightStrictMono α
a b c : α
hc : c < a * b
a' : α
hc' : c / b < a'
ha' : a' < a
⊢ ∃ (a' : α), a' < a ∧ c < a' * b

Tactic:
exact ⟨a', ha', div_lt_iff_lt_mul.1 hc'⟩
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulLeftStrictMono α
a b c : α
hc : c < a * b
obtain : ∀ (a' : α) (hc' : c / a < a') (ha' : a' < b), ∃ (b' : α), b' < b ∧ c < a * b'
⊢ ∃ (b' : α), b' < b ∧ c < a * b'

Tactic:
obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul'.2 hc)

Premises used: Iff.mpr, div_lt_iff_lt_mul', exists_between
-- Module: Mathlib.Algebra.Order.Group.DenselyOrdered
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulLeftStrictMono α
a b c : α
hc : c < a * b
a' : α
hc' : c / a < a'
ha' : a' < b
⊢ ∃ (b' : α), b' < b ∧ c < a * b'

Tactic:
⟨a', ha', div_lt_iff_lt_mul'.1 hc'⟩

Premises used: div_lt_iff_lt_mul', And.intro, Exists.intro, Iff.mp