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

Tactic:
obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hb₀ hc₁

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

Tactic:
⟨n, ha.trans_lt (zpow_pos hc₀ _), mod_cast hn⟩

Premises used: zpow_natCast, congrArg, cast, Nat.cast, zpow_pos, And.intro, LT.lt, Exists.intro, congrFun', Eq.symm, 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : a ≤ 0
n : ℕ
hn : c ^ n < b
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

Tactic:
exact ⟨n, ha.trans_lt (zpow_pos hc₀ _), mod_cast hn⟩
-- 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
ha : 0 < a
inr : ∀ (hb₁ : b ≤ 1), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
inr₁ : ∀ (hb₁ : 1 < b), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

Tactic:
rcases le_or_gt b 1 with hb₁ | hb₁

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

Tactic:
obtain ⟨n, hn⟩ := exists_pow_btwn_of_lt_mul h hb₀ hb₁ hc₀ hc₁

Premises used: exists_pow_btwn_of_lt_mul
-- 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
ha : 0 < a
hb₁ : b ≤ 1
n : ℕ
hn : a < c ^ n ∧ c ^ n < b
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

Tactic:
⟨n, mod_cast hn⟩

Premises used: zpow_natCast, congrArg, cast, Nat.cast, And, congr, LT.lt, Exists.intro, congrFun', Eq.symm
-- 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
ha : 0 < a
hb₁ : b ≤ 1
n : ℕ
hn : a < c ^ n ∧ c ^ n < b
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

Tactic:
exact ⟨n, mod_cast hn⟩
-- 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
ha : 0 < a
hb₁ : 1 < b
inr : ∀ (ha₁ : a < 1), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
inr₁ : ∀ (ha₁ : 1 ≤ a), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

Tactic:
rcases lt_or_ge a 1 with ha₁ | ha₁

Premises used: lt_or_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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

Tactic:
⟨0, ?_⟩

Premises used: Exists.intro, 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
inr : a < HPow.hPow (β := ℤ) c 0 ∧ HPow.hPow (β := ℤ) c 0 < b
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

Tactic:
refine ⟨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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
inr : a < 1 ∧ 1 < b
⊢ a < HPow.hPow (β := ℤ) c 0 ∧ HPow.hPow (β := ℤ) c 0 < b

Tactic:
rw [zpow_zero]

Premises used: zpow_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
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ a < 1 ∧ 1 < b

Tactic:
⟨ha₁, hb₁⟩

Premises used: 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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : a < 1
⊢ a < 1 ∧ 1 < b

Tactic:
exact ⟨ha₁, hb₁⟩
-- 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
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
rwa : b⁻¹ * a < c
rwa₁ rwa₂ rwa₃ rwa₄ : a < b * c
⊢ b⁻¹ < a⁻¹ * c

Tactic:
rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]

Premises used: lt_inv_mul_iff₀', inv_mul_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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
⊢ b⁻¹ < a⁻¹ * c

Tactic:
have : b⁻¹ < a⁻¹ * c := by rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]
-- 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
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
inr : ∀ (n : ℕ) (hn₁ : b⁻¹ < c ^ n) (hn₂ : c ^ n < a⁻¹), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

Tactic:
obtain ⟨n, hn₁, hn₂⟩ :=
          exists_pow_btwn_of_lt_mul this (inv_pos_of_pos ha) (inv_le_one_of_one_le₀ ha₁) hc₀ hc₁

Premises used: exists_pow_btwn_of_lt_mul, inv_pos_of_pos, inv_le_one_of_one_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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

Tactic:
⟨-n, ?_, ?_⟩

Premises used: Nat.cast, And.intro, Exists.intro, Neg.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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
inr : a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))
inr₁ : HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b

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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
inr : ∀ (hn₂ : a < (c ^ n)⁻¹), a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))
inr₁ : ∀ (hn₂ : a < (HPow.hPow (β := ℤ) c (↑n : ℤ))⁻¹), a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))
inr₂ inr₃ inr₄ inr₅ : ∀ (hn₂ : a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))), a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))
⊢ a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))

