awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) x
k : ℕ
hk : x ∈ V ^ (k + 1)
h : x⁻¹ ∈ V⁻¹ ^ (k + 1)
⊢ x⁻¹ ∈ V ^ (k + 1)

Tactic:
rw [← hV.inv]

Premises used: IsTopologicalGroup.mulInvClosureNhd.inv
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
x : G
ha : Membership.mem (γ := Set G) (⋃ (n : ℕ), V ^ (n + 1)) x
k : ℕ
hk : x ∈ V ^ (k + 1)
⊢ x⁻¹ ∈ V⁻¹ ^ (k + 1)

Tactic:
simpa only [inv_pow, Set.mem_inv, inv_inv] using hk

Premises used: inv_pow, inv_inv, Set.mem_inv
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
⊢ IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))

Tactic:
isOpen_iUnion (fun n ↦ ?_)

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
refine : ∀ (n : ℕ), IsOpen[inst_1] (V ^ (n + 1))
⊢ IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))

Tactic:
refine isOpen_iUnion (fun n ↦ ?_)

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
n : ℕ
rw : IsOpen[inst_1] (V ^ n * V)
⊢ IsOpen[inst_1] (V ^ (n + 1))

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
n : ℕ
⊢ IsOpen[inst_1] (V ^ n * V)

Tactic:
hV.isOpen.mul_left

Premises used: IsOpen.mul_left, IsTopologicalGroup.mulInvClosureNhd.isOpen
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
n : ℕ
⊢ IsOpen[inst_1] (V ^ n * V)

Tactic:
exact hV.isOpen.mul_left

Premises used: IsOpen.mul_left, IsTopologicalGroup.mulInvClosureNhd.isOpen
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
⊢ IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))

