awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Order.Archimedean
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)
⊢ ∃ (a : G), s = closure {a}

Tactic:
s.dense_or_cyclic.resolve_left hd

Premises used: Or.resolve_left, Subgroup.dense_or_cyclic
-- Module: Mathlib.Topology.Algebra.Order.Archimedean
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)
⊢ ∃ (a : G), s = closure {a}

Tactic:
exact s.dense_or_cyclic.resolve_left hd

Premises used: Or.resolve_left, Subgroup.dense_or_cyclic
-- Module: Mathlib.Topology.Algebra.Order.Archimedean
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)
if₁ : ∀ (hd : ¬Dense (↑s : Set G)), Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)
if₂ : ∀ (hd : Dense (↑s : Set G)), Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)
if₃ 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)

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

Premises used: Dense, xor_true, id, SetLike.coe, xor_false, Subgroup.zpowers_eq_closure, rfl
-- Module: Mathlib.Topology.Algebra.Order.Archimedean
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
⊢ Dense (↑s : Set G) ↔ ∀ (a : G), s ≠ zpowers a

Tactic:
simp [xor_iff_iff_not.1 s.dense_xor_cyclic]

Premises used: xor_iff_iff_not, Subgroup.dense_xor_cyclic, Iff.mp
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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)
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)
⊢ DiscreteTopology.{u_1} ↥(zpowers g)

Tactic:
wlog ha : 1 ≤ g
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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⁻¹)

Tactic:
specialize this g⁻¹ (one_le_inv'.mpr (le_of_not_ge ha))

Premises used: Iff.mpr, le_of_not_ge, Inv.inv, one_le_inv'
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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⁻¹)
inr inr₁ inr₂ inr₃ : ∀ (this : DiscreteTopology.{u_1} ↥(zpowers g)), DiscreteTopology.{u_1} ↥(zpowers g)
⊢ DiscreteTopology.{u_1} ↥(zpowers g)

Tactic:
rwa [zpowers_inv] at this

Premises used: Subgroup.zpowers_inv
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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)
inr : ∀ (ha : 1 < g), DiscreteTopology.{u_1} ↥(zpowers g)
⊢ DiscreteTopology.{u_1} ↥(zpowers g)

Tactic:
rcases eq_or_lt_of_le ha with rfl | ha

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
inl : DiscreteTopology.{u_1} ↥⊥
⊢ DiscreteTopology.{u_1} ↥(zpowers 1)

Tactic:
rw [zpowers_one_eq_bot]

Premises used: Subgroup.zpowers_one_eq_bot
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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} ↥⊥

Tactic:
Subsingleton.discreteTopology

Premises used: Subsingleton.discreteTopology
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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} ↥⊥

Tactic:
exact Subsingleton.discreteTopology

Premises used: Subsingleton.discreteTopology
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
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}
⊢ DiscreteTopology.{u_1} ↥(zpowers g)

Tactic:
rw [discreteTopology_iff_isOpen_singleton_one, isOpen_induced_iff]

Premises used: discreteTopology_iff_isOpen_singleton_one, isOpen_induced_iff
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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}

Tactic:
⟨Set.Ioo (g ^ (-1 : ℤ)) (g ^ (1 : ℤ)), isOpen_Ioo, ?_⟩

Premises used: isOpen_Ioo, HPow.hPow, And.intro, Exists.intro, OfNat.ofNat, Set.Ioo, Neg.neg
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
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}
⊢ ∃ (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:
refine ⟨Set.Ioo (g ^ (-1 : ℤ)) (g ^ (1 : ℤ)), isOpen_Ioo, ?_⟩
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
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) ⋯) ↔
      Membership.mem (γ := Set ↥(zpowers g)) {1}
        (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) ((fun (x : ℤ) ↦ g ^ x) n) ⋯)
⊢ 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:
ext ⟨_, ⟨n, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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) ⋯)
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) ⋯) →
    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))
      (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) ⋯)

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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 :
  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) ⋯)
        1
⊢ 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) ⋯)

Tactic:
simp only [Set.mem_preimage, Set.mem_Ioo, Set.mem_singleton_iff, and_imp]

Premises used: Set.mem_Ioo, and_imp, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
⊢ -1 < n

Tactic:
rw [zpow_lt_zpow_iff_right ha] at hn hn'

Premises used: zpow_lt_zpow_iff_right
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
⊢ n < 1

Tactic:
rw [zpow_lt_zpow_iff_right ha] at hn hn'

Premises used: zpow_lt_zpow_iff_right
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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 : -1 < n
hn' : n < 1
⊢ n = 0

Tactic:
lia
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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 : -1 < n
hn' : n < 1
⊢ Eq (α := ↥(zpowers g)) (Subtype.mk (p := fun (x : G) ↦ Membership.mem (γ := Subgroup G) (zpowers g) x) (g ^ n) ⋯) 1

Tactic:
simp only [Subtype.ext_iff, show n = 0 by lia, zpow_zero, coe_one]

Premises used: zpow_zero, Subtype.ext_iff, Subgroup.coe_one
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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)) {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) ⋯)

Tactic:
simp_all
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
⊢ Nontrivial G

Tactic:
nontriviality G
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
h : Nontrivial G
⊢ IsCyclic G

