awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m : ℕ
hm : y / δ + 1 / δ ≤ (↑m : K)
⊢ ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n

Tactic:
⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩

Premises used: Exists.intro, le_self_pow₀, le_trans
-- 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
m : ℕ
hm : y / δ + 1 / δ ≤ (↑m : K)
refine_1 : y ≤ (↑m : K) * δ
refine_2 : 1 ≤ (↑m : K) * δ
⊢ ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n

Tactic:
refine ⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩
-- 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
m : ℕ
hm : y / δ + 1 / δ ≤ (↑m : K)
refine_1 : y / δ ≤ (↑m : K)
⊢ y ≤ (↑m : K) * δ

Tactic:
rw [← div_le_iff₀ δ_pos]

Premises used: div_le_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
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
m : ℕ
hm : y / δ + 1 / δ ≤ (↑m : K)
refine_2 : 1 / δ ≤ (↑m : K)
⊢ 1 ≤ (↑m : K) * δ

Tactic:
rw [← div_le_iff₀ δ_pos]

Premises used: div_le_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
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
m : ℕ
hm : y / δ + 1 / δ ≤ (↑m : K)
⊢ 0 < 1 / δ

Tactic:
positivity
-- 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
m : ℕ
hm : y / δ + 1 / δ ≤ (↑m : K)
⊢ y / δ ≤ (↑m : K)

Tactic:
exact (lt_add_of_pos_right _ <| by positivity).le.trans hm

Premises used: lt_add_of_pos_right, LT.lt.le, LE.le.trans
-- 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
m : ℕ
hm : y / δ + 1 / δ ≤ (↑m : K)
⊢ 0 ≤ y / δ

Tactic:
positivity
-- 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
m : ℕ
hm : y / δ + 1 / δ ≤ (↑m : K)
⊢ 1 / δ ≤ (↑m : K)

Tactic:
exact (le_add_of_nonneg_left <| by positivity).trans hm

Premises used: LE.le.trans, le_add_of_nonneg_left
-- 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
⊢ ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n

Tactic:
have ex : ∃ m : ℕ, y ≤ (m * δ) ^ n := by
    have ⟨m, hm⟩ := exists_nat_ge (y / δ + 1 / δ)
    refine ⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩ <;> rw [← div_le_iff₀ δ_pos]
    · exact (lt_add_of_pos_right _ <| by positivity).le.trans hm
    · exact (le_add_of_nonneg_left <| by positivity).trans hm
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
⊢ ¬y ≤ ((↑0 : K) * δ) ^ n

Tactic:
simpa [zero_pow hn] using hy

Premises used: zero_pow
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
⊢ 0 < m

Tactic:
have m_pos : 0 < m := (Nat.find_pos _).mpr <| by simpa [zero_pow hn] using hy
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
⊢ q ^ n < y

