awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A_1 : Type u_1
A : Type u_2
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : LocallyFiniteOrderBot A
inst_4 : DecidableEq A
n : A
a : A × A
simp : a.1 + a.2 = n → a ∈ Iic n ×ˢ Iic n
⊢ a ∈ {uv ∈ Iic n ×ˢ Iic n | uv.1 + uv.2 = n} ↔ a.1 + a.2 = n

Tactic:
simp only [mem_filter, and_iff_right_iff_imp]

Premises used: and_iff_right_iff_imp, Finset.mem_filter
-- Module: Mathlib.Algebra.Order.Antidiag.Prod
Goal:
A_1 : Type u_1
A : Type u_2
inst : AddCommMonoid A
inst_1 : PartialOrder A
inst_2 : CanonicallyOrderedAdd A
inst_3 : LocallyFiniteOrderBot A
inst_4 : DecidableEq A
n : A
a : A × A
h : a.1 + a.2 = n
⊢ a ∈ Iic n ×ˢ Iic n

Tactic:
simp [← h]
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
inst : CommMonoid G
inst_1 : LinearOrder G
inst_2 : CommMonoid M
inst_3 : PartialOrder M
inst_4 : MulArchimedean M
f : G →* M
hf : StrictMono.{u_1, u_2} (α := G) (β := M) (⇑f : (a : G) → M)
x x_1 : G
h : 1 < x_1
⊢ LT.lt.{u_2} (α := M) (1 : M) ((f : (a : G) → M) x_1 : M)

Tactic:
simpa using hf h
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
inst : CommMonoid G
inst_1 : LinearOrder G
inst_2 : CommMonoid M
inst_3 : PartialOrder M
inst_4 : MulArchimedean M
f : G →* M
hf : StrictMono.{u_1, u_2} (α := G) (β := M) (⇑f : (a : G) → M)
x x_1 : G
h : 1 < x_1
refine : ∀ (a : ℕ), (f : (a : G) → M) x ≤ HPow.hPow (α := M) ((f : (a : G) → M) x_1 : M) a → x ≤ x_1 ^ a
⊢ ∃ (n : ℕ), x ≤ x_1 ^ n

Tactic:
refine (MulArchimedean.arch (f x) (by simpa using hf h)).imp ?_

Premises used: Exists.imp, DFunLike.coe, MulArchimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
inst : CommMonoid G
inst_1 : LinearOrder G
inst_2 : CommMonoid M
inst_3 : PartialOrder M
inst_4 : MulArchimedean M
f : G →* M
hf : StrictMono.{u_1, u_2} (α := G) (β := M) (⇑f : (a : G) → M)
x x_1 : G
h : 1 < x_1
⊢ ∀ (a : ℕ), (f : (a : G) → M) x ≤ HPow.hPow (α := M) ((f : (a : G) → M) x_1 : M) a → x ≤ x_1 ^ a

Tactic:
simp [← map_pow, hf.le_iff_le]

Premises used: map_pow, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
x y : Gᵒᵈ
hy_1 : 1 < y
hy : LT.lt (α := G) ((ofDual : (a : Gᵒᵈ) → G) y : G) (1 : G)
n : ℕ
hn : ((ofDual : (a : Gᵒᵈ) → G) x)⁻¹ ≤ HPow.hPow (α := G) (((ofDual : (a : Gᵒᵈ) → G) y)⁻¹ : G) n
rwa : ∀ (hn : ((ofDual : (a : Gᵒᵈ) → G) x)⁻¹ ≤ (HPow.hPow (α := G) ((ofDual : (a : Gᵒᵈ) → G) y : G) n)⁻¹), x ≤ y ^ n
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hn : HPow.hPow (α := G) ((ofDual : (a : Gᵒᵈ) → G) y : G) n ≤ (ofDual : (a : Gᵒᵈ) → G) x), x ≤ y ^ n
⊢ x ≤ y ^ n

Tactic:
rwa [inv_pow, inv_le_inv_iff] at hn

Premises used: inv_pow, inv_le_inv_iff
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst : CommGroup G
inst_1 : PartialOrder G
inst_2 : MulArchimedean G
⊢ Archimedean.{u_1} (Additive G)

Tactic:
⟨fun x _ hy ↦ MulArchimedean.arch x.toMul hy⟩

Premises used: Archimedean.mk, Additive.toMul, DFunLike.coe, MulArchimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst : AddCommGroup G
inst_1 : PartialOrder G
inst_2 : Archimedean G
⊢ MulArchimedean.{u_1} (Multiplicative G)

Tactic:
⟨fun x _ hy ↦ Archimedean.arch x.toAdd hy⟩

Premises used: Multiplicative.toAdd, Archimedean.arch, MulArchimedean.mk, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
obtain : ∀ (k : ℕ) (hk : g⁻¹ ≤ a ^ k), ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
obtain ⟨k, hk : g⁻¹ ≤ a ^ k⟩ := MulArchimedean.arch g⁻¹ ha

