awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
f : G →* H
I : Type w
inst_2 : Group I
g : H →* I
x : Abelianization G
⊢ Eq.{w + 1} (α := Abelianization I)
    ((map g : (a : Abelianization H) → Abelianization I) ((map f : (a : Abelianization G) → Abelianization H) x) :
      Abelianization I)
    ((map (g.comp f) : (a : Abelianization G) → Abelianization I) x : Abelianization I)

Tactic:
DFunLike.congr_fun (map_comp _ _) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', Abelianization.map_comp, Con.liftOn
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
e : G ≃* H
x : Abelianization G
a : G
⊢ Eq.{u + 1} (α := Abelianization G)
    ((Abelianization.map e.symm.toMonoidHom : (a : Abelianization H) → Abelianization G)
        ((Abelianization.map e.toMonoidHom : (a : Abelianization G) → Abelianization H)
          (Quot.mk (⇑(QuotientGroup.leftRel (commutator G)) : G → G → Prop) a)) :
      Abelianization G)
    (Quot.mk (⇑(QuotientGroup.leftRel (commutator G)) : G → G → Prop) a :
      Quot (α := G) (⇑(QuotientGroup.leftRel (commutator G)) : G → G → Prop))

Tactic:
simp
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
e : G ≃* H
x : Abelianization H
a : H
⊢ Eq.{v + 1} (α := Abelianization H)
    ((Abelianization.map e.toMonoidHom : (a : Abelianization G) → Abelianization H)
        ((Abelianization.map e.symm.toMonoidHom : (a : Abelianization H) → Abelianization G)
          (Quot.mk (⇑(QuotientGroup.leftRel (commutator H)) : H → H → Prop) a)) :
      Abelianization H)
    (Quot.mk (⇑(QuotientGroup.leftRel (commutator H)) : H → H → Prop) a :
      Quot (α := H) (⇑(QuotientGroup.leftRel (commutator H)) : H → H → Prop))

Tactic:
simp
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
e : G ≃* H
x : G
⊢ Eq (α := Abelianization H)
    ((e.abelianizationCongr : (a : Abelianization G) → Abelianization H)
        ((Abelianization.of : (a : G) → Abelianization G) x) :
      Abelianization H)
    ((Abelianization.of : (a : H) → Abelianization H) ((e : (a : G) → H) x) : Abelianization H)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
⊢ Eq (α := Abelianization G ≃* Abelianization G) (MulEquiv.abelianizationCongr (MulEquiv.refl G))
    (MulEquiv.refl (Abelianization G))

Tactic:
MulEquiv.toMonoidHom_injective Abelianization.lift_of

Premises used: MulEquiv.toMonoidHom_injective, Abelianization.lift_of
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
e : G ≃* H
⊢ e.abelianizationCongr.symm = e.symm.abelianizationCongr

Tactic:
rfl

Premises used: MulEquiv.abelianizationCongr, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
I : Type v
inst_2 : Group I
e : G ≃* H
e₂ : H ≃* I
⊢ e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr

Tactic:
MulEquiv.toMonoidHom_injective (Abelianization.hom_ext _ _ rfl)

Premises used: Abelianization.hom_ext, MulEquiv.toMonoidHom_injective, rfl
-- Module: Mathlib.GroupTheory.Abelianization.Defs
Goal:
G : Type u
inst : Group G
H : Type u_1
inst_1 : CommGroup H
x : Abelianization H
a : H
⊢ Eq (α := Abelianization H)
    ((of : (a : H) → Abelianization H)
        ((((lift : (a : H →* H) → Abelianization H →* H) (MonoidHom.id H) : Abelianization H →* H) :
            (a : Abelianization H) → H)
          (Quot.mk (⇑(QuotientGroup.leftRel (commutator H)) : H → H → Prop) a)) :
      Abelianization H)
    (Quot.mk (⇑(QuotientGroup.leftRel (commutator H)) : H → H → Prop) a :
      Quot (α := H) (⇑(QuotientGroup.leftRel (commutator H)) : H → H → Prop))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Abelianization.Finite
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
⊢ Finite.{u_1 + 1} (Abelianization G)