Tactic:
have qny : q ^ n < y := lt_of_not_ge (Nat.find_min ex <| Nat.pred_lt m_pos.ne')
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
qny : q ^ n < y
⊢ 0 ≤ q

Tactic:
positivity
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
qny : q ^ n < y
⊢ |q| < max 1 y

Tactic:
have q1y : |q| < max 1 y := (abs_eq_self.mpr <| by positivity).trans_lt <| lt_max_iff.mpr
    (or_iff_not_imp_left.mpr fun q1 ↦ (le_self_pow₀ (le_of_not_gt q1) hn).trans_lt qny)
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
qny : q ^ n < y
q1y : |q| < max 1 y
rw rw₁ : max x 0 = max x 0
⊢ max x 0 = y - (y - max x 0)

Tactic:
rw [sub_sub_cancel]

Premises used: sub_sub_cancel
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ ((↑m : K) * δ) ^ n - (y - max x 0) < ((↑m : K) * δ) ^ n - (((↑m : K) * δ) ^ n - q ^ n)

Tactic:
sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _

Premises used: le_abs_self, LT.lt.le, LE.le.trans_lt, sub_lt_sub_left
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
qny : q ^ n < y
q1y : |q| < max 1 y
refine : |(↑m : K) * δ - q| ≤ δ
⊢ ((↑m : K) * δ) ^ n - (y - max x 0) < ((↑m : K) * δ) ^ n - (((↑m : K) * δ) ^ n - q ^ n)

Tactic:
refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _

Premises used: le_abs_self, LT.lt.le, LE.le.trans_lt, sub_lt_sub_left
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ 0 ≤ δ

Tactic:
positivity
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
qny : q ^ n < y
q1y : |q| < max 1 y
rw : |(↑m.pred.succ : K) * δ - q| ≤ δ
rw₁ : |HAdd.hAdd (α := K) (↑m.pred : K) 1 * δ - q| ≤ δ
rw₂ : |(HAdd.hAdd (α := K) (↑m.pred : K) 1 - (↑m.pred : K)) * δ| ≤ δ
rw₃ : |1 * δ| ≤ δ
rw₄ : |δ| ≤ δ
rw₅ rw₆ : δ ≤ δ
⊢ |(↑m : K) * δ - q| ≤ δ

Tactic:
rw [← Nat.succ_pred_eq_of_pos m_pos, Nat.cast_succ, ← sub_mul,
          add_sub_cancel_left, one_mul, abs_eq_self.mpr (by positivity)]

Premises used: Iff.mpr, Nat.cast_succ, Nat.succ_pred_eq_of_pos, add_sub_cancel_left, sub_mul, abs_eq_self, one_mul
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
qny : q ^ n < y
q1y : |q| < max 1 y
⊢ max x 0 < q ^ n

Tactic:
have xqn : max x 0 < q ^ n :=
    calc _ = y - (y - max x 0) := by rw [sub_sub_cancel]
      _ ≤ (m * δ) ^ n - (y - max x 0) := sub_le_sub_right (Nat.find_spec ex) _
      _ < (m * δ) ^ n - ((m * δ) ^ n - q ^ n) := by
        refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _
        rw [← Nat.succ_pred_eq_of_pos m_pos, Nat.cast_succ, ← sub_mul,
          add_sub_cancel_left, one_mul, abs_eq_self.mpr (by positivity)]
      _ = q ^ n := sub_sub_cancel ..
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
qny : q ^ n < y
q1y : |q| < max 1 y
xqn : max x 0 < q ^ n
⊢ 0 ≤ q

Tactic:
positivity
-- 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
ex : ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
m : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ y ≤ ((↑n_1 : K) * δ) ^ n) ex
m_pos : 0 < m
q : K := (↑m.pred : K) * δ
qny : q ^ n < y
q1y : |q| < max 1 y
xqn : max x 0 < q ^ n
⊢ ∃ (q : K), 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
exact ⟨q, lt_of_le_of_ne (by positivity) fun q0 ↦
    (le_sup_right.trans_lt xqn).ne <| q0 ▸ (zero_pow hn).symm, le_sup_left.trans_lt xqn, qny⟩
-- 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
obtain :
  ∀ (q₂ : ℚ) (hx₂ : max x 0 < (↑q₂ : K)) (hy₂ : (↑q₂ : K) < y),
    ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y
⊢ ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y

Tactic:
obtain ⟨q₂, hx₂, hy₂⟩ := exists_rat_btwn (max_lt h hy)

Premises used: exists_rat_btwn, max_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
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
obtain :
  ∀ (q₁ : ℚ) (hx₁ : max x 0 < (↑q₁ : K)) (hq₁₂ : LT.lt.{u_4} (α := K) (↑q₁ : K) (↑q₂ : K)),
    ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y
⊢ ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y

Tactic:
obtain ⟨q₁, hx₁, hq₁₂⟩ := exists_rat_btwn hx₂

Premises used: exists_rat_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
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : LT.lt.{u_4} (α := K) (↑q₁ : K) (↑q₂ : K)
⊢ LT.lt.{u_4} (α := K) 0 (↑q₂ : K)

Tactic:
have : (0 : K) < q₂ := (le_max_right _ _).trans_lt hx₂
-- 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
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : LT.lt.{u_4} (α := K) (↑q₁ : K) (↑q₂ : K)
this : LT.lt.{u_4} (α := K) 0 (↑q₂ : K)
⊢ q₁ < q₂