Premises used: Inv.inv, MulArchimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
⊢ -(↑k : ℤ) ∈ s

Tactic:
simpa [s] using inv_le_inv' hk

Premises used: inv_le_inv'
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
⊢ s.Nonempty

Tactic:
have h_ne : s.Nonempty := ⟨-k, by simpa [s] using inv_le_inv' hk⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
h_ne : s.Nonempty
obtain : ∀ (k : ℕ) (hk : g ≤ a ^ k), ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
obtain ⟨k, hk⟩ := MulArchimedean.arch g ha

Premises used: MulArchimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
n : ℤ
hn : n ∈ s
apply : a ^ n ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)
⊢ n ≤ (↑k : ℤ)

Tactic:
apply (zpow_le_zpow_iff_right ha).mp

Premises used: zpow_le_zpow_iff_right, Iff.mp
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
n : ℤ
hn : n ∈ s
rw : ∀ (hk : g ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)) (n : ℤ) (hn : n ∈ s), a ^ n ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)
⊢ a ^ n ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)

Tactic:
rw [← zpow_natCast] at hk

Premises used: zpow_natCast
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)
n : ℤ
hn : n ∈ s
⊢ a ^ n ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)

Tactic:
le_trans hn hk

Premises used: le_trans
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)
n : ℤ
hn : n ∈ s
⊢ a ^ n ≤ HPow.hPow (β := ℤ) a (↑k : ℤ)

Tactic:
exact le_trans hn hk

Premises used: le_trans
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
⊢ ∀ n ∈ s, n ≤ (↑k : ℤ)

