-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q : α) < y

Proof state:
case intro.intro.hp
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
rw [Rat.cast_div_of_ne_zero, Rat.cast_natCast, Rat.cast_intCast, div_lt_iff₀ n0']

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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.hp
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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.hq
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
case intro.intro.hq
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
subst H

Result:
case intro.intro.hq
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
case intro.intro.hp
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
rw [Rat.den_intCast, Nat.cast_one]

Result:
case intro.intro.hp
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
⊢ ∃ q, x < ↑q ∧ ↑q < y

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

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
refine lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) ?_

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
case intro.intro.hq
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
cases n0

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

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

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
refine ⟨(z + 1 : ℤ) / n, ?_⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
case intro.intro.hq
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
rw [Rat.num_natCast, Int.cast_natCast, Nat.cast_eq_zero] at H

Result:
case intro.intro.hq
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y : α
h : x < y
⊢ ∃ q, x < ↑q ∧ ↑q < y

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

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
x y : α
h : x < y
n : ℕ
nh : (y - x)⁻¹ < ↑n
⊢ ∃ q, x < ↑q ∧ ↑q < y

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

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

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
case intro.intro.hq
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
intro H

Result:
case intro.intro.hq
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

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

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
have n0' := (inv_pos.2 (sub_pos.2 h)).trans nh

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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

Tactic:
have n0 := Nat.cast_pos.1 n0'

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
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