[GOAL]
α : Type u_1
inst✝¹ : OrderedAddCommGroup α
inst✝ : Archimedean α
x y : αᵒᵈ
hy : 0 < y
n : ℕ
hn : -↑ofDual x ≤ n • -y
⊢ x ≤ n • y
[PROOFSTEP]
rwa [neg_nsmul, neg_le_neg_iff] at hn 
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
let s : Set ℤ := {n : ℤ | n • a ≤ g}
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
obtain ⟨k, hk : -g ≤ k • a⟩ := Archimedean.arch (-g) ha
[GOAL]
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
have h_ne : s.Nonempty := ⟨-k, by simpa using neg_le_neg hk⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
⊢ -↑k ∈ s
[PROOFSTEP]
simpa using neg_le_neg hk
[GOAL]
case intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k : ℕ
hk : -g ≤ k • a
h_ne : Set.Nonempty s
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
obtain ⟨k, hk⟩ := Archimedean.arch g ha
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
have h_bdd : ∀ n ∈ s, n ≤ (k : ℤ) := by
  intro n hn
  apply (zsmul_le_zsmul_iff ha).mp
  rw [← coe_nat_zsmul] at hk 
  exact le_trans hn hk
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
⊢ ∀ (n : ℤ), n ∈ s → n ≤ ↑k
[PROOFSTEP]
intro n hn
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
n : ℤ
hn : n ∈ s
⊢ n ≤ ↑k
[PROOFSTEP]
apply (zsmul_le_zsmul_iff ha).mp
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
n : ℤ
hn : n ∈ s
⊢ n • a ≤ ↑k • a
[PROOFSTEP]
rw [← coe_nat_zsmul] at hk 
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ ↑k • a
n : ℤ
hn : n ∈ s
⊢ n • a ≤ ↑k • a
[PROOFSTEP]
exact le_trans hn hk
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
obtain ⟨m, hm, hm'⟩ := Int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
have hm'' : g < (m + 1) • a := by
  contrapose! hm'
  exact ⟨m + 1, hm', lt_add_one _⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