Tactic:
rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂

Premises used: zpow_natCast, pow_pos, lt_inv_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
inst_4 : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hc₀ : 0 < c
hc₁ : c < 1
ha : 0 < a
hb₁ : 1 < b
ha₁ : 1 ≤ a
this : b⁻¹ < a⁻¹ * c
n : ℕ
hn₁ : b⁻¹ < c ^ n
hn₂ : c ^ n < a⁻¹
inr : ∀ (hn₁ : (c ^ n)⁻¹ < b) (hn₂ : c ^ n < a⁻¹), HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
inr₁ : ∀ (hn₁ : (HPow.hPow (β := ℤ) c (↑n : ℤ))⁻¹ < b) (hn₂ : c ^ n < a⁻¹), HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
inr₂ inr₃ inr₄ inr₅ :
  ∀ (hn₁ : HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b) (hn₂ : c ^ n < a⁻¹), HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
⊢ HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b

Tactic:
rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁

Premises used: zpow_natCast, pow_pos, inv_lt_comm₀, zpow_neg
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
H : ∀ (x : K), ∃ (n : ℕ), x < (↑n : K)
x y : K
y0 : 0 < y
n : ℕ
h : x / y < (↑n : K)
rwa : ∀ (h : x < (↑n : K) * y), x < n • y
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : x < n • y), x < n • y
⊢ x < n • y

Tactic:
rwa [div_lt_iff₀ y0, ← nsmul_eq_mul] at h

Premises used: div_lt_iff₀, nsmul_eq_mul
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ Archimedean K ↔ ∀ (x : K), ∃ (n : ℕ), x ≤ (↑n : K)

Tactic:
archimedean_iff_nat_lt.trans
    ⟨fun H x => (H x).imp fun _ => le_of_lt, fun H x =>
      let ⟨n, h⟩ := H x
      ⟨n + 1, lt_of_le_of_lt h (Nat.cast_lt.2 (lt_add_one _))⟩⟩

Premises used: Iff.mpr, lt_of_le_of_lt, lt_add_one, le_of_lt, _private.0.archimedean_iff_nat_le.match_1, Exists, Exists.imp, Nat.cast, archimedean_iff_nat_lt, HAdd.hAdd, LT.lt, Iff.intro, Exists.intro, Iff.trans, OfNat.ofNat, Nat.cast_lt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
rw : (∀ (x : K), ∃ (n : ℤ), x < (↑n : K)) → ∀ (x : K), ∃ (n : ℕ), x < (↑n : K)
⊢ (∀ (x : K), ∃ (n : ℤ), x < (↑n : K)) → Archimedean K

Tactic:
rw [archimedean_iff_nat_lt]

Premises used: archimedean_iff_nat_lt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
h : ∀ (x : K), ∃ (n : ℤ), x < (↑n : K)
x : K
obtain : ∀ (n : ℤ) (h : x < (↑n : K)), ∃ (n : ℕ), x < (↑n : K)
⊢ ∃ (n : ℕ), x < (↑n : K)

Tactic:
obtain ⟨n, h⟩ := h x
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
h_1 : ∀ (x : K), ∃ (n : ℤ), x < (↑n : K)
x : K
n : ℤ
h : x < (↑n : K)
⊢ ∃ (n : ℕ), x < (↑n : K)

Tactic:
⟨n.toNat, h.trans_le ?_⟩

Premises used: LT.lt.trans_le, Exists.intro, Int.toNat
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
h_1 : ∀ (x : K), ∃ (n : ℤ), x < (↑n : K)
x : K
n : ℤ
h : x < (↑n : K)
refine : LE.le.{u_4} (α := K) (↑n : K) (↑n.toNat : K)
⊢ ∃ (n : ℕ), x < (↑n : K)

