awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℤ), x < HDiv.hDiv (α := K) (↑z : K) (↑n : K) ∧ HDiv.hDiv (α := K) (↑z : K) (↑n : K) < y
have 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
Tactic: obtain ⟨z, zh⟩ := exists_floor (x * n)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
have refine : x < HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) ∧ HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) < y
Tactic: refine ⟨z + 1, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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)
⊢ x < HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) ∧ HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) < y
have n0' : LT.lt.{u_4} (α := K) 0 (↑n : K)
Tactic: have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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) ∧ HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) < y
have rw : x < HDiv.hDiv (α := K) (↑(z + 1) : K) (↑n : K) ∧ (↑(z + 1) : K) < y * (↑n : K)
Tactic: rw [div_lt_iff₀ n0']
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
have refine : (↑(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 _), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
⊢ (↑(z + 1) : K) < y * (↑n : K)
have rw : HAdd.hAdd (α := K) (↑z : K) 1 < y * (↑n : K)
Tactic: rw [Int.cast_add, Int.cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
⊢ HAdd.hAdd (α := K) (↑z : K) 1 < y * (↑n : K)
have grw : x * (↑n : K) + 1 < y * (↑n : K)
Tactic: grw [(zh _).1 le_rfl]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 * (↑n : K) + 1 < y * (↑n : K)
have rwa : 1 < y * (↑n : K) - x * (↑n : K)
Tactic: rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff₀' (sub_pos.2 h), one_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
⊢ x * (↑n : K) + 1 < y * (↑n : K)
have rwa₁ : 1 < (y - x) * (↑n : K)
Tactic: rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff₀' (sub_pos.2 h), one_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
⊢ x * (↑n : K) + 1 < y * (↑n : K)
have rwa₂ : 1 / (y - x) < (↑n : K)
Tactic: rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff₀' (sub_pos.2 h), one_div]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℚ), x < (↑q : K) ∧ (↑q : K) < y
have obtain : ∀ (n : ℕ) (nh : (y - x)⁻¹ < (↑n : K)), ∃ (q : ℚ), x < (↑q : K) ∧ (↑q : K) < y
Tactic: obtain ⟨n, nh⟩ := exists_nat_gt (y - x)⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
⊢ ∃ (q : ℚ), x < (↑q : K) ∧ (↑q : K) < y
have 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
Tactic: obtain ⟨z, zh, zh'⟩ := exists_div_btwn h nh
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
have refine_1 : x < (↑(HDiv.hDiv (α := ℚ) (↑z : ℚ) (↑n : ℚ)) : K)
Tactic: refine ⟨(z : ℚ) / n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
⊢ ∃ (q : ℚ), x < (↑q : K) ∧ (↑q : K) < y
have refine_2 : (↑(HDiv.hDiv (α := ℚ) (↑z : ℚ) (↑n : ℚ)) : K) < y
Tactic: refine ⟨(z : ℚ) / n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : K), 0 < q ∧ x < q ^ n ∧ q ^ n < y
have 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
Tactic: have ⟨δ, δ_pos, cont⟩ := uniform_continuous_npow_on_bounded (max 1 y)
    (sub_pos.mpr <| max_lt_iff.mpr ⟨h, hy⟩) n
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
have have : ∀ (m : ℕ) (hm : y / δ + 1 / δ ≤ (↑m : K)), ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
Tactic: have ⟨m, hm⟩ := exists_nat_ge (y / δ + 1 / δ)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
have refine_1 : y ≤ (↑m : K) * δ
Tactic: refine ⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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) * δ
⊢ ∃ (m : ℕ), y ≤ ((↑m : K) * δ) ^ n
have refine_2 : 1 ≤ (↑m : K) * δ
Tactic: refine ⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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) * δ
have refine_1 : y / δ ≤ (↑m : K)
Tactic: rw [← div_le_iff₀ δ_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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) * δ
have refine_2 : 1 / δ ≤ (↑m : K)
Tactic: rw [← div_le_iff₀ δ_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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
⊢ ∃ (q : K), 0 < q ∧ x < q ^ n ∧ q ^ n < y
have ex : ∃ (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
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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
⊢ ∃ (q : K), 0 < q ∧ x < q ^ n ∧ q ^ n < y
have m_pos : 0 < m
Tactic: have m_pos : 0 < m := (Nat.find_pos _).mpr <| by simpa [zero_pow hn] using hy
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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 : K), 0 < q ∧ x < q ^ n ∧ q ^ n < y
have qny : q ^ n < y
Tactic: have qny : q ^ n < y := lt_of_not_ge (Nat.find_min ex <| Nat.pred_lt m_pos.ne')
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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 : K), 0 < q ∧ x < q ^ n ∧ q ^ n < y
have q1y : |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)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 = y - (y - max x 0)
have rw : max x 0 = max x 0
Tactic: rw [sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
have refine : |(↑m : K) * δ - q| ≤ δ
Tactic: refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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) * δ - q| ≤ δ
have rw : |(↑m.pred.succ : 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)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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| ≤ δ
⊢ |(↑m : K) * δ - q| ≤ δ
have rw₁ : |HAdd.hAdd (α := K) (↑m.pred : K) 1 * δ - 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)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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| ≤ δ
⊢ |(↑m : K) * δ - q| ≤ δ
have rw₂ : |(HAdd.hAdd (α := K) (↑m.pred : K) 1 - (↑m.pred : K)) * δ| ≤ δ
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)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)) * δ| ≤ δ
⊢ |(↑m : K) * δ - q| ≤ δ
have rw₃ : |1 * δ| ≤ δ
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)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 * δ| ≤ δ
⊢ |(↑m : K) * δ - q| ≤ δ
have rw₄ : |δ| ≤ δ
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)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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₄ : |δ| ≤ δ
⊢ |(↑m : K) * δ - q| ≤ δ
have rw₅ : δ ≤ δ
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)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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
⊢ ∃ (q : K), 0 < q ∧ x < q ^ n ∧ q ^ n < y
have xqn : 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 ..
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y
have 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
Tactic: obtain ⟨q₂, hx₂, hy₂⟩ := exists_rat_btwn (max_lt h hy)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y
have 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
Tactic: obtain ⟨q₁, hx₁, hq₁₂⟩ := exists_rat_btwn hx₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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)
⊢ ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y
have this : LT.lt.{u_4} (α := K) 0 (↑q₂ : K)
Tactic: have : (0 : K) < q₂ := (le_max_right _ _).trans_lt hx₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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 : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y
have hq₁₃ : q₁ < q₂
Tactic: norm_cast at hq₁₂ this
Cleared hypotheses: hq₁₂, this
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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₂
⊢ ∃ (q : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y
have this₁ : 0 < q₂
Tactic: norm_cast at hq₁₂ this
Cleared hypotheses: hq₁₂, this
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℚ), 0 < q ∧ x < HPow.hPow (α := K) (↑q : K) n ∧ HPow.hPow (α := K) (↑q : K) n < y
have 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
Tactic: obtain ⟨q, hq, hq₁, hq₂⟩ := exists_pow_btwn hn hq₁₂ this
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
have refine_1 : (↑q₁ : K) < HPow.hPow (α := K) (↑q : K) n
Tactic: refine ⟨q, hq, (le_max_left _ _).trans_lt <| hx₁.trans ?_, hy₂.trans' ?_⟩