awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 < ε
n : ℕ
hn : 1 / ε < (↑n : K)
h : 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε
⊢ ∃ (n : ℕ), 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε

Tactic:
use n
-- 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 < ε
n : ℕ
hn : 1 / ε < (↑n : K)
h : 1 / ε < HAdd.hAdd (α := K) (↑n : K) 1
h₁ : 0 < HAdd.hAdd (α := K) (↑n : K) 1
⊢ 1 / HAdd.hAdd (α := K) (↑n : K) 1 < ε

Tactic:
rw [div_lt_iff₀, ← div_lt_iff₀' hε]

Premises used: div_lt_iff₀, div_lt_iff₀'
-- 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 < ε
n : ℕ
hn : 1 / ε < (↑n : K)
h : (↑n : K) < HAdd.hAdd (α := K) (↑n : K) 1
⊢ 1 / ε < HAdd.hAdd (α := K) (↑n : K) 1

Tactic:
apply hn.trans

Premises used: LT.lt.trans
-- 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 < ε
n : ℕ
hn : 1 / ε < (↑n : K)
⊢ (↑n : K) < HAdd.hAdd (α := K) (↑n : K) 1

Tactic:
simp [zero_lt_one]

Premises used: zero_lt_one
-- 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 < ε
n : ℕ
hn : 1 / ε < (↑n : K)
⊢ 0 < HAdd.hAdd (α := K) (↑n : K) 1

Tactic:
n.cast_add_one_pos

Premises used: Nat.cast_add_one_pos
-- 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 < ε
n : ℕ
hn : 1 / ε < (↑n : K)
⊢ 0 < HAdd.hAdd (α := K) (↑n : K) 1

Tactic:
exact n.cast_add_one_pos

Premises used: Nat.cast_add_one_pos
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
obtain : ∀ (N : ℕ) (hN : x⁻¹ < y ^ N), ∃ (m : ℤ), y ^ m ≤ x
⊢ ∃ (m : ℤ), y ^ m ≤ x

Tactic:
obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy

Premises used: Inv.inv, pow_unbounded_of_one_lt
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
h : HPow.hPow (β := ℤ) y (-(↑N : ℤ)) ≤ x
⊢ ∃ (m : ℤ), y ^ m ≤ x

Tactic:
use -N
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
h : (y ^ N)⁻¹ ≤ x
⊢ HPow.hPow (β := ℤ) y (-(↑N : ℤ)) ≤ x

Tactic:
rw [zpow_neg y ↑N, zpow_natCast]

Premises used: zpow_natCast, Nat.cast, zpow_neg
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ ≤ x

Tactic:
((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le

Premises used: Iff.mpr, lt_trans, inv_pos, LT.lt.le, inv_lt_comm₀, Iff.mp
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ ≤ x

Tactic:
exact ((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le

Premises used: Iff.mpr, lt_trans, inv_pos, LT.lt.le, inv_lt_comm₀, Iff.mp
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
⊢ ∃ (m : ℤ), y ^ m ≤ x

Tactic:
have he : ∃ m : ℤ, y ^ m ≤ x := by
    obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
    use -N
    rw [zpow_neg y ↑N, zpow_natCast]
    exact ((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
obtain : ∀ (M : ℕ) (hM : x < y ^ M), ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
⊢ ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b

Tactic:
obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy

Premises used: pow_unbounded_of_one_lt
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
M : ℕ
hM : x < y ^ M
⊢ ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b

Tactic:
⟨M, fun m hm ↦ ?_⟩

Premises used: Nat.cast, Exists.intro
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
M : ℕ
hM : x < y ^ M
refine : ∀ (m : ℤ) (hm : y ^ m ≤ x), m ≤ (↑M : ℤ)
⊢ ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b

Tactic:
refine ⟨M, fun m hm ↦ ?_⟩
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
M : ℕ
hM : x < y ^ M
m : ℤ
hm : y ^ m ≤ x
contrapose! : ∀ (hM : (↑M : ℤ) < m), y ^ M ≤ x
⊢ m ≤ (↑M : ℤ)

Tactic:
contrapose! hM
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
M : ℕ
m : ℤ
hm : y ^ m ≤ x
hM : (↑M : ℤ) < m
rw : HPow.hPow (β := ℤ) y (↑M : ℤ) ≤ x
⊢ y ^ M ≤ x

Tactic:
rw [← zpow_natCast]

Premises used: zpow_natCast
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
M : ℕ
m : ℤ
hm : y ^ m ≤ x
hM : (↑M : ℤ) < m
⊢ HPow.hPow (β := ℤ) y (↑M : ℤ) ≤ x

Tactic:
le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm

Premises used: LT.lt.le, zpow_le_zpow_right₀, le_trans
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
M : ℕ
m : ℤ
hm : y ^ m ≤ x
hM : (↑M : ℤ) < m
⊢ HPow.hPow (β := ℤ) y (↑M : ℤ) ≤ x

Tactic:
exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm

Premises used: LT.lt.le, zpow_le_zpow_right₀, le_trans
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
⊢ ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b

Tactic:
have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b := by
    obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    refine ⟨M, fun m hm ↦ ?_⟩
    contrapose! hM
    rw [← zpow_natCast]
    exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
hb : ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
obtain : ∀ (n : ℤ) (hn₁ : y ^ n ≤ x) (hn₂ : ∀ (z : ℤ), y ^ z ≤ x → z ≤ n), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he

Premises used: Int.exists_greatest_of_bdd
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
hb : ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
n : ℤ
hn₁ : y ^ n ≤ x
hn₂ : ∀ (z : ℤ), y ^ z ≤ x → z ≤ n
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
⟨n, hn₁, lt_of_not_ge fun hge => (Int.lt_succ _).not_ge (hn₂ _ hge)⟩

Premises used: Int.lt_succ, lt_of_not_ge, HAdd.hAdd, And.intro, Exists.intro, LT.lt.not_ge, OfNat.ofNat
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
he : ∃ (m : ℤ), y ^ m ≤ x
hb : ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b
n : ℤ
hn₁ : y ^ n ≤ x
hn₂ : ∀ (z : ℤ), y ^ z ≤ x → z ≤ n
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
exact ⟨n, hn₁, lt_of_not_ge fun hge => (Int.lt_succ _).not_ge (hn₂ _ hge)⟩
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
have : ∃ (m : ℤ), y ^ m ≤ x
have₁ : ∀ (he : ∃ (m : ℤ), y ^ m ≤ x), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have₂ : ∃ (m : ℤ), y ^ m ≤ x
have₃ have₄ : ∀ (he : ∃ (m : ℤ), y ^ m ≤ x), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have₅ :
  ∀ (he : ∃ (m : ℤ), y ^ m ≤ x) (hb : ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
have₆ :
  ∀ (he : ∃ (m : ℤ), y ^ m ≤ x) (hb : ∃ (b : ℤ), ∀ (m : ℤ), y ^ m ≤ x → m ≤ b) (n : ℤ) (hn₁ : y ^ n ≤ x)
    (hn₂ : ∀ (z : ℤ), y ^ z ≤ x → z ≤ n), ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))
⊢ ∃ (n : ℤ), x ∈ Ico (y ^ n) (y ^ (n + 1))

Tactic:
classical
  have he : ∃ m : ℤ, y ^ m ≤ x := by
    obtain ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
    use -N
    rw [zpow_neg y ↑N, zpow_natCast]
    exact ((inv_lt_comm₀ hx (lt_trans (inv_pos.2 hx) hN)).1 hN).le
  have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b := by
    obtain ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
    refine ⟨M, fun m hm ↦ ?_⟩
    contrapose! hM
    rw [← zpow_natCast]
    exact le_trans (zpow_le_zpow_right₀ hy.le hM.le) hm
  obtain ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
  exact ⟨n, hn₁, lt_of_not_ge fun hge => (Int.lt_succ _).not_ge (hn₂ _ hge)⟩
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
rwa : (y ^ (m + 1))⁻¹ < x
rwa₁ rwa₂ rwa₃ rwa₄ : x⁻¹ < y ^ (m + 1)
⊢ y ^ (-(m + 1)) < x

Tactic:
rwa [zpow_neg, inv_lt_comm₀ (zpow_pos hyp _) hx]

Premises used: zpow_pos, inv_lt_comm₀, zpow_neg
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
rwa : x ≤ y ^ (-m + -1 + 1)
rwa₁ : x ≤ y ^ (-m)
rwa₂ : x ≤ (y ^ m)⁻¹
rwa₃ rwa₄ rwa₅ rwa₆ : y ^ m ≤ x⁻¹
⊢ x ≤ y ^ (-(m + 1) + 1)

Tactic:
rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv_comm₀ hx (zpow_pos hyp _)]

Premises used: le_inv_comm₀, neg_add, zpow_pos, zpow_neg, neg_add_cancel_right
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
pos : ∀ (y_pos : y ≤ 0), ∃ (n : ℕ), y ^ n < x
neg : ∀ (y_pos : 0 < y), ∃ (n : ℕ), y ^ n < x
⊢ ∃ (n : ℕ), y ^ n < x

Tactic:
by_cases! y_pos : y ≤ 0
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
h : HPow.hPow (β := ℕ) y 1 < x
⊢ ∃ (n : ℕ), y ^ n < x

Tactic:
use 1
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
h : y < x
⊢ HPow.hPow (β := ℕ) y 1 < x

Tactic:
simp only [pow_one]

Premises used: pow_one
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y < x

Tactic:
y_pos.trans_lt hx

Premises used: LE.le.trans_lt
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y < x

Tactic:
exact y_pos.trans_lt hx

Premises used: LE.le.trans_lt
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : 0 < y
neg : ∀ (q : ℕ) (hq : x⁻¹ < y⁻¹ ^ q), ∃ (n : ℕ), y ^ n < x
⊢ ∃ (n : ℕ), y ^ n < x

Tactic:
rcases pow_unbounded_of_one_lt x⁻¹ ((one_lt_inv₀ y_pos).2 hy) with ⟨q, hq⟩

Premises used: Iff.mpr, Inv.inv, pow_unbounded_of_one_lt, one_lt_inv₀
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
rwa : ∀ (hq : x⁻¹ < (y ^ q)⁻¹), y ^ q < x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hq : y ^ q < x), y ^ q < x
⊢ y ^ q < x

Tactic:
rwa [inv_pow, inv_lt_inv₀ hx (pow_pos y_pos _)] at hq

Premises used: pow_pos, inv_pow, inv_lt_inv₀
-- 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
x y : K
inst_4 : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ ∃ (n : ℕ), y ^ n < x

Tactic:
exact ⟨q, by rwa [inv_pow, inv_lt_inv₀ hx (pow_pos y_pos _)] at hq⟩
-- 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
x y : K
inst_4 : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
rcases : ∀ (n : ℕ) (hn : y⁻¹ ^ n ≤ x⁻¹) (h'n : x⁻¹ < y⁻¹ ^ (n + 1)), ∃ (n : ℕ), y ^ (n + 1) < x ∧ x ≤ y ^ n
⊢ ∃ (n : ℕ), y ^ (n + 1) < x ∧ x ≤ y ^ n

Tactic:
rcases exists_nat_pow_near (one_le_inv_iff₀.2 ⟨xpos, hx⟩) (one_lt_inv_iff₀.2 ⟨ypos, hy⟩) with
    ⟨n, hn, h'n⟩

Premises used: Iff.mpr, one_lt_inv_iff₀, exists_nat_pow_near, one_le_inv_iff₀, And.intro
-- 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
x y : K
inst_4 : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
⊢ ∃ (n : ℕ), y ^ (n + 1) < x ∧ x ≤ y ^ n

Tactic:
⟨n, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- 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
x y : K
inst_4 : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
refine_1 : y ^ (n + 1) < x
refine_2 : x ≤ y ^ n
⊢ ∃ (n : ℕ), y ^ (n + 1) < x ∧ x ≤ y ^ n

Tactic:
refine ⟨n, ?_, ?_⟩
-- 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
x y : K
inst_4 : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
refine_1 : ∀ (h'n : x⁻¹ < (y ^ (n + 1))⁻¹), y ^ (n + 1) < x
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (h'n : y ^ (n + 1) < x), y ^ (n + 1) < x
⊢ y ^ (n + 1) < x

Tactic:
rwa [inv_pow, inv_lt_inv₀ xpos (pow_pos ypos _)] at h'n

Premises used: pow_pos, inv_pow, inv_lt_inv₀
-- 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
x y : K
inst_4 : ExistsAddOfLE K
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
n : ℕ
hn : y⁻¹ ^ n ≤ x⁻¹
h'n : x⁻¹ < y⁻¹ ^ (n + 1)
refine_2 : ∀ (hn : (y ^ n)⁻¹ ≤ x⁻¹) (h'n : x⁻¹ < y⁻¹ ^ (n + 1)), x ≤ y ^ n
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : ∀ (hn : x ≤ y ^ n) (h'n : x⁻¹ < y⁻¹ ^ (n + 1)), x ≤ y ^ n
⊢ x ≤ y ^ n

Tactic:
rwa [inv_pow, inv_le_inv₀ (pow_pos ypos _) xpos] at hn

Premises used: pow_pos, inv_pow, inv_le_inv₀
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
⊢ ∃ (n : ℕ), c ^ n < b

Tactic:
have := exists_pow_lt_of_lt_one hb₀ hc₁
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
⊢ ∃ (n : ℕ), a < c ^ n ∧ c ^ n < b

Tactic:
⟨Nat.find this, h.trans_le ?_, Nat.find_spec this⟩

Premises used: LT.lt.trans_le, And.intro, Nat.find, Exists.intro, 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
refine : b * c ≤ c ^ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this
⊢ ∃ (n : ℕ), a < c ^ n ∧ c ^ n < b

Tactic:
refine ⟨Nat.find this, h.trans_le ?_, Nat.find_spec this⟩
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
by_contra! : ∀ (H : c ^ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this < b * c), False
⊢ b * c ≤ c ^ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this

Tactic:
by_contra! H
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
H : c ^ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this < b * c
hf : Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this = 0
⊢ 1 < b * c

Tactic:
simp only [hf, pow_zero] at H

Premises used: pow_zero
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
hf : Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this = 0
H : 1 < b * c
⊢ False

Tactic:
(H.trans <| (mul_lt_of_lt_one_right hb₀ hc₁).trans_le hb₁).false

Premises used: LT.lt.trans_le, LT.lt.trans, mul_lt_of_lt_one_right, LT.lt.false
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
hf : Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this = 0
H : 1 < b * c
⊢ False

Tactic:
exact (H.trans <| (mul_lt_of_lt_one_right hb₀ hc₁).trans_le hb₁).false

Premises used: LT.lt.trans_le, LT.lt.trans, mul_lt_of_lt_one_right, LT.lt.false
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
H : c ^ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this < b * c
⊢ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this ≠ 0

Tactic:
have hn : Nat.find this ≠ 0 := by
    intro hf
    simp only [hf, pow_zero] at H
    exact (H.trans <| (mul_lt_of_lt_one_right hb₀ hc₁).trans_le hb₁).false
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
H : c ^ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this < b * c
hn : Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this ≠ 0
⊢ c ^ (Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this).pred < b

Tactic:
rw [(Nat.succ_pred_eq_of_ne_zero hn).symm, pow_succ, mul_lt_mul_iff_left₀ hc₀] at H

Premises used: pow_succ, Nat.succ_pred_eq_of_ne_zero, Eq.symm, mul_lt_mul_iff_left₀
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
H : c ^ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this < b * c
hn : Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this ≠ 0
H₁ : c ^ (Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this).pred < b
⊢ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this ≠ 0

Tactic:
rw [(Nat.succ_pred_eq_of_ne_zero hn).symm, pow_succ, mul_lt_mul_iff_left₀ hc₀] at H

Premises used: pow_succ, Nat.succ_pred_eq_of_ne_zero, Eq.symm, mul_lt_mul_iff_left₀
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
H : c ^ (Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this).pred < b
hn : Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this ≠ 0
⊢ False

Tactic:
Nat.find_min this (Nat.sub_one_lt hn) H

Premises used: Nat.sub_one_lt, Nat.find_min
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ (n : ℕ), c ^ n < b
H : c ^ (Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this).pred < b
hn : Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this ≠ 0
⊢ False

Tactic:
exact Nat.find_min this (Nat.sub_one_lt hn) H

Premises used: Nat.sub_one_lt, Nat.find_min
-- 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
inl : ∀ (ha : a ≤ 0), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
inr : ∀ (ha : 0 < a), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

Tactic:
rcases le_or_gt a 0 with ha | ha

Premises used: le_or_gt, OfNat.ofNat