Tactic:
refine ⟨n.toNat, h.trans_le ?_⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
h_1 : ∀ (x : K), ∃ (n : ℤ), x < (↑n : K)
x : K
n : ℤ
h : x < (↑n : K)
⊢ LE.le.{u_4} (α := K) (↑n : K) (↑n.toNat : K)

Tactic:
mod_cast Int.self_le_toNat _

Premises used: Int.cast, Int.cast_natCast, Int.self_le_toNat, congrArg, cast, LE.le, Int.cast_le._simp_1, Int.toNat, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
h_1 : ∀ (x : K), ∃ (n : ℤ), x < (↑n : K)
x : K
n : ℤ
h : x < (↑n : K)
⊢ LE.le.{u_4} (α := K) (↑n : K) (↑n.toNat : K)

Tactic:
exact mod_cast Int.self_le_toNat _

Premises used: Int.self_le_toNat
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ Archimedean K ↔ ∀ (x : K), ∃ (n : ℤ), x ≤ (↑n : K)

Tactic:
archimedean_iff_int_lt.trans
    ⟨fun H x => (H x).imp fun _ => le_of_lt, fun H x =>
      let ⟨n, h⟩ := H x
      ⟨n + 1, lt_of_le_of_lt h (Int.cast_lt.2 (lt_add_one _))⟩⟩

Premises used: Iff.mpr, Int.cast, lt_of_le_of_lt, lt_add_one, le_of_lt, Exists, Int.cast_lt, Exists.imp, _private.0.archimedean_iff_int_le.match_1, HAdd.hAdd, LT.lt, Iff.intro, Exists.intro, Iff.trans, archimedean_iff_int_lt, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
h_1 : Archimedean K
x : K
n : ℕ
h : x < (↑n : K)
rwa rwa₁ rwa₂ rwa₃ : x < (↑n : K)
⊢ x < (↑(↑n : ℚ) : K)

Tactic:
rwa [Rat.cast_natCast]

Premises used: Rat.cast_natCast
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
⊢ Archimedean K ↔ ∀ (x : K), ∃ (q : ℚ), x ≤ (↑q : K)

Tactic:
archimedean_iff_rat_lt.trans
    ⟨fun H x => (H x).imp fun _ => le_of_lt, fun H x =>
      let ⟨n, h⟩ := H x
      ⟨n + 1, lt_of_le_of_lt h (Rat.cast_lt.2 (lt_add_one _))⟩⟩

Premises used: Iff.mpr, lt_of_le_of_lt, lt_add_one, le_of_lt, Exists, Rat.cast_lt, Rat.cast, Exists.imp, _private.0.archimedean_iff_rat_le.match_1, HAdd.hAdd, LT.lt, Iff.intro, Exists.intro, Iff.trans, archimedean_iff_rat_lt, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
q : ℚ
rw rw₁ : q ≤ q
⊢ q ≤ (↑q : ℚ)

Tactic:
rw [Rat.cast_id]

Premises used: Rat.cast_id
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x : K
⊢ ∃ (q : ℚ), x < (↑q : K)

Tactic:
archimedean_iff_rat_lt.mp ‹_› _

Premises used: Iff.mp, archimedean_iff_rat_lt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x : K
n : ℤ
h rwa rwa₁ rwa₂ rwa₃ : (↑n : K) < x
⊢ (↑(↑n : ℚ) : K) < x

Tactic:
rwa [Rat.cast_intCast]

Premises used: Rat.cast_intCast
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < (↑n : K)
obtain :
  ∀ (z : ℤ) (zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ (↑z_1 : K) ≤ x * (↑n : K)),
    ∃ (z : ℤ), x < HDiv.hDiv (α := K) (↑z : K) (↑n : K) ∧ HDiv.hDiv (α := K) (↑z : K) (↑n : K) < y
⊢ ∃ (z : ℤ), x < HDiv.hDiv (α := K) (↑z : K) (↑n : K) ∧ HDiv.hDiv (α := K) (↑z : K) (↑n : K) < y

