awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Archimedean (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h : Nontrivial G
a b : G
hlt : a < b
g : G
hgS : g ∈ S
hg0 : 1 < g
hg : g < b / a
m : ℤ
hm : g ^ m ∈ Ioc a (a * g)
⊢ a * g < b
have inr : ∀ (hg : a * g < b) (m : ℤ) (hm : g ^ m ∈ Ioc a (a * g)), a * g < b
Tactic: rwa [lt_div_iff_mul_lt'] at hg
Cleared hypotheses: hg, m, hm
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Archimedean (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
S : Subgroup G
hbot : S ≠ ⊥
H : ¬∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a
⊢ Dense (↑S : Set G)
have refine : ∀ (ε : G) (ε1 : ε > 1), ∃ g ∈ S, g ∈ Ioo 1 ε
Tactic: refine S.dense_of_not_isolated_one fun ε ε1 => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Archimedean (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
S : Subgroup G
hbot : S ≠ ⊥
H : ¬∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a
ε : G
ε1 : ε > 1
⊢ ∃ g ∈ S, g ∈ Ioo 1 ε
have contrapose! : ∀ (H : ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε), ∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Archimedean (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
S : Subgroup G
⊢ Dense (↑S : Set G) ∨ ∃ (a : G), S = closure {a}
have refine : ∀ (h : ¬∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε), ∃ (a : G), S = closure {a}
Tactic: refine (em _).imp (dense_of_not_isolated_one S) fun h => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Archimedean (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
S : Subgroup G
h : ¬∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
⊢ ∃ (a : G), S = closure {a}
have h₁ : ∃ ε > 1, ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Archimedean (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
S : Subgroup G
h : ∃ ε > 1, ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε
⊢ ∃ (a : G), S = closure {a}
have rcases : ∀ (ε : G) (ε1 : ε > 1) (hε : ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε), ∃ (a : G), S = closure {a}
Tactic: rcases h with ⟨ε, ε1, hε⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Archimedean (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
inst_6 : Nontrivial G
inst_7 : DenselyOrdered G
s : Subgroup G
hd : Dense (↑s : Set G)
⊢ Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)
have simp : ¬∃ (a : G), s = zpowers a
Tactic: simp only [hd, xor_true]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Archimedean (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
inst_6 : Nontrivial G
inst_7 : DenselyOrdered G
s : Subgroup G
hd : ¬Dense (↑s : Set G)
⊢ Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)
have simp : ∃ (a : G), s = closure {a}
Tactic: simp only [hd, xor_false, id, zpowers_eq_closure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Archimedean (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
inst_6 : Nontrivial G
inst_7 : DenselyOrdered G
s : Subgroup G
⊢ Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)
have if : ∀ (hd : Dense (↑s : Set G)), Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)
Tactic: if hd : Dense (s : Set G) then
    simp only [hd, xor_true]
    rintro ⟨a, rfl⟩
    exact not_denseRange_zpow hd
  else
    simp only [hd, xor_false, id, zpowers_eq_closure]
    exact s.dense_or_cyclic.resolve_left hd
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.Archimedean (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
inst_6 : Nontrivial G
inst_7 : DenselyOrdered G
s : Subgroup G
if : ∀ (hd : Dense (↑s : Set G)), Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)
⊢ Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)
have if₁ : ∀ (hd : ¬Dense (↑s : Set G)), Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)
Tactic: if hd : Dense (s : Set G) then
    simp only [hd, xor_true]
    rintro ⟨a, rfl⟩
    exact not_denseRange_zpow hd
  else
    simp only [hd, xor_false, id, zpowers_eq_closure]
    exact s.dense_or_cyclic.resolve_left hd
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
g : G
⊢ DiscreteTopology.{u_1} ↥(zpowers g)
have inr : ∀
  (this :
    ∀ {G : Type u_1} [inst : CommGroup G] [inst_5 : LinearOrder G] [IsOrderedMonoid G] [inst_7 : TopologicalSpace G]
      [OrderTopology G] (g : G) (ha : 1 ≤ g), DiscreteTopology.{u_1} ↥(zpowers g))
  (ha : ¬1 ≤ g), DiscreteTopology.{u_1} ↥(zpowers g)
Tactic: wlog ha : 1 ≤ g
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
g : G
inr :
  ∀
    (this :
      ∀ {G : Type u_1} [inst : CommGroup G] [inst_5 : LinearOrder G] [IsOrderedMonoid G] [inst_7 : TopologicalSpace G]
        [OrderTopology G] (g : G) (ha : 1 ≤ g), DiscreteTopology.{u_1} ↥(zpowers g))
    (ha : ¬1 ≤ g), DiscreteTopology.{u_1} ↥(zpowers g)
⊢ DiscreteTopology.{u_1} ↥(zpowers g)
have wlog : ∀ {G : Type u_1} [inst : CommGroup G] [inst_5 : LinearOrder G] [IsOrderedMonoid G] [inst_7 : TopologicalSpace G]
  [OrderTopology G] (g : G) (ha : 1 ≤ g), DiscreteTopology.{u_1} ↥(zpowers g)
Tactic: wlog ha : 1 ≤ g
Cleared hypotheses: inst_1, inst_2, inst_4, g
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
g : G
this :
  ∀ {G : Type u_1} [inst : CommGroup G] [inst_5 : LinearOrder G] [IsOrderedMonoid G] [inst_7 : TopologicalSpace G]
    [OrderTopology G] (g : G) (ha : 1 ≤ g), DiscreteTopology.{u_1} ↥(zpowers g)
ha : ¬1 ≤ g
⊢ DiscreteTopology.{u_1} ↥(zpowers g)
have this₁ : DiscreteTopology.{u_1} ↥(zpowers g⁻¹)
Tactic: specialize this g⁻¹ (one_le_inv'.mpr (le_of_not_ge ha))
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
g : G
ha : ¬1 ≤ g
this : DiscreteTopology.{u_1} ↥(zpowers g⁻¹)
⊢ DiscreteTopology.{u_1} ↥(zpowers g)
have inr : ∀ (this : DiscreteTopology.{u_1} ↥(zpowers g)), DiscreteTopology.{u_1} ↥(zpowers g)
Tactic: rwa [zpowers_inv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
g : G
ha : 1 ≤ g
⊢ DiscreteTopology.{u_1} ↥(zpowers g)
have inl : ∀ (ha : LE.le.{u_1} (α := G) 1 1), DiscreteTopology.{u_1} ↥(zpowers 1)
Tactic: rcases eq_or_lt_of_le ha with rfl | ha
Cleared hypotheses: g, ha
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
g : G
ha : 1 ≤ g
inl : ∀ (ha : LE.le.{u_1} (α := G) 1 1), DiscreteTopology.{u_1} ↥(zpowers 1)
⊢ DiscreteTopology.{u_1} ↥(zpowers g)
have inr : ∀ (ha : 1 < g), DiscreteTopology.{u_1} ↥(zpowers g)
Tactic: rcases eq_or_lt_of_le ha with rfl | ha
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
ha : LE.le.{u_1} (α := G) 1 1
⊢ DiscreteTopology.{u_1} ↥(zpowers 1)
have inl : DiscreteTopology.{u_1} ↥⊥
Tactic: rw [zpowers_one_eq_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
g : G
ha_1 : 1 ≤ g
ha : 1 < g
⊢ DiscreteTopology.{u_1} ↥(zpowers g)
have inr : ∃ (t : Set G),
  IsOpen t ∧
    Eq (α := Set ↥(zpowers g)) (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹' t)
      {1}
Tactic: rw [discreteTopology_iff_isOpen_singleton_one, isOpen_induced_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
g : G
ha_1 : 1 ≤ g
ha : 1 < g
⊢ ∃ (t : Set G),
    IsOpen t ∧
      Eq (α := Set ↥(zpowers g)) (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹' t)
        {1}
have inr : Eq (α := Set ↥(zpowers g))
  (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹'
    Set.Ioo (HPow.hPow (β := ℤ) g (-1)) (HPow.hPow (β := ℤ) g 1))
  {1}
Tactic: refine ⟨Set.Ioo (g ^ (-1 : ℤ)) (g ^ (1 : ℤ)), isOpen_Ioo, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
g : G
ha_1 : 1 ≤ g
ha : 1 < g
⊢ Eq (α := Set ↥(zpowers g))
    (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹'
      Set.Ioo (HPow.hPow (β := ℤ) g (-1)) (HPow.hPow (β := ℤ) g 1))
    {1}
have inr : ∀ (n : ℤ),
  Membership.mem (γ := Set ↥(zpowers g))
      (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹'
        Set.Ioo (HPow.hPow (β := ℤ) g (-1)) (HPow.hPow (β := ℤ) g 1))
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) sorry) ↔
    Membership.mem (γ := Set ↥(zpowers g)) {1}
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) sorry)
Tactic: ext ⟨_, ⟨n, rfl⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
g : G
ha_1 : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ Membership.mem (γ := Set ↥(zpowers g))
      (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹'
        Set.Ioo (HPow.hPow (β := ℤ) g (-1)) (HPow.hPow (β := ℤ) g 1))
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) ⋯) ↔
    Membership.mem (γ := Set ↥(zpowers g)) {1}
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) ⋯)
have inr : Membership.mem (γ := Set ↥(zpowers g))
    (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹'
      Set.Ioo (HPow.hPow (β := ℤ) g (-1)) (HPow.hPow (β := ℤ) g 1))
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) sorry) →
  Membership.mem (γ := Set ↥(zpowers g)) {1}
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) sorry)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
g : G
ha_1 : 1 ≤ g
ha : 1 < g
n : ℤ
inr :
  Membership.mem (γ := Set ↥(zpowers g))
      (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹'
        Set.Ioo (HPow.hPow (β := ℤ) g (-1)) (HPow.hPow (β := ℤ) g 1))
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) ⋯) →
    Membership.mem (γ := Set ↥(zpowers g)) {1}
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) ⋯)
⊢ Membership.mem (γ := Set ↥(zpowers g))
      (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹'
        Set.Ioo (HPow.hPow (β := ℤ) g (-1)) (HPow.hPow (β := ℤ) g 1))
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) ⋯) ↔
    Membership.mem (γ := Set ↥(zpowers g)) {1}
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) ⋯)
have inr₁ : Membership.mem (γ := Set ↥(zpowers g)) {1}
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) sorry) →
  Membership.mem (γ := Set ↥(zpowers g))
    (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹'
      Set.Ioo (HPow.hPow (β := ℤ) g (-1)) (HPow.hPow (β := ℤ) g 1))
    (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) sorry)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