Tactic:
have h_bdd : ∀ n ∈ s, n ≤ (k : ℤ) := by
    intro n hn
    apply (zpow_le_zpow_iff_right ha).mp
    rw [← zpow_natCast] at hk
    exact le_trans hn hk
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
obtain : ∀ (m : ℤ) (hm : m ∈ s) (hm' : ∀ z ∈ s, z ≤ m), ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
obtain ⟨m, hm, hm'⟩ := Int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne

Premises used: Nat.cast, Exists.intro, Int.exists_greatest_of_bdd
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
contrapose! : ∀ (hm' : a ^ (m + 1) ≤ g), ∃ z ∈ s, m < z
⊢ g < a ^ (m + 1)

Tactic:
contrapose! hm'
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : a ^ (m + 1) ≤ g
⊢ ∃ z ∈ s, m < z

Tactic:
⟨m + 1, hm', lt_add_one _⟩

Premises used: lt_add_one, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : a ^ (m + 1) ≤ g
⊢ ∃ z ∈ s, m < z

Tactic:
exact ⟨m + 1, hm', lt_add_one _⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
⊢ g < a ^ (m + 1)

Tactic:
have hm'' : g < a ^ (m + 1) := by
    contrapose! hm'
    exact ⟨m + 1, hm', lt_add_one _⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
⟨m, ⟨hm, hm''⟩, fun n hn => (hm' n hn.1).antisymm <| Int.le_of_lt_add_one ?_⟩

Premises used: Int.le_of_lt_add_one, LE.le.antisymm, And.left, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
refine : ∀ (n : ℤ) (hn : (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) n), m < n + 1
⊢ ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
refine ⟨m, ⟨hm, hm''⟩, fun n hn => (hm' n hn.1).antisymm <| Int.le_of_lt_add_one ?_⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
n : ℤ
hn : (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) n
rw : a ^ m < a ^ (n + 1)
⊢ m < n + 1

Tactic:
rw [← zpow_lt_zpow_iff_right ha]

Premises used: zpow_lt_zpow_iff_right
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
n : ℤ
hn : (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) n
⊢ a ^ m < a ^ (n + 1)

Tactic:
lt_of_le_of_lt hm hn.2

Premises used: lt_of_le_of_lt, And.right
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
s : Set ℤ := {n : ℤ | a ^ n ≤ g}
k_1 : ℕ
hk_1 : g⁻¹ ≤ a ^ k_1
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ (↑k : ℤ)
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
n : ℤ
hn : (fun (k : ℤ) ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) n
⊢ a ^ m < a ^ (n + 1)

Tactic:
exact lt_of_le_of_lt hm hn.2

Premises used: lt_of_le_of_lt, And.right
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
g : G
⊢ ∃! k : ℤ, 1 ≤ g / a ^ k ∧ g / a ^ k < a

Tactic:
simpa only [one_le_div', zpow_add_one, div_lt_iff_lt_mul'] using
    existsUnique_zpow_near_of_one_lt ha g

Premises used: div_lt_iff_lt_mul', zpow_add_one, one_le_div', existsUnique_zpow_near_of_one_lt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! m : ℤ, b / a ^ m ∈ Ico c (c * a)

Tactic:
simpa only [mem_Ico, le_div_iff_mul_le, one_mul, mul_comm c, div_lt_iff_lt_mul, mul_assoc] using
    existsUnique_zpow_near_of_one_lt' ha (b / c)

Premises used: Set.mem_Ico, mul_assoc, HDiv.hDiv, existsUnique_zpow_near_of_one_lt', mul_comm, one_mul, le_div_iff_mul_le, div_lt_iff_lt_mul
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x : ℤ, b * HPow.hPow (β := ℤ) a ((Equiv.neg ℤ : (a : ℤ) → ℤ) x : ℤ) ∈ Ico c (c * a)

Tactic:
simpa only [Equiv.neg_apply, mem_Ico, zpow_neg, ← div_eq_mul_inv, le_div_iff_mul_le, one_mul,
      mul_comm c, div_lt_iff_lt_mul, mul_assoc] using existsUnique_zpow_near_of_one_lt' ha (b / c)

Premises used: Set.mem_Ico, mul_assoc, HDiv.hDiv, div_eq_mul_inv, Equiv.neg_apply, existsUnique_zpow_near_of_one_lt', zpow_neg, mul_comm, one_mul, le_div_iff_mul_le, div_lt_iff_lt_mul
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x : ℤ, b * HPow.hPow (β := ℤ) a ((Equiv.addRight 1 : (a : ℤ) → ℤ) x : ℤ) ∈ Ioc c (c * a)

Tactic:
simpa only [zpow_add_one, div_lt_iff_lt_mul', le_div_iff_mul_le', ← mul_assoc, and_comm,
      mem_Ioc, Equiv.coe_addRight, mul_le_mul_iff_right] using
      existsUnique_zpow_near_of_one_lt ha (c / b)

Premises used: div_lt_iff_lt_mul', mul_le_mul_iff_right, mul_assoc, le_div_iff_mul_le', zpow_add_one, HDiv.hDiv, Equiv.coe_addRight, and_comm, Set.mem_Ioc, existsUnique_zpow_near_of_one_lt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
inst : CommGroup G
inst_1 : LinearOrder G
inst_2 : IsOrderedMonoid G
inst_3 : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! x : ℤ, b / HPow.hPow (β := ℤ) a ((Equiv.neg ℤ : (a : ℤ) → ℤ) x : ℤ) ∈ Ioc c (c * a)

Tactic:
simpa only [Equiv.neg_apply, zpow_neg, div_inv_eq_mul] using
      existsUnique_add_zpow_mem_Ioc ha b c

Premises used: existsUnique_add_zpow_mem_Ioc, Equiv.neg_apply, zpow_neg, div_inv_eq_mul
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
⊢ IsDirectedOrder R

Tactic:
⟨fun x y ↦
    let ⟨m, hm⟩ := exists_nat_ge x; let ⟨n, hn⟩ := exists_nat_ge y
    let ⟨k, hmk, hnk⟩ := exists_ge_ge m n
    ⟨k, hm.trans <| Nat.mono_cast hmk, hn.trans <| Nat.mono_cast hnk⟩⟩

Premises used: _private.0.instIsDirectedOrder.match_2, _private.0.instIsDirectedOrder.match_1, Nat.mono_cast, Exists, exists_nat_ge, LE.le, Nat.cast, IsDirected.mk, exists_ge_ge, And, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
y x : R
hy : 0 < y
this : 0 ≤ 1 + y
n : ℕ
h : x ≤ n • y
rw rw₁ : (y + 1) ^ n = (y + 1) ^ n
⊢ (1 + y) ^ n = (y + 1) ^ n

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
y : R
inst_4 : ExistsAddOfLE R
x : R
hy1 : 1 < y
obtain : ∀ (z : R) (hz : 0 < z) (hy1 : 1 < 1 + z), ∃ (n : ℕ), x < (1 + z) ^ n
⊢ ∃ (n : ℕ), x < y ^ n

Tactic:
obtain ⟨z, hz, rfl⟩ := exists_pos_add_of_lt' hy1

Premises used: exists_pos_add_of_lt', rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x z : R
hz : 0 < z
hy1 : 1 < 1 + z
rw : ∃ (n : ℕ), x < (z + 1) ^ n
⊢ ∃ (n : ℕ), x < (1 + z) ^ n

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x z : R
hz : 0 < z
hy1 : 1 < 1 + z
⊢ ∃ (n : ℕ), x < (z + 1) ^ n

Tactic:
add_one_pow_unbounded_of_pos _ hz

Premises used: add_one_pow_unbounded_of_pos
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x z : R
hz : 0 < z
hy1 : 1 < 1 + z
⊢ ∃ (n : ℕ), x < (z + 1) ^ n

Tactic:
exact add_one_pow_unbounded_of_pos _ hz

Premises used: add_one_pow_unbounded_of_pos
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
below : ∃ (n : ℤ), (↑n : R) ≤ x
above : ∃ (n : ℤ), x ≤ (↑n : R)
⊢ ∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ (↑z : R) ≤ x

Tactic:
apply exists_floor'

Premises used: exists_floor'
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
below : ∀ (n : ℤ) (hn : (↑n : R) < x), ∃ (n : ℤ), (↑n : R) ≤ x
⊢ ∃ (n : ℤ), (↑n : R) ≤ x

Tactic:
obtain ⟨n, hn⟩ := exists_int_lt x

Premises used: exists_int_lt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
n : ℤ
hn : (↑n : R) < x
⊢ ∃ (n : ℤ), (↑n : R) ≤ x

Tactic:
⟨n, hn.le⟩

Premises used: LT.lt.le, Exists.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
n : ℤ
hn : (↑n : R) < x
⊢ ∃ (n : ℤ), (↑n : R) ≤ x

Tactic:
exact ⟨n, hn.le⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
above : ∀ (n : ℤ) (hn : x < (↑n : R)), ∃ (n : ℤ), x ≤ (↑n : R)
⊢ ∃ (n : ℤ), x ≤ (↑n : R)

Tactic:
obtain ⟨n, hn⟩ := exists_int_gt x

Premises used: exists_int_gt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
n : ℤ
hn : x < (↑n : R)
⊢ ∃ (n : ℤ), x ≤ (↑n : R)

Tactic:
⟨n, hn.le⟩

Premises used: LT.lt.le, Exists.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
n : ℤ
hn : x < (↑n : R)
⊢ ∃ (n : ℤ), x ≤ (↑n : R)

Tactic:
exact ⟨n, hn.le⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
⊢ ∃ (n : ℕ), x < y ^ n

Tactic:
have h : ∃ n : ℕ, x < y ^ n := pow_unbounded_of_one_lt _ hy
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ (n : ℕ), x < y ^ n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x < y ^ n) h
hn : x < y ^ n
hn0 : n = 0
⊢ x < 1

Tactic:
rw [hn0, pow_zero] at hn

Premises used: pow_zero
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ (n : ℕ), x < y ^ n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x < y ^ n) h
hn : x < y ^ n
hn0 : n = 0
hn₁ : x < 1
⊢ n = 0

Tactic:
rw [hn0, pow_zero] at hn

Premises used: pow_zero
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ (n : ℕ), x < y ^ n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x < y ^ n) h
hn : x < 1
hn0 : n = 0
⊢ False

Tactic:
not_le_of_gt hn hx

Premises used: not_le_of_gt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ (n : ℕ), x < y ^ n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x < y ^ n) h
hn : x < 1
hn0 : n = 0
⊢ False