Tactic:
norm_cast at hq₁₂ this
-- 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
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : LT.lt.{u_4} (α := K) (↑q₁ : K) (↑q₂ : K)
this : LT.lt.{u_4} (α := K) 0 (↑q₂ : K)
hq₁₃ : q₁ < q₂
⊢ 0 < q₂

Tactic:
norm_cast at hq₁₂ this
-- 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
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : q₁ < q₂
this : 0 < q₂
obtain :
  ∀ (q : ℚ) (hq : 0 < q) (hq₁ : q₁ < q ^ n) (hq₂ : q ^ n < q₂),
    ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y
⊢ ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y

Tactic:
obtain ⟨q, hq, hq₁, hq₂⟩ := exists_pow_btwn hn hq₁₂ this

Premises used: exists_pow_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
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y

Tactic:
⟨q, hq, (le_max_left _ _).trans_lt <| hx₁.trans ?_, hy₂.trans' ?_⟩

Premises used: LT.lt.trans', And.intro, Exists.intro, LT.lt.trans, le_max_left, LE.le.trans_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
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
refine_1 : (↑q₁ : K) < HPow.hPow (α := K) (↑q : K) n
refine_2 : HPow.hPow (α := K) (↑q : K) n < (↑q₂ : K)
⊢ ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y

Tactic:
refine ⟨q, hq, (le_max_left _ _).trans_lt <| hx₁.trans ?_, hy₂.trans' ?_⟩
-- 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
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
refine_1 refine_1₁ refine_1₂ refine_1₃ :
  ∀ (hy : 0 < y) (hx₂ : max x 0 < (↑q₂ : K)) (hx₁ : max x 0 < (↑q₁ : K)) (hq : 0 < q), q₁ < q ^ n
⊢ (↑q₁ : K) < HPow.hPow (α := K) (↑q : K) n

Tactic:
assumption_mod_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
n : ℕ
hn : n ≠ 0
x y : K
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < (↑q₂ : K)
hy₂ : (↑q₂ : K) < y
q₁ : ℚ
hx₁ : max x 0 < (↑q₁ : K)
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  ∀ (hy : 0 < y) (hx₂ : max x 0 < (↑q₂ : K)) (hx₁ : max x 0 < (↑q₁ : K)) (hq : 0 < q), q ^ n < q₂
⊢ HPow.hPow (α := K) (↑q : K) n < (↑q₂ : K)

Tactic:
assumption_mod_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
h : ∀ (q : ℚ), (↑q : K) < x → (↑q : K) ≤ y
⊢ x ≤ y

Tactic:
le_of_not_gt fun hyx =>
    let ⟨_, hy, hx⟩ := exists_rat_btwn hyx
    hy.not_ge <| h _ hx

Premises used: False, le_of_not_gt, exists_rat_btwn, LT.lt.not_ge, _private.0.le_of_forall_rat_lt_imp_le.match_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
h : ∀ (q : ℚ), y < (↑q : K) → x ≤ (↑q : K)
⊢ x ≤ y

Tactic:
le_of_not_gt fun hyx =>
    let ⟨_, hy, hx⟩ := exists_rat_btwn hyx
    hx.not_ge <| h _ hy

Premises used: False, le_of_not_gt, exists_rat_btwn, LT.lt.not_ge, _private.0.le_of_forall_rat_lt_imp_le.match_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
⊢ x ≤ y ↔ ∀ (q : ℚ), (↑q : K) < x → (↑q : K) ≤ y

Tactic:
⟨fun hxy _ hqx ↦ hqx.le.trans hxy, le_of_forall_rat_lt_imp_le⟩

Premises used: le_of_forall_rat_lt_imp_le, LT.lt.le, Iff.intro, LE.le.trans
-- 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
⊢ x ≤ y ↔ ∀ (q : ℚ), y < (↑q : K) → x ≤ (↑q : K)

Tactic:
⟨fun hxy _ hqx ↦ hxy.trans hqx.le, le_of_forall_lt_rat_imp_le⟩

Premises used: LT.lt.le, le_of_forall_lt_rat_imp_le, Iff.intro, LE.le.trans
-- 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 : ∀ (q : ℚ), (↑q : K) < x ↔ (↑q : K) < y
⊢ x = y

