awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ x ≤ y ^ (-(m + 1) + 1)
have rwa : x ≤ y ^ (-m + -1 + 1)
Tactic: rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv_comm₀ hx (zpow_pos hyp _)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
⊢ x ≤ y ^ (-(m + 1) + 1)
have rwa₁ : x ≤ y ^ (-m)
Tactic: rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv_comm₀ hx (zpow_pos hyp _)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
⊢ x ≤ y ^ (-(m + 1) + 1)
have rwa₂ : x ≤ (y ^ m)⁻¹
Tactic: rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv_comm₀ hx (zpow_pos hyp _)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℕ), y ^ n < x
have pos : ∀ (y_pos : y ≤ 0), ∃ (n : ℕ), y ^ n < x
Tactic: by_cases! y_pos : y ≤ 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℕ), y ^ n < x
have neg : ∀ (y_pos : 0 < y), ∃ (n : ℕ), y ^ n < x
Tactic: by_cases! y_pos : y ≤ 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℕ), y ^ n < x
have h : HPow.hPow (β := ℕ) y 1 < x
Tactic: use 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ HPow.hPow (β := ℕ) y 1 < x
have h : y < x
Tactic: simp only [pow_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℕ), y ^ n < x
have neg : ∀ (q : ℕ) (hq : x⁻¹ < y⁻¹ ^ q), ∃ (n : ℕ), y ^ n < x
Tactic: rcases pow_unbounded_of_one_lt x⁻¹ ((one_lt_inv₀ y_pos).2 hy) with ⟨q, hq⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ y ^ q < x
have rwa : ∀ (hq : x⁻¹ < (y ^ q)⁻¹), y ^ q < x
Tactic: rwa [inv_pow, inv_lt_inv₀ hx (pow_pos y_pos _)] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ y ^ q < x
have rwa₁ : ∀ (hq : y ^ q < x), y ^ q < x
Tactic: rwa [inv_pow, inv_lt_inv₀ hx (pow_pos y_pos _)] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℕ), y ^ (n + 1) < x ∧ x ≤ y ^ n
have rcases : ∀ (n : ℕ) (hn : y⁻¹ ^ n ≤ x⁻¹) (h'n : x⁻¹ < y⁻¹ ^ (n + 1)), ∃ (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⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
have refine_1 : y ^ (n + 1) < x
Tactic: refine ⟨n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℕ), y ^ (n + 1) < x ∧ x ≤ y ^ n
have refine_2 : x ≤ y ^ n
Tactic: refine ⟨n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
⊢ y ^ (n + 1) < x
have refine_1 : ∀ (h'n : x⁻¹ < (y ^ (n + 1))⁻¹), y ^ (n + 1) < x
Tactic: rwa [inv_pow, inv_lt_inv₀ xpos (pow_pos ypos _)] at h'n
Cleared hypotheses: h'n
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ y ^ (n + 1) < x
have refine_1₁ : ∀ (h'n : y ^ (n + 1) < x), y ^ (n + 1) < x
Tactic: rwa [inv_pow, inv_lt_inv₀ xpos (pow_pos ypos _)] at h'n
Cleared hypotheses: h'n
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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)
⊢ x ≤ y ^ n
have refine_2 : ∀ (hn : (y ^ n)⁻¹ ≤ x⁻¹) (h'n : x⁻¹ < y⁻¹ ^ (n + 1)), x ≤ y ^ n
Tactic: rwa [inv_pow, inv_le_inv₀ (pow_pos ypos _) xpos] at hn
Cleared hypotheses: hn, h'n
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ x ≤ y ^ n
have refine_2₁ : ∀ (hn : x ≤ y ^ n) (h'n : x⁻¹ < y⁻¹ ^ (n + 1)), x ≤ y ^ n
Tactic: rwa [inv_pow, inv_le_inv₀ (pow_pos ypos _) xpos] at hn
Cleared hypotheses: hn, h'n
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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 : ℕ), a < c ^ n ∧ c ^ n < b
have this : ∃ (n : ℕ), c ^ n < b
Tactic: have := exists_pow_lt_of_lt_one hb₀ hc₁
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
have refine : b * c ≤ c ^ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this
Tactic: refine ⟨Nat.find this, h.trans_le ?_, Nat.find_spec this⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ b * c ≤ c ^ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this
have by_contra! : ∀ (H : c ^ Nat.find (p := fun (n : ℕ) ↦ c ^ n < b) this < b * c), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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
⊢ False
have H₁ : 1 < b * c
Tactic: simp only [hf, pow_zero] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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
⊢ False
have hn : 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
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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
⊢ False
have H₁ : 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
Cleared hypotheses: H, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
have inl : ∀ (ha : a ≤ 0), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
Tactic: rcases le_or_gt a 0 with ha | ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
have inr : ∀ (ha : 0 < a), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
Tactic: rcases le_or_gt a 0 with ha | ha
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℤ), a < c ^ n ∧ c ^ n < b
have inl : ∀ (n : ℕ) (hn : c ^ n < b), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
Tactic: obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hb₀ hc₁
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
have inr : ∀ (hb₁ : b ≤ 1), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
Tactic: rcases le_or_gt b 1 with hb₁ | hb₁
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
have inr₁ : ∀ (hb₁ : 1 < b), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
Tactic: rcases le_or_gt b 1 with hb₁ | hb₁
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℤ), a < c ^ n ∧ c ^ n < b
have inr : ∀ (n : ℕ) (hn : 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₁
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
have inr : ∀ (ha₁ : a < 1), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
Tactic: rcases lt_or_ge a 1 with ha₁ | ha₁
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
have inr₁ : ∀ (ha₁ : 1 ≤ a), ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
Tactic: rcases lt_or_ge a 1 with ha₁ | ha₁
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
have inr : a < HPow.hPow (β := ℤ) c 0 ∧ HPow.hPow (β := ℤ) c 0 < b
Tactic: refine ⟨0, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 < HPow.hPow (β := ℤ) c 0 ∧ HPow.hPow (β := ℤ) c 0 < b
have inr : a < 1 ∧ 1 < b
Tactic: rw [zpow_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
have rwa : b⁻¹ * a < c
Tactic: rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (hypothesis)
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
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
have this : b⁻¹ < a⁻¹ * c
Tactic: have : b⁻¹ < a⁻¹ * c := by rwa [lt_inv_mul_iff₀' ha, inv_mul_lt_iff₀ hb₀]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℤ), a < c ^ n ∧ c ^ n < b
have inr : ∀ (n : ℕ) (hn₁ : b⁻¹ < c ^ n) (hn₂ : c ^ n < a⁻¹), ∃ (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₁
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
have inr : a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))
Tactic: refine ⟨-n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℤ))
⊢ ∃ (n : ℤ), a < c ^ n ∧ c ^ n < b
have inr₁ : HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
Tactic: refine ⟨-n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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⁻¹
⊢ a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))
have inr : ∀ (hn₂ : a < (c ^ n)⁻¹), a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))
Tactic: rwa [lt_inv_comm₀ (pow_pos hc₀ n) ha, ← zpow_natCast, ← zpow_neg] at hn₂
Cleared hypotheses: hn₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℤ))
⊢ a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))
have inr₁ : ∀ (hn₂ : 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₂
Cleared hypotheses: hn₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℤ))
⊢ a < HPow.hPow (β := ℤ) c (-(↑n : ℤ))
have inr₂ : ∀ (hn₂ : 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₂
Cleared hypotheses: hn₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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⁻¹
⊢ HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
have inr : ∀ (hn₁ : (c ^ n)⁻¹ < b) (hn₂ : c ^ n < a⁻¹), HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
Tactic: rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁
Cleared hypotheses: hn₁, hn₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
have inr₁ : ∀ (hn₁ : (HPow.hPow (β := ℤ) c (↑n : ℤ))⁻¹ < b) (hn₂ : c ^ n < a⁻¹), HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
Tactic: rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁
Cleared hypotheses: hn₁, hn₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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
⊢ HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
have inr₂ : ∀ (hn₁ : HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b) (hn₂ : c ^ n < a⁻¹), HPow.hPow (β := ℤ) c (-(↑n : ℤ)) < b
Tactic: rwa [inv_lt_comm₀ hb₀ (pow_pos hc₀ n), ← zpow_natCast, ← zpow_neg] at hn₁
Cleared hypotheses: hn₁, 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
H : ∀ (x : K), ∃ (n : ℕ), x < (↑n : K)
x y : K
y0 : 0 < y
n : ℕ
h : x / y < (↑n : K)
⊢ x < n • y
have rwa : ∀ (h : x < (↑n : K) * y), x < n • y
Tactic: rwa [div_lt_iff₀ y0, ← nsmul_eq_mul] at h
Cleared hypotheses: h
-- 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
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
⊢ x < n • y
have rwa₁ : ∀ (h : x < n • y), x < n • y
Tactic: rwa [div_lt_iff₀ y0, ← nsmul_eq_mul] at h
Cleared hypotheses: h
-- 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
⊢ (∀ (x : K), ∃ (n : ℤ), x < (↑n : K)) → Archimedean K
have rw : (∀ (x : K), ∃ (n : ℤ), x < (↑n : K)) → ∀ (x : K), ∃ (n : ℕ), x < (↑n : K)
Tactic: rw [archimedean_iff_nat_lt]
-- 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
h : ∀ (x : K), ∃ (n : ℤ), x < (↑n : K)
x : K
⊢ ∃ (n : ℕ), x < (↑n : K)
have obtain : ∀ (n : ℤ) (h : x < (↑n : K)), ∃ (n : ℕ), x < (↑n : K)
Tactic: obtain ⟨n, h⟩ := h 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
h_1 : ∀ (x : K), ∃ (n : ℤ), x < (↑n : K)
x : K
n : ℤ
h : x < (↑n : K)
⊢ ∃ (n : ℕ), x < (↑n : K)
have refine : LE.le.{u_4} (α := K) (↑n : K) (↑n.toNat : K)
Tactic: refine ⟨n.toNat, h.trans_le ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Basic (goal)
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 : ℚ
⊢ q ≤ (↑q : ℚ)
have rw : q ≤ q
Tactic: rw [Rat.cast_id]