awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
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
⊢ 0 < k ∧ k < 1
have 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
Tactic: rw [← one_lt_inv'] at hlt
Cleared hypotheses: hlt, k, hab, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
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
⊢ 0 < k ∧ k < 1
have inl : HPow.hPow (β := ℤ) a⁻¹ 0 < a⁻¹ ^ k ∧ a⁻¹ ^ k < HPow.hPow (β := ℤ) a⁻¹ 1
Tactic: simp_rw [← zpow_lt_zpow_iff_right hlt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
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
⊢ False
have inr : ∀ (b : α) (hb : b ≠ 1), False
Tactic: rcases exists_ne (1 : α) with ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
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
⊢ False
have inr : ∀ (b : α) (hb : 1 < b) (hba : b < a), False
Tactic: rcases exists_between hlt with ⟨b, hb, hba⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
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
⊢ False
have inr : ∀ (k : ℤ) (hb : LT.lt.{u_1} (α := α) 1 ((fun (x : ℤ) ↦ a ^ x) k)) (hba : (fun (x : ℤ) ↦ a ^ x) k < a), False
Tactic: rcases ha b with ⟨k, rfl⟩
Cleared hypotheses: b, hb, hba
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
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
⊢ False
have inr : 0 < k ∧ k < 1
Tactic: suffices 0 < k ∧ k < 1 by lia
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Basic (goal)
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
⊢ 0 < k ∧ k < 1
have inr : HPow.hPow (β := ℤ) a 0 < a ^ k ∧ a ^ k < HPow.hPow (β := ℤ) a 1
Tactic: simp_rw [← zpow_lt_zpow_iff_right hlt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cone (goal)
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)
⊢ p = q
have 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
Tactic: cases p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cone (goal)
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)
⊢ { toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := @eq_one_of_mem_of_inv_mem' : GroupCone G } = q
have 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 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cone (goal)
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, 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 }
have mk : toSubmonoid = toSubmonoid_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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 < 1, Subgroup.zpowers a = H
have obtain : ∀ (a : G) (ha : Subgroup.zpowers a = H), ∃ a < 1, Subgroup.zpowers a = H
Tactic: obtain ⟨a, ha⟩ := H.isCyclic_iff_exists_zpowers_eq_top.mp hH
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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
⊢ ∃ a < 1, Subgroup.zpowers a = H
have inl : ∀ (ha1 : a < 1), ∃ a < 1, Subgroup.zpowers a = H
Tactic: obtain ha1 | rfl | ha1 := lt_trichotomy a 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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
⊢ ∃ a < 1, Subgroup.zpowers a = H
have inr : ∀ (ha : Subgroup.zpowers 1 = H), ∃ a < 1, Subgroup.zpowers a = H
Tactic: obtain ha1 | rfl | ha1 := lt_trichotomy a 1
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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
⊢ ∃ a < 1, Subgroup.zpowers a = H
have inr₁ : ∀ (ha1 : 1 < a), ∃ a < 1, Subgroup.zpowers a = H
Tactic: obtain ha1 | rfl | ha1 := lt_trichotomy a 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (hypothesis)
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
⊢ ∃ a < 1, Subgroup.zpowers a = H
have ha₁ : ⊥ = H
Tactic: rw [Subgroup.zpowers_one_eq_bot] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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
⊢ ∃ a < 1, Subgroup.zpowers a = H
have right : Subgroup.zpowers a⁻¹ = H
Tactic: use a⁻¹, Left.inv_lt_one_iff.mpr ha1
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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
⊢ Subgroup.zpowers a⁻¹ = H
have right₁ : H = H
Tactic: rw [Subgroup.zpowers_inv, ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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 ∈ H
have nth_rewrite : Membership.mem (γ := Subgroup G) (Subgroup.zpowers (Subgroup.genLTOne H)) (Subgroup.genLTOne H)
Tactic: nth_rewrite 1 [← H.genLTOne_zpowers_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (hypothesis)
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
⊢ g = Subgroup.genLTOne H
have hg' : ¬IsOfFinOrder g
Tactic: have hg' : ¬ IsOfFinOrder g := not_isOfFinOrder_of_isMulTorsionFree (ne_of_lt hg)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (hypothesis)
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
⊢ g = Subgroup.genLTOne H
have hH₁ : Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers (Subgroup.genLTOne H))
Tactic: rw [← H.genLTOne_zpowers_eq_top] at hH
Cleared hypotheses: hH, hg'
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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
⊢ g = Subgroup.genLTOne H
have inl : g = Subgroup.genLTOne H → g = Subgroup.genLTOne H
Tactic: rcases (Subgroup.zpowers_eq_zpowers_iff hg').mp hH with _ | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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
⊢ g = Subgroup.genLTOne H
have inr : ∀ (h : g⁻¹ = Subgroup.genLTOne H), g = Subgroup.genLTOne H
Tactic: rcases (Subgroup.zpowers_eq_zpowers_iff hg').mp hH with _ | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (hypothesis)
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
have hg₁ : 1 < Subgroup.genLTOne H
Tactic: rw [← one_lt_inv', h] at hg
Cleared hypotheses: hg, hH, hg', h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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)
⊢ g1 = g2
have inl : ∀ (h' : Eq (α := Subgroup G) (Subgroup.zpowers g2) ⊥), g1 = g2
Tactic: rcases (Subgroup.zpowers g2).bot_or_nontrivial with (h' | h')
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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
⊢ g1 = g2
have inr : ∀ (h' : Nontrivial.{u_1} ↥(Subgroup.zpowers g2)), g1 = g2
Tactic: rcases (Subgroup.zpowers g2).bot_or_nontrivial with (h' | h')
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (hypothesis)
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) ⊥
⊢ g1 = g2
have h₁ : Eq (α := Subgroup G) (Subgroup.zpowers g1) ⊥
Tactic: rw [h'] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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)
have rw : ∃ (g : G), Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers g2)
Tactic: rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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
⊢ ∃ (g : G), Eq (α := Subgroup G) (Subgroup.zpowers g) (Subgroup.zpowers g2)
have h₁ : Eq (α := Subgroup G) (Subgroup.zpowers g2) (Subgroup.zpowers g2)
Tactic: use g2
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (hypothesis)
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)
⊢ g1 = g2
have h1 : IsCyclic.{u_1} ↥(Subgroup.zpowers g2)
Tactic: have h1 : IsCyclic ↥(Subgroup.zpowers g2) := by
      rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]; use g2
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (hypothesis)
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)
⊢ g1 = g2
have h2 : Nontrivial.{u_1} ↥(Subgroup.zpowers g1)
Tactic: have h2 : Nontrivial ↥(Subgroup.zpowers g1) := by rw [h]; exact h'
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (hypothesis)
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)
⊢ g1 = g2
have h3 : IsCyclic.{u_1} ↥(Subgroup.zpowers g1)
Tactic: have h3 : IsCyclic ↥(Subgroup.zpowers g1) := by rw [h]; exact h1
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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)
⊢ g1 = g2
have inr : Subgroup.genLTOne (Subgroup.zpowers g2) = g2
Tactic: simp only [(Subgroup.zpowers g2).genLTOne_unique hg1 h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Cyclic (goal)
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 g2) = g2
have inr : Subgroup.genLTOne (Subgroup.zpowers g1) = g2
Tactic: simp only [← h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Defs (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : Nontrivial α
⊢ ∃ (a : α), 1 < a
have obtain : ∀ (y : α) (hy : y ≠ 1), ∃ (a : α), 1 < a
Tactic: obtain ⟨y, hy⟩ := Decidable.exists_ne (1 : α)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Defs (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : Nontrivial α
y : α
hy : y ≠ 1
⊢ ∃ (a : α), 1 < a
have inl : ∀ (h : y < 1), ∃ (a : α), 1 < a
Tactic: obtain h | h := hy.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Defs (goal)
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
⊢ ∃ (a : α), 1 < a
have inr : ∀ (h : 1 < y), ∃ (a : α), 1 < a
Tactic: obtain h | h := hy.lt_or_gt
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Defs (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
inst_3 : Nontrivial α
⊢ ∀ (a : α), ∃ (b : α), a < b
have obtain : ∀ (y : α) (hy : 1 < y) (a : α), ∃ (b : α), a < b
Tactic: obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Defs (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
inst_3 : Nontrivial α
⊢ ∀ (a : α), ∃ (b : α), b < a
have obtain : ∀ (y : α) (hy : 1 < y) (a : α), ∃ (b : α), b < a
Tactic: obtain ⟨y, hy⟩ : ∃ a : α, 1 < a := exists_one_lt'
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Defs (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a ≤ a⁻¹ ↔ a ≤ 1
have contrapose! : a⁻¹ < a ↔ 1 < a
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Defs (goal)
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a < a⁻¹ ↔ a < 1
have contrapose! : a⁻¹ ≤ a ↔ 1 ≤ a
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulRightStrictMono α
a b c : α
hc : c < a * b
⊢ ∃ (a' : α), a' < a ∧ c < a' * b
have obtain : ∀ (a' : α) (hc' : c / b < a') (ha' : a' < a), ∃ (a' : α), a' < a ∧ c < a' * b
Tactic: obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul.2 hc)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulLeftStrictMono α
a b c : α
hc : c < a * b
⊢ ∃ (b' : α), b' < b ∧ c < a * b'
have obtain : ∀ (a' : α) (hc' : c / a < a') (ha' : a' < b), ∃ (b' : α), b' < b ∧ c < a * b'
Tactic: obtain ⟨a', hc', ha'⟩ := exists_between (div_lt_iff_lt_mul'.2 hc)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulRightStrictMono α
a b c : α
hc : a * b < c
⊢ ∃ (a' : α), a' > a ∧ a' * b < c
have obtain : ∀ (a' : α) (ha' : a < a') (hc' : a' < c / b), ∃ (a' : α), a' > a ∧ a' * b < c
Tactic: obtain ⟨a', ha', hc'⟩ := exists_between (lt_div_iff_mul_lt.2 hc)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LT α
inst_2 : DenselyOrdered α
inst_3 : MulLeftStrictMono α
a b c : α
hc : a * b < c
⊢ ∃ (b' : α), b' > b ∧ a * b' < c
have obtain : ∀ (a' : α) (ha' : b < a') (hc' : a' < c / a), ∃ (b' : α), b' > b ∧ a * b' < c
Tactic: obtain ⟨a', ha', hc'⟩ := exists_between (lt_div_iff_mul_lt'.2 hc)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
⊢ c ≤ a * b
have refine : ∀ (d : α) (hd : a * b < d), c ≤ d
Tactic: refine le_of_forall_gt_imp_ge_of_dense fun d hd ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd : a * b < d
⊢ c ≤ d
have obtain : ∀ (a' : α) (ha' : a' > a) (hd : a' * b < d), c ≤ d
Tactic: obtain ⟨a', ha', hd⟩ := exists_mul_left_lt hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' > a → ∀ (b' : α), b' > b → c ≤ a' * b'
d : α
hd_1 : a * b < d
a' : α
ha' : a' > a
hd : a' * b < d
⊢ c ≤ d
have obtain : ∀ (b' : α) (hb' : b' > b) (hd : a' * b' < d), c ≤ d
Tactic: obtain ⟨b', hb', hd⟩ := exists_mul_right_lt hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
⊢ a * b ≤ c
have refine : ∀ (d : α) (hd : d < a * b), d ≤ c
Tactic: refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd : d < a * b
⊢ d ≤ c
have obtain : ∀ (a' : α) (ha' : a' < a) (hd : d < a' * b), d ≤ c
Tactic: obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : DenselyOrdered α
a b c : α
h : ∀ (a' : α), a' < a → ∀ (b' : α), b' < b → a' * b' ≤ c
d : α
hd_1 : d < a * b
a' : α
ha' : a' < a
hd : d < a' * b
⊢ d ≤ c
have obtain : ∀ (b' : α) (hb' : b' < b) (hd : d < a' * b'), d ≤ c
Tactic: obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
⊢ ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
have obtain : ∀ (y : M) (hy : 1 < y) (hyx : y < x), ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
Tactic: obtain ⟨y, hy, hyx⟩ := exists_between hx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.DenselyOrdered (goal)
Goal:
M : Type u_2
inst : LinearOrder M
inst_1 : DenselyOrdered M
x : M
inst_2 : CommMonoid M
inst_3 : ExistsMulOfLE M
inst_4 : IsOrderedCancelMonoid M
hx : 1 < x
y : M
hy : 1 < y
hyx : y < x
⊢ ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
have inl : ∀ (hyx : HPow.hPow (β := ℕ) y 2 ≤ x), ∃ (y : M), 1 < y ∧ HPow.hPow (β := ℕ) y 2 ≤ x
Tactic: obtain hyx | hxy := le_total (y ^ 2) x