Tactic:
obtain ⟨z, zh⟩ := exists_floor (x * n)

Premises used: exists_floor, HMul.hMul, Nat.cast
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ (↑z_1 : K) ≤ x * (↑n : K)
⊢ ∃ (z : ℤ), x < HDiv.hDiv (α := K) (↑z : K) (↑n : K) ∧ HDiv.hDiv (α := K) (↑z : K) (↑n : K) < y

Tactic:
⟨z + 1, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ (↑z_1 : K) ≤ x * (↑n : K)
refine : x < HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) ∧ HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) < y
⊢ ∃ (z : ℤ), x < HDiv.hDiv (α := K) (↑z : K) (↑n : K) ∧ HDiv.hDiv (α := K) (↑z : K) (↑n : K) < y

Tactic:
refine ⟨z + 1, ?_⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ (↑z_1 : K) ≤ x * (↑n : K)
⊢ LT.lt.{u_4} (α := K) 0 (↑n : K)

Tactic:
have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ (↑z_1 : K) ≤ x * (↑n : K)
n0' : LT.lt.{u_4} (α := K) 0 (↑n : K)
rw : x < HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) ∧ (↑(z + 1) : K) < y * (↑n : K)
⊢ x < HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) ∧ HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) < y

Tactic:
rw [div_lt_iff₀ n0']

Premises used: div_lt_iff₀
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ (↑z_1 : K) ≤ x * (↑n : K)
n0' : LT.lt.{u_4} (α := K) 0 (↑n : K)
⊢ x < HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) ∧ (↑(z + 1) : K) < y * (↑n : K)

Tactic:
⟨(lt_div_iff₀ n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), ?_⟩

Premises used: Iff.mpr, lt_div_iff₀, lt_add_one, And.intro, Iff.mp, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ (↑z_1 : K) ≤ x * (↑n : K)
n0' : LT.lt.{u_4} (α := K) 0 (↑n : K)
refine : (↑(z + 1) : K) < y * (↑n : K)
⊢ x < HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) ∧ (↑(z + 1) : K) < y * (↑n : K)

Tactic:
refine ⟨(lt_div_iff₀ n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), ?_⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ (↑z_1 : K) ≤ x * (↑n : K)
n0' : LT.lt.{u_4} (α := K) 0 (↑n : K)
rw : HAdd.hAdd (α := K) (↑z : K) 1 < y * (↑n : K)
⊢ (↑(z + 1) : K) < y * (↑n : K)

Tactic:
rw [Int.cast_add, Int.cast_one]

Premises used: Int.cast_add, Int.cast_one
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ (↑z_1 : K) ≤ x * (↑n : K)
n0' : LT.lt.{u_4} (α := K) 0 (↑n : K)
grw : x * (↑n : K) + 1 < y * (↑n : K)
⊢ HAdd.hAdd (α := K) (↑z : K) 1 < y * (↑n : K)

Tactic:
grw [(zh _).1 le_rfl]

Premises used: le_rfl, Iff.mp
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ (↑z_1 : K) ≤ x * (↑n : K)
n0' : LT.lt.{u_4} (α := K) 0 (↑n : K)
rwa : 1 < y * (↑n : K) - x * (↑n : K)
rwa₁ : 1 < (y - x) * (↑n : K)
rwa₂ : 1 / (y - x) < (↑n : K)
rwa₃ rwa₄ rwa₅ rwa₆ : (y - x)⁻¹ < (↑n : K)
⊢ x * (↑n : K) + 1 < y * (↑n : K)

Tactic:
rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff₀' (sub_pos.2 h), one_div]

Premises used: Iff.mpr, sub_pos, lt_sub_iff_add_lt', sub_mul, div_lt_iff₀', one_div
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
h : x < y
obtain : ∀ (n : ℕ) (nh : (y - x)⁻¹ < (↑n : K)), ∃ (q : ℚ), x < (↑q : K) ∧ (↑q : K) < y
⊢ ∃ (q : ℚ), x < (↑q : K) ∧ (↑q : K) < y