Tactic:
Quotient.finite _

Premises used: Quotient.finite, Abelianization
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
ha : IsLeast {g : G | g ∈ H ∧ 1 < g} a
⊢ Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a

Tactic:
obtain ⟨⟨a_in, a_pos⟩, a_min⟩ := ha
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
ha : IsLeast {g : G | g ∈ H ∧ 1 < g} a
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
⊢ a ∈ H

Tactic:
obtain ⟨⟨a_in, a_pos⟩, a_min⟩ := ha
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
ha : IsLeast {g : G | g ∈ H ∧ 1 < g} a
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
⊢ 1 < a

Tactic:
obtain ⟨⟨a_in, a_pos⟩, a_min⟩ := ha
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
⊢ {a} ⊆ (↑H : Set G)

Tactic:
simp [a_in]
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
refine : H ≤ closure {a}
⊢ H = closure {a}

Tactic:
refine le_antisymm ?_ (H.closure_le.mpr <| by simp [a_in])

Premises used: Iff.mpr, Subgroup.closure_le, le_antisymm
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
obtain :
  ∀ (k : ℤ),
    (∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k) →
      ∀ (nonneg : a ^ k ≤ g) (lt : g < a ^ (k + 1)), Membership.mem (γ := Subgroup G) (closure {a}) g
⊢ Membership.mem (γ := Subgroup G) (closure {a}) g

Tactic:
obtain ⟨k, ⟨nonneg, lt⟩, _⟩ := existsUnique_zpow_near_of_one_lt a_pos g

Premises used: existsUnique_zpow_near_of_one_lt
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
by_contra : ∀ (h : ¬g / a ^ k = 1), False
⊢ g / a ^ k = 1

Tactic:
by_contra h
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ a ≤ g / a ^ k

Tactic:
a_min ⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
refine_1 : g / a ^ k ∈ H
refine_2 : 1 < g / a ^ k
⊢ a ≤ g / a ^ k

Tactic:
refine a_min ⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ g / a ^ k ∈ H

Tactic:
Subgroup.div_mem H g_in (Subgroup.zpow_mem H a_in k)

Premises used: Subgroup.div_mem, Subgroup.zpow_mem
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ g / a ^ k ∈ H

Tactic:
exact Subgroup.div_mem H g_in (Subgroup.zpow_mem H a_in k)

Premises used: Subgroup.div_mem, Subgroup.zpow_mem
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ 1 ≤ g / a ^ k

Tactic:
simpa using nonneg
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ 1 < g / a ^ k

Tactic:
exact lt_of_le_of_ne (by simpa using nonneg) (Ne.symm h)

Premises used: Ne.symm, lt_of_le_of_ne
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ a ≤ g / a ^ k

Tactic:
have h : a ≤ g / (a ^ k) := by
      refine a_min ⟨?_, ?_⟩
      · exact Subgroup.div_mem H g_in (Subgroup.zpow_mem H a_in k)
      · exact lt_of_le_of_ne (by simpa using nonneg) (Ne.symm h)
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h_1 : ¬g / a ^ k = 1
h : a ≤ g / a ^ k
⊢ g / a ^ k < a

Tactic:
simpa [zpow_add_one, div_lt_iff_lt_mul'] using lt

Premises used: div_lt_iff_lt_mul', zpow_add_one
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h_1 : ¬g / a ^ k = 1
h : a ≤ g / a ^ k
⊢ ¬a ≤ g / a ^ k

Tactic:
have h' : ¬a ≤ g / (a ^ k) := not_le.mpr (by simpa [zpow_add_one, div_lt_iff_lt_mul'] using lt)
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h_1 : ¬g / a ^ k = 1
h : a ≤ g / a ^ k
h' : ¬a ≤ g / a ^ k
⊢ False

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
⊢ g / a ^ k = 1