Tactic:
LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered.mpr fun h ↦
    have := h.subsingleton_of_discreteTopology; false_of_nontrivial_of_subsingleton G

Premises used: Iff.mpr, DenselyOrdered.subsingleton_of_discreteTopology, false_of_nontrivial_of_subsingleton, LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
h : Nontrivial G
⊢ IsCyclic G

Tactic:
exact LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered.mpr fun h ↦
    have := h.subsingleton_of_discreteTopology; false_of_nontrivial_of_subsingleton G

Premises used: Iff.mpr, DenselyOrdered.subsingleton_of_discreteTopology, false_of_nontrivial_of_subsingleton, LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
⊢ Nontrivial G

Tactic:
nontriviality G using isCyclic_of_subsingleton, Subsingleton.discreteTopology

Premises used: Subsingleton.discreteTopology, isCyclic_of_subsingleton
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
rw : (∃ (g : G), zpowers g = H) ↔ DiscreteTopology.{u_1} ↥H
⊢ IsCyclic.{u_1} ↥H ↔ DiscreteTopology.{u_1} ↥H

Tactic:
rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]

Premises used: Subgroup.isCyclic_iff_exists_zpowers_eq_top
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
mpr : DiscreteTopology.{u_1} ↥H → ∃ (g : G), zpowers g = H
⊢ (∃ (g : G), zpowers g = H) ↔ DiscreteTopology.{u_1} ↥H

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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 : Nontrivial G
g : G
⊢ DiscreteTopology.{u_1} ↥(zpowers g)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
⊢ Dense (↑H : Set G) ∨ ∃ (a : G), H = closure {a}

Tactic:
have := H.dense_or_cyclic
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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}
⊢ Dense (↑H : Set G) ∨ ∃ (a : G), zpowers a = H

Tactic:
simp only [← Subgroup.zpowers_eq_closure, Eq.comm (a := H)] at this

Premises used: Eq.comm, Subgroup.zpowers_eq_closure
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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

Tactic:
fun hA ↦ this.elim (fun h ↦ ?_) id

Premises used: id, Or.elim
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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
mpr : ∀ (hA : DiscreteTopology.{u_1} ↥H) (h : Dense (↑H : Set G)), ∃ (g : G), zpowers g = H
⊢ DiscreteTopology.{u_1} ↥H → ∃ (g : G), zpowers g = H

Tactic:
refine fun hA ↦ this.elim (fun h ↦ ?_) id

Premises used: id, Or.elim
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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)
rw₂ rw₃ : (↑H : Set G) = (↑H : Set G)
⊢ H = ⊤

Tactic:
rw [← coe_eq_univ, ← (dense_iff_closure_eq.mp h), H.isClosed_of_discrete.closure_eq]

Premises used: IsClosed.closure_eq, dense_iff_closure_eq, Subgroup.isClosed_of_discrete, Subgroup.coe_eq_univ, Iff.mp
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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)
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) ⊤
⊢ ∃ (g : G), zpowers g = H

Tactic:
obtain rfl : H = ⊤ := by
      rw [← coe_eq_univ, ← (dense_iff_closure_eq.mp h), H.isClosed_of_discrete.closure_eq]

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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)
rwa rwa₁ rwa₂ rwa₃ : DiscreteTopology.{u_1} (↑Set.univ : Type u_1)
⊢ DiscreteTopology G

Tactic:
rwa [← (Homeomorph.Set.univ G).discreteTopology_iff]

Premises used: Homeomorph.Set.univ, Homeomorph.discreteTopology_iff
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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

Tactic:
have : DiscreteTopology G := by rwa [← (Homeomorph.Set.univ G).discreteTopology_iff]
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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_1 : Dense (↑⊤ : Set G) ∨ ∃ (a : G), Eq (α := Subgroup G) (zpowers a) ⊤
hA : DiscreteTopology.{u_1} ↥⊤
h : Dense (↑⊤ : Set G)
this : DiscreteTopology G
⊢ ∃ (g : G), Eq (α := Subgroup G) (zpowers g) ⊤

Tactic:
isCyclic_iff_exists_zpowers_eq_top.mp inferInstance

Premises used: isCyclic_iff_exists_zpowers_eq_top, inferInstance, Iff.mp
-- Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete
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_1 : Dense (↑⊤ : Set G) ∨ ∃ (a : G), Eq (α := Subgroup G) (zpowers a) ⊤
hA : DiscreteTopology.{u_1} ↥⊤
h : Dense (↑⊤ : Set G)
this : DiscreteTopology G
⊢ ∃ (g : G), Eq (α := Subgroup G) (zpowers g) ⊤

Tactic:
exact isCyclic_iff_exists_zpowers_eq_top.mp inferInstance

Premises used: isCyclic_iff_exists_zpowers_eq_top, inferInstance, Iff.mp
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
rw :
  (∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / (↑(b - d)! : K)) ∧
    ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / (↑(b - d)! : K) < a'
⊢ Tendsto.{0, u_1} (β := K) (fun (n : ℕ) ↦ a * c ^ n / (↑(n - d)! : K)) atTop (𝓝 0)

Tactic:
rw [tendsto_order]

Premises used: tendsto_order