Tactic:
(le_of_forall_rat_lt_imp_le fun q hq => ((h q).1 hq).le).antisymm <|
    le_of_forall_rat_lt_imp_le fun q hq => ((h q).2 hq).le

Premises used: Iff.mpr, le_of_forall_rat_lt_imp_le, LE.le.antisymm, LT.lt.le, 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
h : ∀ (q : ℚ), x < (↑q : K) ↔ y < (↑q : K)
⊢ x = y

Tactic:
(le_of_forall_lt_rat_imp_le fun q hq => ((h q).2 hq).le).antisymm <|
    le_of_forall_lt_rat_imp_le fun q hq => ((h q).1 hq).le

Premises used: Iff.mpr, LE.le.antisymm, LT.lt.le, le_of_forall_lt_rat_imp_le, 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 : K
x0 : 0 < x
⊢ ∃ (q : ℚ), 0 < q ∧ (↑q : K) < x

Tactic:
simpa only [Rat.cast_pos] using exists_rat_btwn x0

Premises used: exists_rat_btwn, Rat.cast_pos
-- 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
ε0 : 0 < ε
⊢ ∃ (q : ℚ), |x - (↑q : K)| < ε

Tactic:
let ⟨q, h₁, h₂⟩ :=
    exists_rat_btwn <| ((sub_lt_self_iff x).2 ε0).trans ((lt_add_iff_pos_left x).2 ε0)
  ⟨q, abs_sub_lt_iff.2 ⟨sub_lt_comm.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩

Premises used: Iff.mpr, sub_lt_comm, abs, HSub.hSub, abs_sub_lt_iff, Exists, Rat.cast, exists_rat_btwn, _private.0.exists_rat_near.match_1, And.intro, LT.lt, Exists.intro, Iff.mp, LT.lt.trans, sub_lt_self_iff, sub_lt_iff_lt_add, lt_add_iff_pos_left
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n ≤ n * m

Tactic:
Nat.le_mul_of_pos_right n m0

Premises used: Nat.le_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℕ
m0 : 0 < m
⊢ n ≤ n * m

Tactic:
exact Nat.le_mul_of_pos_right n m0

Premises used: Nat.le_mul_of_pos_right
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
n m : ℤ
m0 : 0 < m
⊢ (↑n.toNat : ℤ) ≤ n.toNat • m

Tactic:
simpa only [nsmul_eq_mul, zero_add, mul_one] using
          mul_le_mul_of_nonneg_left (Int.add_one_le_iff.2 m0) (Int.natCast_nonneg n.toNat)

Premises used: Iff.mpr, Int.add_one_le_iff, zero_add, nsmul_eq_mul, Int.toNat, mul_one, mul_le_mul_of_nonneg_left, Int.natCast_nonneg
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst : AddCommMonoid M
inst_1 : PartialOrder M
inst_2 : IsOrderedAddMonoid M
inst_3 : Archimedean M
⊢ Archimedean.{u_2} { x : M // 0 ≤ x }

Tactic:
⟨fun x y hy =>
    let ⟨n, hr⟩ := Archimedean.arch (x : M) (hy : (0 : M) < y)
    ⟨n, mod_cast hr⟩⟩

Premises used: Archimedean.mk, cast, Exists, Subtype.coe_le_coe._simp_1, LE.le, _private.0.Nonneg.instArchimedean.match_1, Exists.intro, HSMul.hSMul, Archimedean.arch, Subtype.val
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
inst_4 : ExistsAddOfLE R
⊢ MulArchimedean.{u_3} { x : R // 0 ≤ x }

Tactic:
⟨fun x _ hy ↦ (pow_unbounded_of_one_lt x hy).imp fun _ h ↦ h.le⟩

Premises used: Exists.imp, MulArchimedean.mk, pow_unbounded_of_one_lt
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
⊢ Archimedean ℚ≥0

Tactic:
Nonneg.instArchimedean

Premises used: NNRat, Nonneg.instArchimedean
-- Module: Mathlib.Algebra.Order.Archimedean.Basic
Goal:
G : Type u_1
M : Type u_2
R : Type u_3
K : Type u_4
⊢ MulArchimedean ℚ≥0

Tactic:
Nonneg.instMulArchimedean

Premises used: NNRat, Nonneg.instMulArchimedean