⊢ g < (m + 1) • a
[PROOFSTEP]
contrapose! hm'
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : (m + 1) • a ≤ g
⊢ ∃ z, z ∈ {n | n • a ≤ g} ∧ m < z
[PROOFSTEP]
exact ⟨m + 1, hm', lt_add_one _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
⊢ ∃! k, k • a ≤ g ∧ g < (k + 1) • a
[PROOFSTEP]
refine' ⟨m, ⟨hm, hm''⟩, fun n hn => (hm' n hn.1).antisymm <| Int.le_of_lt_add_one _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
n : ℤ
hn : (fun k => k • a ≤ g ∧ g < (k + 1) • a) n
⊢ m < n + 1
[PROOFSTEP]
rw [← zsmul_lt_zsmul_iff ha]
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
s : Set ℤ := {n | n • a ≤ g}
k✝ : ℕ
hk✝ : -g ≤ k✝ • a
h_ne : Set.Nonempty s
k : ℕ
hk : g ≤ k • a
h_bdd : ∀ (n : ℤ), n ∈ s → n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ (z : ℤ), z ∈ s → z ≤ m
hm'' : g < (m + 1) • a
n : ℤ
hn : (fun k => k • a ≤ g ∧ g < (k + 1) • a) n
⊢ m • a < (n + 1) • a
[PROOFSTEP]
exact lt_of_le_of_lt hm hn.2
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
g : α
⊢ ∃! k, 0 ≤ g - k • a ∧ g - k • a < a
[PROOFSTEP]
simpa only [sub_nonneg, add_zsmul, one_zsmul, sub_lt_iff_lt_add'] using existsUnique_zsmul_near_of_pos ha g
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
b c : α
⊢ ∃! m, b - m • a ∈ Ico c (c + a)
[PROOFSTEP]
simpa only [mem_Ico, le_sub_iff_add_le, zero_add, add_comm c, sub_lt_iff_lt_add', add_assoc] using
  existsUnique_zsmul_near_of_pos' ha (b - c)
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
b c : α
⊢ ∃! x, b + ↑(Equiv.neg ℤ) x • a ∈ Ico c (c + a)
[PROOFSTEP]
simpa only [Equiv.neg_apply, mem_Ico, neg_zsmul, ← sub_eq_add_neg, le_sub_iff_add_le, zero_add, add_comm c,
  sub_lt_iff_lt_add', add_assoc] using existsUnique_zsmul_near_of_pos' ha (b - c)
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
b c : α
⊢ ∃! x, b + ↑(Equiv.addRight 1) x • a ∈ Ioc c (c + a)
[PROOFSTEP]
simpa only [add_zsmul, sub_lt_iff_lt_add', le_sub_iff_add_le', ← add_assoc, and_comm, mem_Ioc, Equiv.coe_addRight,
  one_zsmul, add_le_add_iff_right] using existsUnique_zsmul_near_of_pos ha (c - b)
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
a : α
ha : 0 < a
b c : α
⊢ ∃! x, b - ↑(Equiv.neg ℤ) x • a ∈ Ioc c (c + a)
[PROOFSTEP]
simpa only [Equiv.neg_apply, neg_zsmul, sub_neg_eq_add] using existsUnique_add_zsmul_mem_Ioc ha b c
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Archimedean α
x : α
n : ℕ
hn : x < n • 1
⊢ x < ↑n
[PROOFSTEP]
rwa [← nsmul_one]
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Archimedean α
x : α
⊢ ∃ n, x ≤ ↑n
[PROOFSTEP]
nontriviality α
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Archimedean α
x : α
✝ : Nontrivial α
⊢ ∃ n, x ≤ ↑n
[PROOFSTEP]
exact (Archimedean.arch x one_pos).imp fun n h => by rwa [← nsmul_one]
[GOAL]
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Archimedean α
x : α
✝ : Nontrivial α
n : ℕ
h : x ≤ n • 1
⊢ x ≤ ↑n
[PROOFSTEP]
rwa [← nsmul_one]
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedSemiring α
inst✝ : Archimedean α
x y : α
hy : 0 < y
this : 0 ≤ 1 + y
n : ℕ
h : x ≤ n • y
⊢ (1 + y) ^ n = (y + 1) ^ n
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℕ
h : x < ↑n
⊢ x < ↑↑n
[PROOFSTEP]
rwa [Int.cast_ofNat]
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℤ
h : -x < ↑n
⊢ ↑(-n) < x
[PROOFSTEP]
rw [Int.cast_neg]
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
n : ℤ
h : -x < ↑n
⊢ -↑n < x
[PROOFSTEP]
exact neg_lt.1 h
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
[PROOFSTEP]
haveI := Classical.propDecidable
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this : (a : Prop) → Decidable a
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
[PROOFSTEP]
have : ∃ ub : ℤ, (ub : α) ≤ x ∧ ∀ z : ℤ, (z : α) ≤ x → z ≤ ub :=
  Int.exists_greatest_of_bdd
    (let ⟨n, hn⟩ := exists_int_gt x
    ⟨n, fun z h' => Int.cast_le.1 <| le_trans h' <| le_of_lt hn⟩)
    (let ⟨n, hn⟩ := exists_int_lt x
    ⟨n, le_of_lt hn⟩)
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
⊢ ∃ fl, ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x
[PROOFSTEP]
refine' this.imp fun fl h z => _
[GOAL]
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl : ℤ
h : ↑fl ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
z : ℤ
⊢ z ≤ fl ↔ ↑z ≤ x
[PROOFSTEP]
cases' h with h₁ h₂
[GOAL]
case intro
α : Type u_1
inst✝¹ : StrictOrderedRing α
inst✝ : Archimedean α
x : α
this✝ : (a : Prop) → Decidable a
this : ∃ ub, ↑ub ≤ x ∧ ∀ (z : ℤ), ↑z ≤ x → z ≤ ub
fl z : ℤ
h₁ : ↑fl ≤ x
h₂ : ∀ (z : ℤ), ↑z ≤ x → z ≤ fl
⊢ z ≤ fl ↔ ↑z ≤ x
[PROOFSTEP]
exact ⟨fun h => le_trans (Int.cast_le.2 h) h₁, h₂ z⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
[PROOFSTEP]
have h : ∃ n : ℕ, x < y ^ n := pow_unbounded_of_one_lt _ hy
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
[PROOFSTEP]
classical exact
  let n := Nat.find h
  have hn : x < y ^ n := Nat.find_spec h
  have hnp : 0 < n := pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn ; exact not_le_of_gt hn hx
  have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
  have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
  ⟨Nat.pred n, le_of_not_lt (Nat.find_min h hltn), by rwa [hnsp]⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
[PROOFSTEP]
exact
  let n := Nat.find h
  have hn : x < y ^ n := Nat.find_spec h
  have hnp : 0 < n := pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn ; exact not_le_of_gt hn hx
  have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
  have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
  ⟨Nat.pred n, le_of_not_lt (Nat.find_min h hltn), by rwa [hnsp]⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hn0 : n = 0
⊢ False
[PROOFSTEP]
rw [hn0, pow_zero] at hn 
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < 1
hn0 : n = 0
⊢ False
[PROOFSTEP]
exact not_le_of_gt hn hx
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hnp : 0 < n
hnsp : Nat.pred n + 1 = n
hltn : Nat.pred n < n
⊢ x < y ^ (Nat.pred n + 1)
[PROOFSTEP]
rwa [hnsp]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))
[PROOFSTEP]
classical exact
  let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
  have he : ∃ m : ℤ, y ^ m ≤ x :=
    ⟨-N,
      le_of_lt
        (by
          rw [zpow_neg y ↑N, zpow_ofNat]
          exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN)⟩
  let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
  have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b :=
    ⟨M, fun m hm =>
      le_of_not_lt fun hlt =>
        not_lt_of_ge (zpow_le_of_le hy.le hlt.le) (lt_of_le_of_lt hm (by rwa [← zpow_ofNat] at hM ))⟩
  let ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
  ⟨n, hn₁, lt_of_not_ge fun hge => not_le_of_gt (Int.lt_succ _) (hn₂ _ hge)⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
⊢ ∃ n, x ∈ Ico (y ^ n) (y ^ (n + 1))
[PROOFSTEP]
exact
  let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy
  have he : ∃ m : ℤ, y ^ m ≤ x :=
    ⟨-N,
      le_of_lt
        (by
          rw [zpow_neg y ↑N, zpow_ofNat]
          exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN)⟩
  let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy
  have hb : ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b :=
    ⟨M, fun m hm =>
      le_of_not_lt fun hlt =>
        not_lt_of_ge (zpow_le_of_le hy.le hlt.le) (lt_of_le_of_lt hm (by rwa [← zpow_ofNat] at hM ))⟩
  let ⟨n, hn₁, hn₂⟩ := Int.exists_greatest_of_bdd hb he
  ⟨n, hn₁, lt_of_not_ge fun hge => not_le_of_gt (Int.lt_succ _) (hn₂ _ hge)⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ y ^ (-↑N) < x
[PROOFSTEP]
rw [zpow_neg y ↑N, zpow_ofNat]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
⊢ (y ^ N)⁻¹ < x
[PROOFSTEP]
exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
N : ℕ
hN : x⁻¹ < y ^ N
he : ∃ m, y ^ m ≤ x
M : ℕ
hM : x < y ^ M
m : ℤ
hm : y ^ m ≤ x
hlt : ↑M < m
⊢ x < y ^ ↑M
[PROOFSTEP]
rwa [← zpow_ofNat] at hM 
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ y ^ (-(m + 1)) < x
[PROOFSTEP]
rwa [zpow_neg, inv_lt (zpow_pos_of_pos hyp _) hx]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : 1 < y
m : ℤ
hle : y ^ m ≤ x⁻¹
hlt : x⁻¹ < y ^ (m + 1)
hyp : 0 < y
⊢ x ≤ y ^ (-(m + 1) + 1)
[PROOFSTEP]
rwa [neg_add, neg_add_cancel_right, zpow_neg, le_inv hx (zpow_pos_of_pos hyp _)]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
⊢ ∃ n, y ^ n < x
[PROOFSTEP]
by_cases y_pos : y ≤ 0
[GOAL]
case pos
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ ∃ n, y ^ n < x
[PROOFSTEP]
use 1
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y ^ 1 < x
[PROOFSTEP]
simp only [pow_one]
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y < x
[PROOFSTEP]
linarith
[GOAL]
case neg
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : ¬y ≤ 0
⊢ ∃ n, y ^ n < x
[PROOFSTEP]
rw [not_le] at y_pos 
[GOAL]
case neg
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
⊢ ∃ n, y ^ n < x
[PROOFSTEP]
rcases pow_unbounded_of_one_lt x⁻¹ (one_lt_inv y_pos hy) with ⟨q, hq⟩
[GOAL]
case neg.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ ∃ n, y ^ n < x
[PROOFSTEP]
exact ⟨q, by rwa [inv_pow, inv_lt_inv hx (pow_pos y_pos _)] at hq ⟩
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ y ^ q < x
[PROOFSTEP]
rwa [inv_pow, inv_lt_inv hx (pow_pos y_pos _)] at hq 
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
xpos : 0 < x
hx : x ≤ 1
ypos : 0 < y
hy : y < 1
⊢ ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n
[PROOFSTEP]
rcases exists_nat_pow_near (one_le_inv_iff.2 ⟨xpos, hx⟩) (one_lt_inv_iff.2 ⟨ypos, hy⟩) with ⟨n, hn, h'n⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
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
[PROOFSTEP]
refine' ⟨n, _, _⟩
[GOAL]
case intro.intro.refine'_1
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
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
[PROOFSTEP]
rwa [inv_pow, inv_lt_inv xpos (pow_pos ypos _)] at h'n 
[GOAL]
case intro.intro.refine'_2
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε : α
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
[PROOFSTEP]
rwa [inv_pow, inv_le_inv (pow_pos ypos _) xpos] at hn 
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y ε x : α
n : ℕ
h : x < ↑n
⊢ x < ↑↑n
[PROOFSTEP]
rwa [Rat.cast_coe_nat]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y ε x : α
n : ℤ
h : ↑n < x
⊢ ↑↑n < x
[PROOFSTEP]
rwa [Rat.cast_coe_int]
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
⊢ ∃ q, x < ↑q ∧ ↑q < y
[PROOFSTEP]
cases' exists_nat_gt (y - x)⁻¹ with n nh
[GOAL]
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
⊢ ∃ q, x < ↑q ∧ ↑q < y
[PROOFSTEP]
cases' exists_floor (x * n) with z zh
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
⊢ ∃ q, x < ↑q ∧ ↑q < y
[PROOFSTEP]
refine' ⟨(z + 1 : ℤ) / n, _⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
⊢ x < ↑(↑(z + 1) / ↑n) ∧ ↑(↑(z + 1) / ↑n) < y
[PROOFSTEP]
have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ x < ↑(↑(z + 1) / ↑n) ∧ ↑(↑(z + 1) / ↑n) < y
[PROOFSTEP]
have n0 := Nat.cast_pos.1 n0'
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ x < ↑(↑(z + 1) / ↑n) ∧ ↑(↑(z + 1) / ↑n) < y
[PROOFSTEP]
rw [Rat.cast_div_of_ne_zero, Rat.cast_coe_nat, Rat.cast_coe_int, div_lt_iff n0']
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ x < ↑(z + 1) / ↑n ∧ ↑(z + 1) < y * ↑n
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑(z + 1)).den ≠ 0
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).num ≠ 0
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).den ≠ 0
[PROOFSTEP]
refine' ⟨(lt_div_iff n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), _⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(z + 1) < y * ↑n
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑(z + 1)).den ≠ 0
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).num ≠ 0
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).den ≠ 0
[PROOFSTEP]
rw [Int.cast_add, Int.cast_one]
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑z + 1 < y * ↑n
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑(z + 1)).den ≠ 0
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).num ≠ 0
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).den ≠ 0
[PROOFSTEP]
refine' lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) _
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ x * ↑n + 1 < y * ↑n
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑(z + 1)).den ≠ 0
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).num ≠ 0
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).den ≠ 0
[PROOFSTEP]
rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff' (sub_pos.2 h), one_div]
[GOAL]
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑(z + 1)).den ≠ 0
[PROOFSTEP]
rw [Rat.coe_int_den, Nat.cast_one]
[GOAL]
case intro.intro.md
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).num ≠ 0
[PROOFSTEP]
intro H
[GOAL]
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
H : ↑(↑n).num = 0
⊢ False
[PROOFSTEP]
rw [Rat.coe_nat_num, Int.cast_ofNat, Nat.cast_eq_zero] at H 
[GOAL]
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
H : n = 0
⊢ False
[PROOFSTEP]
subst H
[GOAL]
case intro.intro.nn
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
z : ℤ
nh : (y - x)⁻¹ < ↑0
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑0
n0' : 0 < ↑0
n0 : 0 < 0
⊢ False
[PROOFSTEP]
cases n0
[GOAL]
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ ↑(↑n).den ≠ 0
[PROOFSTEP]
rw [Rat.coe_nat_den, Nat.cast_one]
[GOAL]
case intro.intro.nd
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y✝ ε x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
n0 : 0 < n
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
⊢ ∃ n, 1 / (↑n + 1) < ε
[PROOFSTEP]
cases' exists_nat_gt (1 / ε) with n hn
[GOAL]
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ∃ n, 1 / (↑n + 1) < ε
[PROOFSTEP]
use n
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / (↑n + 1) < ε
[PROOFSTEP]
rw [div_lt_iff, ← div_lt_iff' hε]
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 1 / ε < ↑n + 1
[PROOFSTEP]
apply hn.trans
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ ↑n < ↑n + 1
[PROOFSTEP]
simp [zero_lt_one]
[GOAL]
case h
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y ε✝ ε : α
hε : 0 < ε
n : ℕ
hn : 1 / ε < ↑n
⊢ 0 < ↑n + 1
[PROOFSTEP]
exact n.cast_add_one_pos
[GOAL]
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x✝ y ε x : α
x0 : 0 < x
⊢ ∃ q, 0 < q ∧ ↑q < x
[PROOFSTEP]
simpa only [Rat.cast_pos] using exists_rat_btwn x0
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
H : ∀ (x : α), ∃ n, x < ↑n
x y : α
y0 : 0 < y
n : ℕ
h : x / y < ↑n
⊢ x < n • y
[PROOFSTEP]
rwa [div_lt_iff y0, ← nsmul_eq_mul] at h 
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
⊢ (∀ (x : α), ∃ n, x < ↑n) → Archimedean α
[PROOFSTEP]
rw [archimedean_iff_nat_lt]
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
⊢ (∀ (x : α), ∃ n, x < ↑n) → ∀ (x : α), ∃ n, x < ↑n
[PROOFSTEP]
intro h x
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
h : ∀ (x : α), ∃ n, x < ↑n
x : α
⊢ ∃ n, x < ↑n
[PROOFSTEP]
obtain ⟨n, h⟩ := h x
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
h✝ : ∀ (x : α), ∃ n, x < ↑n
x : α
n : ℤ
h : x < ↑n
⊢ ∃ n, x < ↑n
[PROOFSTEP]
refine' ⟨n.toNat, h.trans_le _⟩
[GOAL]
case intro
α : Type u_1
inst✝ : LinearOrderedField α
h✝ : ∀ (x : α), ∃ n, x < ↑n
x : α
n : ℤ
h : x < ↑n
⊢ ↑n ≤ ↑(toNat n)
[PROOFSTEP]
exact_mod_cast Int.self_le_toNat _
[GOAL]
α : Type u_1
inst✝ : LinearOrderedField α
H : ∀ (x : α), ∃ q, x < ↑q
x : α
q : ℚ
h : x < ↑q
⊢ ↑q ≤ ↑⌈q⌉₊
[PROOFSTEP]
simpa only [Rat.cast_coe_nat] using (@Rat.cast_le α _ _ _).2 (Nat.le_ceil _)
[GOAL]
α : Type u_1
n m : ℕ
m0 : 0 < m
⊢ n ≤ n • m
[PROOFSTEP]
rw [← mul_one n, smul_eq_mul, mul_assoc, one_mul m]
[GOAL]
α : Type u_1
n m : ℕ
m0 : 0 < m
⊢ n * 1 ≤ n * m
[PROOFSTEP]
exact Nat.mul_le_mul_left n (by linarith)
[GOAL]
α : Type u_1
n m : ℕ
m0 : 0 < m
⊢ 1 ≤ m
[PROOFSTEP]
linarith
[GOAL]
α : Type u_1
n m : ℤ
m0 : 0 < m
⊢ ↑(toNat n) ≤ toNat n • m
[PROOFSTEP]
simpa only [nsmul_eq_mul, zero_add, mul_one] using
  mul_le_mul_of_nonneg_left (Int.add_one_le_iff.2 m0) (Int.ofNat_zero_le n.toNat)
[GOAL]
α : Type u_1
q : ℚ
⊢ q ≤ ↑q
[PROOFSTEP]
rw [Rat.cast_id]
[GOAL]
α✝ : Type u_1
α : Type ?u.91487
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
⊢ Archimedean α
[PROOFSTEP]
rw [archimedean_iff_int_le]
[GOAL]
α✝ : Type u_1
α : Type ?u.91487
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
⊢ ∀ (x : α), ∃ n, x ≤ ↑n
[PROOFSTEP]
exact fun x => ⟨⌈x⌉, Int.le_ceil x⟩