Tactic:
have h_zero : g / (a ^ k) = 1 := by
    by_contra h
    have h : a ≤ g / (a ^ k) := by
      refine a_min ⟨?_, ?_⟩
      · exact Subgroup.div_mem H g_in (Subgroup.zpow_mem H a_in k)
      · exact lt_of_le_of_ne (by simpa using nonneg) (Ne.symm h)
    have h' : ¬a ≤ g / (a ^ k) := not_le.mpr (by simpa [zpow_add_one, div_lt_iff_lt_mul'] using lt)
    contradiction
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
a : G
a_min : Membership.mem (γ := Set G) (lowerBounds {g : G | g ∈ H ∧ 1 < g}) a
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right : ∀ (y : ℤ), (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h_zero : g / a ^ k = 1
⊢ Membership.mem (γ := Subgroup G) (closure {a}) g

Tactic:
simp [div_eq_one.mp h_zero, mem_closure_singleton]

Premises used: Subgroup.mem_closure_singleton, div_eq_one, Iff.mp
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
rcases : ∀ (m : ℤ) (hm : g / a ≤ 1 * a ^ m) (hm' : 1 * a ^ m < g / a * a), ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
⊢ ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
rcases existsUnique_mul_zpow_mem_Ico h₀ 1 (g / a) with ⟨m, ⟨hm, hm'⟩, -⟩

Premises used: HDiv.hDiv, existsUnique_mul_zpow_mem_Ico, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g / a ≤ 1 * a ^ m
hm' : 1 * a ^ m < g / a * a
⊢ g ≤ a ^ (m + 1)

Tactic:
simp only [one_mul, div_le_iff_le_mul, div_mul_cancel, ← zpow_add_one] at hm hm'

Premises used: zpow_add_one, div_mul_cancel, div_le_iff_le_mul, one_mul
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g / a ≤ 1 * a ^ m
hm' : 1 * a ^ m < g / a * a
hm₁ : g ≤ a ^ (m + 1)
⊢ a ^ m < g

Tactic:
simp only [one_mul, div_le_iff_le_mul, div_mul_cancel, ← zpow_add_one] at hm hm'

Premises used: zpow_add_one, div_mul_cancel, div_le_iff_le_mul, one_mul
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
lift : 0 ≤ m
lift₁ :
  ∀ (m : ℕ) (hm : g ≤ a ^ HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) (hm' : HPow.hPow (β := ℤ) a (↑m : ℤ) < g),
    ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
⊢ ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
lift m to ℕ
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
rw : 1 < a ^ (m + 1)
⊢ 0 ≤ m

Tactic:
rw [← Int.lt_add_one_iff, ← zpow_lt_zpow_iff_right h₀, zpow_zero]

Premises used: zpow_lt_zpow_iff_right, zpow_zero, Int.lt_add_one_iff
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
⊢ 1 < a ^ (m + 1)

Tactic:
hg.trans_le hm

Premises used: LT.lt.trans_le
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
m : ℤ
hm : g ≤ a ^ (m + 1)
hm' : a ^ m < g
⊢ 1 < a ^ (m + 1)

Tactic:
exact hg.trans_le hm

Premises used: LT.lt.trans_le
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ HAdd.hAdd (α := ℤ) (↑m : ℤ) 1
hm' : HPow.hPow (β := ℤ) a (↑m : ℤ) < g
⊢ g ≤ a ^ m.succ

Tactic:
simp only [← Nat.cast_succ, zpow_natCast] at hm hm'

Premises used: zpow_natCast, Nat.cast_succ
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ HAdd.hAdd (α := ℤ) (↑m : ℤ) 1
hm' : HPow.hPow (β := ℤ) a (↑m : ℤ) < g
hm₁ : g ≤ a ^ m.succ
⊢ a ^ m < g

Tactic:
simp only [← Nat.cast_succ, zpow_natCast] at hm hm'

Premises used: zpow_natCast, Nat.cast_succ
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ m.succ
hm' : a ^ m < g
⊢ ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
⟨m, hm', hm⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
g : G
hg : g > 1
m : ℕ
hm : g ≤ a ^ m.succ
hm' : a ^ m < g
⊢ ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
exact ⟨m, hm', hm⟩
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
⊢ ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))

Tactic:
have hex : ∀ g > 1, ∃ n : ℕ, g ∈ Ioc (a ^ n) (a ^ (n + 1)) := fun g hg => by
    rcases existsUnique_mul_zpow_mem_Ico h₀ 1 (g / a) with ⟨m, ⟨hm, hm'⟩, -⟩
    simp only [one_mul, div_le_iff_le_mul, div_mul_cancel, ← zpow_add_one] at hm hm'
    lift m to ℕ
    · rw [← Int.lt_add_one_iff, ← zpow_lt_zpow_iff_right h₀, zpow_zero]
      exact hg.trans_le hm
    · simp only [← Nat.cast_succ, zpow_natCast] at hm hm'
      exact ⟨m, hm', hm⟩
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
rcases : ∀ (g : G) (hgH : g ∈ H) (hg₀ : g ≠ 1), ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
⊢ ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty

Tactic:
rcases (bot_or_exists_ne_one H).resolve_left hbot with ⟨g, hgH, hg₀⟩

Premises used: Or.resolve_left, Subgroup.bot_or_exists_ne_one
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
g : G
hgH : g ∈ H
hg₀ : g ≠ 1
rcases :
  ∀ (n : ℕ) (hn : |g|ₘ ∈ Ioc (a ^ n) (a ^ (n + 1))), ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
⊢ ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty

Tactic:
rcases hex |g|ₘ (one_lt_mabs.2 hg₀) with ⟨n, hn⟩

Premises used: Iff.mpr, one_lt_mabs, mabs
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
g : G
hgH : g ∈ H
hg₀ : g ≠ 1
n : ℕ
hn : |g|ₘ ∈ Ioc (a ^ n) (a ^ (n + 1))
⊢ ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty

Tactic:
⟨n, _, (@mabs_mem_iff (Subgroup G) G _ _).2 hgH, hn⟩

Premises used: Iff.mpr, mabs_mem_iff, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
g : G
hgH : g ∈ H
hg₀ : g ≠ 1
n : ℕ
hn : |g|ₘ ∈ Ioc (a ^ n) (a ^ (n + 1))
⊢ ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty

Tactic:
exact ⟨n, _, (@mabs_mem_iff (Subgroup G) G _ _).2 hgH, hn⟩
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
⊢ ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty

Tactic:
have : ∃ n : ℕ, Set.Nonempty (H ∩ Ioc (a ^ n) (a ^ (n + 1))) := by
    rcases (bot_or_exists_ne_one H).resolve_left hbot with ⟨g, hgH, hg₀⟩
    rcases hex |g|ₘ (one_lt_mabs.2 hg₀) with ⟨n, hn⟩
    exact ⟨n, _, (@mabs_mem_iff (Subgroup G) G _ _).2 hgH, hn⟩
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
rcases :
  ∀ (n : ℕ) (hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty) (x : G) (hxH : x ∈ (↑H : Set G))
    (hnx : a ^ n < x) (hxn : x ≤ a ^ (n + 1)), ∃ (b : G), IsLeast {g : G | g ∈ H ∧ 1 < g} b
⊢ ∃ (b : G), IsLeast {g : G | g ∈ H ∧ 1 < g} b

Tactic:
rcases Nat.findX this with ⟨n, ⟨x, hxH, hnx, hxn⟩, hmin⟩

Premises used: Nat.findX
-- Module: Mathlib.GroupTheory.Archimedean
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H : Set G) (Ioo 1 a)
hex : ∀ g > 1, ∃ (n : ℕ), g ∈ Ioc (a ^ n) (a ^ (n + 1))
this : ∃ (n : ℕ), ((↑H : Set G) ∩ Ioc (a ^ n) (a ^ (n + 1))).Nonempty
classical :
  ∀ (n : ℕ) (hmin : ∀ m < n, ¬((↑H : Set G) ∩ Ioc (a ^ m) (a ^ (m + 1))).Nonempty) (x : G) (hxH : x ∈ (↑H : Set G))
    (hnx : a ^ n < x) (hxn : x ≤ a ^ (n + 1)), ∃ (b : G), IsLeast {g : G | g ∈ H ∧ 1 < g} b
⊢ ∃ (b : G), IsLeast {g : G | g ∈ H ∧ 1 < g} b

Tactic:
classical rcases Nat.findX this with ⟨n, ⟨x, hxH, hnx, hxn⟩, hmin⟩