Tactic:
obtain ⟨n, nh⟩ := exists_nat_gt (y - x)⁻¹

Premises used: HSub.hSub, Inv.inv, exists_nat_gt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < (↑n : K)
obtain :
  ∀ (z : ℤ) (zh : x < HDiv.hDiv (α := K) (↑z : K) (↑n : K)) (zh' : HDiv.hDiv (α := K) (↑z : K) (↑n : K) < y),
    ∃ (q : ℚ), x < (↑q : K) ∧ (↑q : K) < y
⊢ ∃ (q : ℚ), x < (↑q : K) ∧ (↑q : K) < y

Tactic:
obtain ⟨z, zh, zh'⟩ := exists_div_btwn h nh

Premises used: exists_div_btwn
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : x < HDiv.hDiv (α := K) (↑z : K) (↑n : K)
zh' : HDiv.hDiv (α := K) (↑z : K) (↑n : K) < y
⊢ ∃ (q : ℚ), x < (↑q : K) ∧ (↑q : K) < y

Tactic:
⟨(z : ℚ) / n, ?_, ?_⟩

Premises used: Int.cast, HDiv.hDiv, Nat.cast, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : x < HDiv.hDiv (α := K) (↑z : K) (↑n : K)
zh' : HDiv.hDiv (α := K) (↑z : K) (↑n : K) < y
refine_1 : x < (↑(HDiv.hDiv (α := ℚ) (↑z : ℚ) (↑n : ℚ)) : K)
refine_2 : (↑(HDiv.hDiv (α := ℚ) (↑z : ℚ) (↑n : ℚ)) : K) < y
⊢ ∃ (q : ℚ), x < (↑q : K) ∧ (↑q : K) < y

Tactic:
refine ⟨(z : ℚ) / n, ?_, ?_⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : x < HDiv.hDiv (α := K) (↑z : K) (↑n : K)
zh' : HDiv.hDiv (α := K) (↑z : K) (↑n : K) < y
⊢ x < (↑(HDiv.hDiv (α := ℚ) (↑z : ℚ) (↑n : ℚ)) : K)

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
h : x < y
n : ℕ
nh : (y - x)⁻¹ < (↑n : K)
z : ℤ
zh : x < HDiv.hDiv (α := K) (↑z : K) (↑n : K)
zh' : HDiv.hDiv (α := K) (↑z : K) (↑n : K) < y
⊢ (↑(HDiv.hDiv (α := ℚ) (↑z : ℚ) (↑n : ℚ)) : K) < y

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
x y : K
h : x ≠ y
⊢ ∃ (q : ℚ), (↑q : K) ∈ uIoo x y

Tactic:
exists_rat_btwn (min_lt_max.mpr h)

Premises used: Iff.mpr, Set.Mem, setOf, exists_rat_btwn, Set.uIoo, min_lt_max, Set.Ioo
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
have :
  ∀ (δ : K) (δ_pos : δ > 0) (cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0),
    ∃ (q : K), 0 < q ∧ x < q ^ n ∧ q ^ n < y
⊢ ∃ (q : K), 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
have ⟨δ, δ_pos, cont⟩ := uniform_continuous_npow_on_bounded (max 1 y)
    (sub_pos.mpr <| max_lt_iff.mpr ⟨h, hy⟩) n
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
K : Type u_4
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : Archimedean K
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
δ : K
δ_pos : δ > 0
cont : ∀ (q r : K), |r| ≤ max 1 y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - max x 0
have : ∀ (m : ℕ) (hm : y / δ + 1 / δ ≤ (↑m : K)), ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
⊢ ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n

Tactic:
have ⟨m, hm⟩ := exists_nat_ge (y / δ + 1 / δ)