Tactic:
exact not_le_of_gt hn hx

Premises used: not_le_of_gt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ (n : ℕ), x < y ^ n
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ x < y ^ n) h
hn : x < y ^ n
hnp : 0 < n
hnsp : n.pred + 1 = n
hltn : n.pred < n
rwa rwa₁ rwa₂ rwa₃ : x < y ^ n
⊢ x < y ^ (n.pred + 1)

Tactic:
rwa [hnsp]
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ (n : ℕ), x < y ^ n
⊢ ∃ (n : ℕ), y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
exact
      let n := Nat.find h
      have hn : x < y ^ n := Nat.find_spec h
      have hnp : 0 < n :=
        pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx
      have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
      have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
      ⟨Nat.pred n, le_of_not_gt (Nat.find_min h hltn), by rwa [hnsp]⟩

Premises used: Iff.mpr, Nat.succ_pred_eq_of_pos, ne_of_gt, Nat.pred_lt, Nat.find, pos_iff_ne_zero, Nat.find_spec
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
R : Type u_3
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
x y : R
hx : 1 ≤ x
hy : 1 < y
h : ∃ (n : ℕ), x < y ^ n
⊢ ∃ (n : ℕ), y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
classical exact
      let n := Nat.find h
      have hn : x < y ^ n := Nat.find_spec h
      have hnp : 0 < n :=
        pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx
      have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
      have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
      ⟨Nat.pred n, le_of_not_gt (Nat.find_min h hltn), by rwa [hnsp]⟩

Premises used: Iff.mpr, Nat.succ_pred_eq_of_pos, ne_of_gt, Nat.pred_lt, Nat.find, pos_iff_ne_zero, Nat.find_spec
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Semifield K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
ε : K
hε : 0 < ε
obtain : ∀ (n : ℕ) (hn : 1 / ε < (↑n : K)), ∃ (n : ℕ), 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε
⊢ ∃ (n : ℕ), 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε

Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt (1 / ε)

Premises used: HDiv.hDiv, exists_nat_gt, OfNat.ofNat