Tactic:
have : IsOpen (⋃ n, V ^ (n + 1)) := by
    refine isOpen_iUnion (fun n ↦ ?_)
    rw [pow_succ]
    exact hV.isOpen.mul_left
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
h : (↑{ toSubgroup := S, isOpen' := this : OpenSubgroup G } : Set G) ⊆ W
⊢ ∃ (H : OpenSubgroup G), (↑H : Set G) ⊆ W

Tactic:
use ⟨S, this⟩
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
⊢ W * V ^ HAdd.hAdd (α := ℕ) 0 1 ⊆ W

Tactic:
simp [hV.mul]

Premises used: IsTopologicalGroup.mulInvClosureNhd.mul
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
n : ℕ
ih : W * V ^ (n + 1) ⊆ W
succ : W * V ^ (n + 1) * V ⊆ W
⊢ W * V ^ (n + 1 + 1) ⊆ W

Tactic:
rw [pow_succ, ← mul_assoc]

Premises used: pow_succ, mul_assoc
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
n : ℕ
ih : W * V ^ (n + 1) ⊆ W
⊢ W * V ^ (n + 1) * V ⊆ W

Tactic:
(Set.mul_subset_mul_right ih).trans hV.mul

Premises used: HasSubset.Subset.trans, Set.mul_subset_mul_right, npowRec, IsTopologicalGroup.mulInvClosureNhd.mul
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
n : ℕ
ih : W * V ^ (n + 1) ⊆ W
⊢ W * V ^ (n + 1) * V ⊆ W

Tactic:
exact (Set.mul_subset_mul_right ih).trans hV.mul

Premises used: HasSubset.Subset.trans, Set.mul_subset_mul_right, IsTopologicalGroup.mulInvClosureNhd.mul
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
n : ℕ
zero : W * V ^ HAdd.hAdd (α := ℕ) 0 1 ⊆ W
succ : ∀ (n : ℕ) (ih : W * V ^ (n + 1) ⊆ W), W * V ^ (n + 1 + 1) ⊆ W
⊢ W * V ^ (n + 1) ⊆ W

Tactic:
induction n with
    | zero => simp [hV.mul]
    | succ n ih =>
      rw [pow_succ, ← mul_assoc]
      exact (Set.mul_subset_mul_right ih).trans hV.mul

Premises used: pow_succ, mul_assoc, IsTopologicalGroup.mulInvClosureNhd.mul
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
⊢ ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W

Tactic:
have mulVpow (n : ℕ) : W * V ^ (n + 1) ⊆ W := by
    induction n with
    | zero => simp [hV.mul]
    | succ n ih =>
      rw [pow_succ, ← mul_assoc]
      exact (Set.mul_subset_mul_right ih).trans hV.mul
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
n : ℕ
x : G
xin : x ∈ V ^ (n + 1)
right : 1 * x = x
⊢ ∃ x_1 ∈ W, ∃ y ∈ V ^ (n + 1), x_1 * y = x

Tactic:
use 1, einW, x, xin
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
n : ℕ
x : G
xin : x ∈ V ^ (n + 1)
right right₁ : x = x
⊢ 1 * x = x

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
⊢ ∀ (n : ℕ), V ^ (n + 1) ⊆ W * V ^ (n + 1)

Tactic:
have (n : ℕ) : V ^ (n + 1) ⊆ W * V ^ (n + 1) := by
    intro x xin
    rw [Set.mem_mul]
    use 1, einW, x, xin
    rw [one_mul]
-- Module: Mathlib.Topology.Algebra.OpenSubgroup
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : CompactSpace G
W : Set G
WClopen : IsClopen W
einW : 1 ∈ W
V : Set G
hV : mulInvClosureNhd V W
S : Subgroup G := { carrier := ⋃ (n : ℕ), V ^ (n + 1), mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
this_1 : IsOpen[inst_1] (⋃ (n : ℕ), V ^ (n + 1))
mulVpow : ∀ (n : ℕ), W * V ^ (n + 1) ⊆ W
this : ∀ (n : ℕ), V ^ (n + 1) ⊆ W * V ^ (n + 1)
⊢ (↑{ toSubgroup := S, isOpen' := this_1 : OpenSubgroup G } : Set G) ⊆ W

Tactic:
apply iUnion_subset fun i _ a ↦ mulVpow i (this i a)

Premises used: Set.iUnion_subset
-- Module: Mathlib.Topology.Algebra.Order.Archimedean
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
inst_5 : Archimedean 𝕜
⊢ DenseRange.{u_1, 0} (X := 𝕜) Rat.cast

Tactic:
dense_of_exists_between fun _ _ h => Set.exists_range_iff.2 <| exists_rat_btwn h

Premises used: Iff.mpr, exists_rat_btwn, Set.exists_range_iff, DenseRange, dense_of_exists_between
-- 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
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
inl : Subsingleton G → Dense (↑S : Set G)
inr : Nontrivial G → Dense (↑S : Set G)
⊢ Dense (↑S : Set G)

Tactic:
cases subsingleton_or_nontrivial G

Premises used: subsingleton_or_nontrivial
-- 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
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h : Subsingleton G
⊢ Dense (↑S : Set G)

Tactic:
fun x => _root_.subset_closure ?_

Premises used: subset_closure, Dense
-- 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
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h : Subsingleton G
inl : ∀ (x : G), x ∈ (↑S : Set G)
⊢ Dense (↑S : Set G)

Tactic:
refine fun x => _root_.subset_closure ?_

Premises used: subset_closure
-- 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
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h : Subsingleton G
x : G
inl : 1 ∈ (↑S : Set G)
⊢ x ∈ (↑S : Set G)

Tactic:
rw [Subsingleton.elim x 1]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h : Subsingleton G
x : G
⊢ 1 ∈ (↑S : Set G)

Tactic:
one_mem S

Premises used: Set.Mem, OneMemClass.one_mem
-- 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
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h : Subsingleton G
x : G
⊢ 1 ∈ (↑S : Set G)

Tactic:
exact one_mem S

Premises used: OneMemClass.one_mem
-- 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
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h : Nontrivial G
⊢ Dense (↑S : Set G)

Tactic:
dense_of_exists_between fun a b hlt => ?_

Premises used: dense_of_exists_between
-- 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
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h : Nontrivial G
inr : ∀ (a b : G) (hlt : a < b), ∃ c ∈ (↑S : Set G), c ∈ Ioo a b
⊢ Dense (↑S : Set G)

Tactic:
refine dense_of_exists_between fun a b hlt => ?_

Premises used: dense_of_exists_between
-- 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
S : Subgroup G
hS : ∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
h : Nontrivial G
a b : G
hlt : a < b
inr : ∀ (g : G) (hgS : g ∈ S) (hg0 : 1 < g) (hg : g < b / a), ∃ c ∈ (↑S : Set G), c ∈ Ioo a b
⊢ ∃ c ∈ (↑S : Set G), c ∈ Ioo a b

Tactic:
rcases hS (b / a) (one_lt_div'.2 hlt) with ⟨g, hgS, hg0, hg⟩

Premises used: Iff.mpr, one_lt_div', HDiv.hDiv
-- 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
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
inr : ∀ (m : ℤ) (hm : 1 * g ^ m ∈ Ioc a (a * g)), ∃ c ∈ (↑S : Set G), c ∈ Ioo a b
⊢ ∃ c ∈ (↑S : Set G), c ∈ Ioo a b

Tactic:
rcases (existsUnique_add_zpow_mem_Ioc hg0 1 a).exists with ⟨m, hm⟩

Premises used: ExistsUnique.exists, existsUnique_add_zpow_mem_Ioc, OfNat.ofNat
-- 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
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 : 1 * g ^ m ∈ Ioc a (a * g)
⊢ g ^ m ∈ Ioc a (a * g)

Tactic:
rw [one_mul] at hm

Premises used: one_mul
-- 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
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)
⊢ ∃ c ∈ (↑S : Set G), c ∈ Ioo a b

Tactic:
⟨g ^ m, zpow_mem hgS _, hm.1, hm.2.trans_lt ?_⟩

Premises used: zpow_mem, HPow.hPow, And.right, And.left, And.intro, Exists.intro, LE.le.trans_lt
-- 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
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)
inr : a * g < b
⊢ ∃ c ∈ (↑S : Set G), c ∈ Ioo a b

Tactic:
refine ⟨g ^ m, zpow_mem hgS _, hm.1, hm.2.trans_lt ?_⟩
-- 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
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)
inr inr₁ inr₂ inr₃ : ∀ (hg : a * g < b) (m : ℤ) (hm : g ^ m ∈ Ioc a (a * g)), a * g < b
⊢ a * g < b

Tactic:
rwa [lt_div_iff_mul_lt'] at hg

Premises used: lt_div_iff_mul_lt'
-- 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
S : Subgroup G
hbot : S ≠ ⊥
H : ¬∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a
⊢ Dense (↑S : Set G)

Tactic:
S.dense_of_not_isolated_one fun ε ε1 => ?_

Premises used: Subgroup.dense_of_not_isolated_one
-- 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
S : Subgroup G
hbot : S ≠ ⊥
H : ¬∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a
refine : ∀ (ε : G) (ε1 : ε > 1), ∃ g ∈ S, g ∈ Ioo 1 ε
⊢ Dense (↑S : Set G)

Tactic:
refine S.dense_of_not_isolated_one fun ε ε1 => ?_

Premises used: Subgroup.dense_of_not_isolated_one
-- 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
S : Subgroup G
hbot : S ≠ ⊥
H : ¬∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a
ε : G
ε1 : ε > 1
contrapose! : ∀ (H : ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε), ∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a
⊢ ∃ g ∈ S, g ∈ Ioo 1 ε

Tactic:
contrapose! H
-- 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
S : Subgroup G
hbot : S ≠ ⊥
ε : G
ε1 : ε > 1
H : ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε
⊢ ∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a

Tactic:
exists_isLeast_one_lt hbot ε1 (disjoint_left.2 H)

Premises used: Iff.mpr, Set.disjoint_left, Subgroup.exists_isLeast_one_lt
-- 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
S : Subgroup G
hbot : S ≠ ⊥
ε : G
ε1 : ε > 1
H : ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε
⊢ ∃ (a : G), IsLeast {g : G | g ∈ S ∧ 1 < g} a

Tactic:
exact exists_isLeast_one_lt hbot ε1 (disjoint_left.2 H)

Premises used: Iff.mpr, Set.disjoint_left, Subgroup.exists_isLeast_one_lt
-- 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
S : Subgroup G
⊢ Dense (↑S : Set G) ∨ ∃ (a : G), S = closure {a}

Tactic:
(em _).imp (dense_of_not_isolated_one S) fun h => ?_

Premises used: Subgroup.dense_of_not_isolated_one, em, Or.imp
-- 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
S : Subgroup G
refine : ∀ (h : ¬∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε), ∃ (a : G), S = closure {a}
⊢ Dense (↑S : Set G) ∨ ∃ (a : G), S = closure {a}

Tactic:
refine (em _).imp (dense_of_not_isolated_one S) fun h => ?_

Premises used: Subgroup.dense_of_not_isolated_one, em, Or.imp
-- 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
S : Subgroup G
h : ¬∀ ε > 1, ∃ g ∈ S, g ∈ Ioo 1 ε
⊢ ∃ ε > 1, ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε

Tactic:
push Not at h

Premises used: Not
-- 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
S : Subgroup G
h : ∃ ε > 1, ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε
rcases : ∀ (ε : G) (ε1 : ε > 1) (hε : ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε), ∃ (a : G), S = closure {a}
⊢ ∃ (a : G), S = closure {a}

Tactic:
rcases h with ⟨ε, ε1, hε⟩
-- 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
S : Subgroup G
ε : G
ε1 : ε > 1
hε : ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε
⊢ ∃ (a : G), S = closure {a}

Tactic:
cyclic_of_isolated_one ε1 (disjoint_left.2 hε)

Premises used: Iff.mpr, Set.disjoint_left, Subgroup.cyclic_of_isolated_one
-- 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
S : Subgroup G
ε : G
ε1 : ε > 1
hε : ∀ (g : G) (_ : g ∈ S), g ∉ Ioo 1 ε
⊢ ∃ (a : G), S = closure {a}

Tactic:
exact cyclic_of_isolated_one ε1 (disjoint_left.2 hε)

Premises used: Iff.mpr, Set.disjoint_left, Subgroup.cyclic_of_isolated_one
-- 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)
simp : ¬∃ (a : G), s = zpowers a
⊢ Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)

Tactic:
simp only [hd, xor_true]

Premises used: xor_true
-- 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
a : G
hd : Dense (↑(zpowers a) : Set G)
⊢ False

Tactic:
not_denseRange_zpow hd

Premises used: not_denseRange_zpow
-- 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
a : G
hd : Dense (↑(zpowers a) : Set G)
⊢ False

Tactic:
exact not_denseRange_zpow hd

Premises used: not_denseRange_zpow
-- 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)
simp : ∃ (a : G), s = closure {a}
⊢ Xor (Dense (↑s : Set G)) (∃ (a : G), s = zpowers a)

Tactic:
simp only [hd, xor_false, id, zpowers_eq_closure]

Premises used: id, xor_false, Subgroup.zpowers_eq_closure