g : G
ha_1 : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ Membership.mem (γ := Set ↥(zpowers g))
      (Subtype.val (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ⁻¹'
        Set.Ioo (HPow.hPow (β := ℤ) g (-1)) (HPow.hPow (β := ℤ) g 1))
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) ⋯) →
    Membership.mem (γ := Set ↥(zpowers g)) {1}
      (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) ⋯)
have inr : HPow.hPow (β := ℤ) g (-1) < g ^ n →
  g ^ n < HPow.hPow (β := ℤ) g 1 →
    Eq (α := ↥(zpowers g)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) (g ^ n) sorry) 1
Tactic: simp only [Set.mem_preimage, Set.mem_Ioo, Set.mem_singleton_iff, and_imp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (hypothesis)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
g : G
ha_1 : 1 ≤ g
ha : 1 < g
n : ℤ
hn : HPow.hPow (β := ℤ) g (-1) < g ^ n
hn' : g ^ n < HPow.hPow (β := ℤ) g 1
⊢ Eq (α := ↥(zpowers g)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) (g ^ n) ⋯) 1
have hn₁ : -1 < n
Tactic: rw [zpow_lt_zpow_iff_right ha] at hn hn'
Cleared hypotheses: hn, hn'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (hypothesis)
Goal:
G_1 : Type u_1
inst : CommGroup G_1
inst_1 : TopologicalSpace G_1
G : Type u_1
inst_2 : CommGroup G
inst_3 : LinearOrder G
inst_4 : IsOrderedMonoid G
inst_5 : TopologicalSpace G
inst_6 : OrderTopology G
g : G
ha_1 : 1 ≤ g
ha : 1 < g
n : ℤ
hn : HPow.hPow (β := ℤ) g (-1) < g ^ n
hn' : g ^ n < HPow.hPow (β := ℤ) g 1
hn₁ : -1 < n
⊢ Eq (α := ↥(zpowers g)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) (g ^ n) ⋯) 1
have hn'₁ : n < 1
Tactic: rw [zpow_lt_zpow_iff_right ha] at hn hn'
Cleared hypotheses: hn, hn'
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
inst_6 : DiscreteTopology G
⊢ IsCyclic G
have a : Nontrivial G
Tactic: nontriviality G
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
⊢ IsCyclic.{u_1} ↥H ↔ DiscreteTopology.{u_1} ↥H
have a : Nontrivial G
Tactic: nontriviality G using isCyclic_of_subsingleton, Subsingleton.discreteTopology
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
h : Nontrivial G
⊢ IsCyclic.{u_1} ↥H ↔ DiscreteTopology.{u_1} ↥H
have rw : (∃ (g : G), zpowers g = H) ↔ DiscreteTopology.{u_1} ↥H
Tactic: rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
h : Nontrivial G
⊢ (∃ (g : G), zpowers g = H) ↔ DiscreteTopology.{u_1} ↥H
have mp : (∃ (g : G), zpowers g = H) → DiscreteTopology.{u_1} ↥H
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
h : Nontrivial G
mp : (∃ (g : G), zpowers g = H) → DiscreteTopology.{u_1} ↥H
⊢ (∃ (g : G), zpowers g = H) ↔ DiscreteTopology.{u_1} ↥H
have mpr : DiscreteTopology.{u_1} ↥H → ∃ (g : G), zpowers g = H
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
h : Nontrivial G
⊢ DiscreteTopology.{u_1} ↥H → ∃ (g : G), zpowers g = H
have this : Dense (↑H : Set G) ∨ ∃ (a : G), H = closure {a}
Tactic: have := H.dense_or_cyclic
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
h : Nontrivial G
this : Dense (↑H : Set G) ∨ ∃ (a : G), H = closure {a}
⊢ DiscreteTopology.{u_1} ↥H → ∃ (g : G), zpowers g = H
have this₁ : Dense (↑H : Set G) ∨ ∃ (a : G), zpowers a = H
Tactic: simp only [← Subgroup.zpowers_eq_closure, Eq.comm (a := H)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
h : Nontrivial G
this : Dense (↑H : Set G) ∨ ∃ (a : G), zpowers a = H
⊢ DiscreteTopology.{u_1} ↥H → ∃ (g : G), zpowers g = H
have mpr : ∀ (hA : DiscreteTopology.{u_1} ↥H) (h : Dense (↑H : Set G)), ∃ (g : G), zpowers g = H
Tactic: refine fun hA ↦ this.elim (fun h ↦ ?_) id
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
h_1 : Nontrivial G
this : Dense (↑H : Set G) ∨ ∃ (a : G), zpowers a = H
hA : DiscreteTopology.{u_1} ↥H
h : Dense (↑H : Set G)
⊢ H = ⊤
have rw : (↑H : Set G) = Set.univ
Tactic: rw [← coe_eq_univ, ← (dense_iff_closure_eq.mp h), H.isClosed_of_discrete.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
h_1 : Nontrivial G
this : Dense (↑H : Set G) ∨ ∃ (a : G), zpowers a = H
hA : DiscreteTopology.{u_1} ↥H
h : Dense (↑H : Set G)
rw : (↑H : Set G) = Set.univ
⊢ H = ⊤
have rw₁ : (↑H : Set G) = _root_.closure (↑H : Set G)
Tactic: rw [← coe_eq_univ, ← (dense_iff_closure_eq.mp h), H.isClosed_of_discrete.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
h_1 : Nontrivial G
this : Dense (↑H : Set G) ∨ ∃ (a : G), zpowers a = H
hA : DiscreteTopology.{u_1} ↥H
h : Dense (↑H : Set G)
rw : (↑H : Set G) = Set.univ
rw₁ : (↑H : Set G) = _root_.closure (↑H : Set G)
⊢ H = ⊤
have rw₂ : (↑H : Set G) = (↑H : Set G)
Tactic: rw [← coe_eq_univ, ← (dense_iff_closure_eq.mp h), H.isClosed_of_discrete.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
H : Subgroup G
h_1 : Nontrivial G
this : Dense (↑H : Set G) ∨ ∃ (a : G), zpowers a = H
hA : DiscreteTopology.{u_1} ↥H
h : Dense (↑H : Set G)
⊢ ∃ (g : G), zpowers g = H
have mpr : ∀ (this : Dense (↑⊤ : Set G) ∨ ∃ (a : G), Eq (α := Subgroup G) (zpowers a) ⊤) (hA : DiscreteTopology.{u_1} ↥⊤)
  (h : Dense (↑⊤ : Set G)), ∃ (g : G), Eq (α := Subgroup G) (zpowers g) ⊤
Tactic: obtain rfl : H = ⊤ := by
      rw [← coe_eq_univ, ← (dense_iff_closure_eq.mp h), H.isClosed_of_discrete.closure_eq]
Cleared hypotheses: H, this, hA, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (goal)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
h_1 : Nontrivial G
this : Dense (↑⊤ : Set G) ∨ ∃ (a : G), Eq (α := Subgroup G) (zpowers a) ⊤
hA : DiscreteTopology.{u_1} ↥⊤
h : Dense (↑⊤ : Set G)
⊢ DiscreteTopology G
have rwa : DiscreteTopology.{u_1} (↑Set.univ : Type u_1)
Tactic: rwa [← (Homeomorph.Set.univ G).discreteTopology_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete (hypothesis)
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : TopologicalSpace G
inst_4 : OrderTopology G
inst_5 : MulArchimedean G
h_1 : Nontrivial G
this : Dense (↑⊤ : Set G) ∨ ∃ (a : G), Eq (α := Subgroup G) (zpowers a) ⊤
hA : DiscreteTopology.{u_1} ↥⊤
h : Dense (↑⊤ : Set G)
⊢ ∃ (g : G), Eq (α := Subgroup G) (zpowers g) ⊤
have this₁ : DiscreteTopology G
Tactic: have : DiscreteTopology G := by rwa [← (Homeomorph.Set.univ G).discreteTopology_iff]