Theorem: eq_ratio_of_proportion (Pythagoras/proportion.lean)

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
h : proportion r s t u
⊢ r / s = t / u
Tactic:
obtain ⟨ hr, hs, ht, hu, h⟩ := h
State after:
case intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
⊢ r / s = t / u

State before:
case intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
⊢ r / s = t / u
Tactic:
by_contra hh
State after:
case intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : ¬r / s = t / u
⊢ False

State before:
case intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : ¬r / s = t / u
⊢ False
Tactic:
change r / s ≠ t / u at hh
State after:
case intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
⊢ False

State before:
case intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
⊢ False
Tactic:
by_cases rstu : r / s < t / u
State after:
case pos
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
⊢ False

case neg
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
⊢ False

State before:
case pos
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
⊢ False
Tactic:
have : ∃ n m : ℕ, r / s < n / m ∧ (n:ℝ) / m < t / u ∧ n ≠ 0 ∧ m ≠ 0
State after:
case this
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

case pos
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
this : ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
⊢ False

State before:
case pos
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
this : ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
⊢ False
Tactic:
obtain ⟨n, m, hrs_le_nm, hnm_le_tu, n_ne, m_ne⟩ := this
State after:
case pos.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
⊢ False

State before:
case pos.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
⊢ False
Tactic:
have m_ne_ℝ : (m:ℝ) ≠ 0 := by exact_mod_cast m_ne
State after:
case pos.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
⊢ False

State before:
case pos.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
⊢ False
Tactic:
have mrns : (m:ℝ)*r < n*s → (m:ℝ) * t < n * u := by exact_mod_cast (h m n).2.1
State after:
case pos.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ False

State before:
case pos.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ False
Tactic:
have' := mrns _
State after:
case pos.intro.intro.intro.intro.intro.refine'_2
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ False

case pos.intro.intro.intro.intro.intro.refine'_1
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ ↑m * r < ↑n * s

State before:
case pos.intro.intro.intro.intro.intro.refine'_1
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ ↑m * r < ↑n * s
Tactic:
convert mul_lt_mul hrs_le_nm (by simp : s * m ≤ s * m) (by positivity) (by positivity) using 1
State after:
case h.e'_3
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ ↑m * r = r / s * (s * ↑m)

case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ ↑n * s = ↑n / ↑m * (s * ↑m)

State before:
case h.e'_3
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ ↑m * r = r / s * (s * ↑m)

case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ ↑n * s = ↑n / ↑m * (s * ↑m)
Tactic:
all_goals (field_simp; ring)
State after:
no goals

State before:
case this
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
obtain ⟨q, hq⟩ := exists_rat_btwn rstu
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
have q_gt : (0:ℚ) < q := by
  exact_mod_cast
  calc (0:ℝ) ≤ r / s := by positivity
           r / s < q := hq.1
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
let m := q.den
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
have m_ne : m ≠ 0 := q.den_nz
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
let nn := q.num
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
have nn_gt : 0 < nn := Rat.num_pos_iff_pos.mpr q_gt
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
let n := nn.toNat
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
have n_nn : (n:ℤ) = nn := Int.toNat_of_nonneg (le_of_lt nn_gt)
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ ∃ n m, r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
use n, m
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
have : (n : ℝ) / m = q := by
  have : (nn : ℝ) / m = q := by exact_mod_cast (q.num_den)
  convert this using 2
  exact_mod_cast Int.toNat_of_nonneg (le_of_lt nn_gt)
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑n / ↑m = ↑q
⊢ r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑n / ↑m = ↑q
⊢ r / s < ↑n / ↑m ∧ ↑n / ↑m < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
rw [this]
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑n / ↑m = ↑q
⊢ r / s < ↑q ∧ ↑q < t / u ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑n / ↑m = ↑q
⊢ r / s < ↑q ∧ ↑q < t / u ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
exact ⟨hq.1, hq.2, by linarith, m_ne⟩
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
⊢ 0 < q
Tactic:
exact_mod_cast
calc (0:ℝ) ≤ r / s := by positivity
         r / s < q := hq.1
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
⊢ 0 ≤ r / s
Tactic:
positivity
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ ↑n / ↑m = ↑q
Tactic:
have : (nn : ℝ) / m = q := by exact_mod_cast (q.num_den)
State after:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑nn / ↑m = ↑q
⊢ ↑n / ↑m = ↑q

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑nn / ↑m = ↑q
⊢ ↑n / ↑m = ↑q
Tactic:
convert this using 2
State after:
case h.e'_2.h.e'_5
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑nn / ↑m = ↑q
⊢ ↑n = ↑nn

State before:
case h.e'_2.h.e'_5
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑nn / ↑m = ↑q
⊢ ↑n = ↑nn
Tactic:
exact_mod_cast Int.toNat_of_nonneg (le_of_lt nn_gt)
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ ↑nn / ↑m = ↑q
Tactic:
exact_mod_cast (q.num_den)
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
q : ℚ
hq : r / s < ↑q ∧ ↑q < t / u
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑n / ↑m = ↑q
⊢ n ≠ 0
Tactic:
linarith
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
⊢ ↑m ≠ 0
Tactic:
exact_mod_cast m_ne
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
⊢ ↑m * r < ↑n * s → ↑m * t < ↑n * u
Tactic:
exact_mod_cast (h m n).2.1
State after:
no goals

State before:
case pos.intro.intro.intro.intro.intro.refine'_2
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ False
Tactic:
suffices hh : (n:ℝ) * u < m * t
State after:
case pos.intro.intro.intro.intro.intro.refine'_2
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh✝ : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
hh : ↑n * u < ↑m * t
⊢ False

case hh
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ ↑n * u < ↑m * t

State before:
case pos.intro.intro.intro.intro.intro.refine'_2
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh✝ : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
hh : ↑n * u < ↑m * t
⊢ False
Tactic:
exact (lt_self_iff_false ((m : ℝ) * t)).mp (this.trans hh)
State after:
no goals

State before:
case hh
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ ↑n * u < ↑m * t
Tactic:
convert mul_lt_mul hnm_le_tu (by simp : u * m ≤ u * m) (by positivity) (by positivity) using 1
State after:
case h.e'_3
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ ↑n * u = ↑n / ↑m * (u * ↑m)

case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ ↑m * t = t / u * (u * ↑m)

State before:
case h.e'_3
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ ↑n * u = ↑n / ↑m * (u * ↑m)

case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ ↑m * t = t / u * (u * ↑m)
Tactic:
all_goals (field_simp; ring)
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ u * ↑m ≤ u * ↑m
Tactic:
simp
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ 0 < u * ↑m
Tactic:
positivity
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ 0 ≤ t / u
Tactic:
positivity
State after:
no goals

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ ↑m * t = t / u * (u * ↑m)
Tactic:
(field_simp; ring)
State after:
no goals

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ ↑m * t = t / u * (u * ↑m)
Tactic:
field_simp
State after:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ ↑m * t * u = t * (u * ↑m)

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
this : ↑m * t < ↑n * u
⊢ ↑m * t * u = t * (u * ↑m)
Tactic:
ring
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ s * ↑m ≤ s * ↑m
Tactic:
simp
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ 0 < s * ↑m
Tactic:
positivity
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ 0 ≤ ↑n / ↑m
Tactic:
positivity
State after:
no goals

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ ↑n * s = ↑n / ↑m * (s * ↑m)
Tactic:
(field_simp; ring)
State after:
no goals

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ ↑n * s = ↑n / ↑m * (s * ↑m)
Tactic:
field_simp
State after:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ ↑n * s * ↑m = ↑n * (s * ↑m)

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : r / s < t / u
n m : ℕ
hrs_le_nm : r / s < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < t / u
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑m * r < ↑n * s → ↑m * t < ↑n * u
⊢ ↑n * s * ↑m = ↑n * (s * ↑m)
Tactic:
ring
State after:
no goals

State before:
case neg
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
⊢ False
Tactic:
have turs : t / u < r / s := (or_iff_right rstu).mp (lt_or_lt_iff_ne.mpr hh)
State after:
case neg
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
⊢ False

State before:
case neg
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
⊢ False
Tactic:
have : ∃ n m : ℕ, t / u < n / m ∧ (n:ℝ) / m < r / s ∧ n ≠ 0 ∧ m ≠ 0
State after:
case this
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

case neg
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
this : ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
⊢ False

State before:
case neg
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
this : ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
⊢ False
Tactic:
obtain ⟨n, m, hrs_le_nm, hnm_le_tu, n_ne, m_ne⟩ := this
State after:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
⊢ False

State before:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
⊢ False
Tactic:
have m_ne_ℝ : (m : ℝ) ≠ 0 := by exact_mod_cast m_ne
State after:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
⊢ False

State before:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
⊢ False
Tactic:
have mrns : (n : ℝ) * s < m * r → (n : ℝ) * u < m * t := by exact_mod_cast (h m n).2.2
State after:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ False

State before:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ False
Tactic:
have : (n : ℝ) * s < m * r := by
  convert mul_lt_mul hnm_le_tu (by simp : s * m ≤ s * m) (by positivity) (by positivity) using 1
  all_goals (field_simp; ring)
State after:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this : ↑n * s < ↑m * r
⊢ False

State before:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this : ↑n * s < ↑m * r
⊢ False
Tactic:
have := mrns this
State after:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ False

State before:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ False
Tactic:
have : t * m < n * u := by
  convert mul_lt_mul hrs_le_nm (by simp : u * m ≤ u * m) (by positivity) (by positivity) using 1;
  all_goals (field_simp; ring)
State after:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝¹ : ↑n * s < ↑m * r
this✝ : ↑n * u < ↑m * t
this : t * ↑m < ↑n * u
⊢ False

State before:
case neg.intro.intro.intro.intro.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝¹ : ↑n * s < ↑m * r
this✝ : ↑n * u < ↑m * t
this : t * ↑m < ↑n * u
⊢ False
Tactic:
linarith
State after:
no goals

State before:
case this
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
obtain ⟨q, hq⟩ := exists_rat_btwn turs
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
have q_gt : (0:ℚ) < q := by exact_mod_cast
  calc (0 : ℝ) ≤ t / u := by positivity
         t / u < q := hq.1
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
let m := q.den
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
have m_ne : m ≠ 0 := q.den_nz
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
let nn := q.num
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
have nn_gt : 0 < nn := Rat.num_pos_iff_pos.mpr q_gt
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
let n := nn.toNat
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
have n_nn : (n:ℤ) = nn := Int.toNat_of_nonneg (le_of_lt nn_gt)
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ ∃ n m, t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
use n, m
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
have : (n : ℝ) / m = q := by
  have : (nn : ℝ) / m = q := by exact_mod_cast (q.num_den)
  convert this using 2
  exact_mod_cast Int.toNat_of_nonneg (le_of_lt nn_gt)
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑n / ↑m = ↑q
⊢ t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑n / ↑m = ↑q
⊢ t / u < ↑n / ↑m ∧ ↑n / ↑m < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
rw [this]
State after:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑n / ↑m = ↑q
⊢ t / u < ↑q ∧ ↑q < r / s ∧ n ≠ 0 ∧ m ≠ 0

State before:
case this.intro
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑n / ↑m = ↑q
⊢ t / u < ↑q ∧ ↑q < r / s ∧ n ≠ 0 ∧ m ≠ 0
Tactic:
exact ⟨hq.1, hq.2, by linarith, m_ne⟩
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
⊢ 0 < q
Tactic:
exact_mod_cast
calc (0 : ℝ) ≤ t / u := by positivity
t / u < q := hq.1
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
⊢ 0 ≤ t / u
Tactic:
positivity
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ ↑n / ↑m = ↑q
Tactic:
have : (nn : ℝ) / m = q := by exact_mod_cast (q.num_den)
State after:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑nn / ↑m = ↑q
⊢ ↑n / ↑m = ↑q

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑nn / ↑m = ↑q
⊢ ↑n / ↑m = ↑q
Tactic:
convert this using 2
State after:
case h.e'_2.h.e'_5
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑nn / ↑m = ↑q
⊢ ↑n = ↑nn

State before:
case h.e'_2.h.e'_5
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑nn / ↑m = ↑q
⊢ ↑n = ↑nn
Tactic:
exact_mod_cast Int.toNat_of_nonneg (le_of_lt nn_gt)
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
⊢ ↑nn / ↑m = ↑q
Tactic:
exact_mod_cast (q.num_den)
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
q : ℚ
hq : t / u < ↑q ∧ ↑q < r / s
q_gt : 0 < q
m : ℕ := q.den
m_ne : m ≠ 0
nn : ℤ := q.num
nn_gt : 0 < nn
n : ℕ := Int.toNat nn
n_nn : ↑n = nn
this : ↑n / ↑m = ↑q
⊢ n ≠ 0
Tactic:
linarith
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
⊢ ↑m ≠ 0
Tactic:
exact_mod_cast m_ne
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
⊢ ↑n * s < ↑m * r → ↑n * u < ↑m * t
Tactic:
exact_mod_cast (h m n).2.2
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ ↑n * s < ↑m * r
Tactic:
convert mul_lt_mul hnm_le_tu (by simp : s * m ≤ s * m) (by positivity) (by positivity) using 1
State after:
case h.e'_3
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ ↑n * s = ↑n / ↑m * (s * ↑m)

case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ ↑m * r = r / s * (s * ↑m)

State before:
case h.e'_3
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ ↑n * s = ↑n / ↑m * (s * ↑m)

case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ ↑m * r = r / s * (s * ↑m)
Tactic:
all_goals (field_simp; ring)
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ s * ↑m ≤ s * ↑m
Tactic:
simp
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ 0 < s * ↑m
Tactic:
positivity
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ 0 ≤ r / s
Tactic:
positivity
State after:
no goals

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ ↑m * r = r / s * (s * ↑m)
Tactic:
(field_simp; ring)
State after:
no goals

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ ↑m * r = r / s * (s * ↑m)
Tactic:
field_simp
State after:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ ↑m * r * s = r * (s * ↑m)

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
⊢ ↑m * r * s = r * (s * ↑m)
Tactic:
ring
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ t * ↑m < ↑n * u
Tactic:
convert mul_lt_mul hrs_le_nm (by simp : u * m ≤ u * m) (by positivity) (by positivity) using 1
State after:
case h.e'_3
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ t * ↑m = t / u * (u * ↑m)

case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ ↑n * u = ↑n / ↑m * (u * ↑m)

State before:
case h.e'_3
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ t * ↑m = t / u * (u * ↑m)

case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ ↑n * u = ↑n / ↑m * (u * ↑m)
Tactic:
all_goals (field_simp; ring)
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ u * ↑m ≤ u * ↑m
Tactic:
simp
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ 0 < u * ↑m
Tactic:
positivity
State after:
no goals

State before:
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ 0 ≤ ↑n / ↑m
Tactic:
positivity
State after:
no goals

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ ↑n * u = ↑n / ↑m * (u * ↑m)
Tactic:
(field_simp; ring)
State after:
no goals

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ ↑n * u = ↑n / ↑m * (u * ↑m)
Tactic:
field_simp
State after:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ ↑n * u * ↑m = ↑n * (u * ↑m)

State before:
case h.e'_4
r s t u : ℝ
s_ne : s ≠ 0
u_ne : u ≠ 0
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
h :
  ∀ (n m : ℕ),
    (↑n * r = ↑m * s → ↑n * t = ↑m * u) ∧ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
hh : r / s ≠ t / u
rstu : ¬r / s < t / u
turs : t / u < r / s
n m : ℕ
hrs_le_nm : t / u < ↑n / ↑m
hnm_le_tu : ↑n / ↑m < r / s
n_ne : n ≠ 0
m_ne : m ≠ 0
m_ne_ℝ : ↑m ≠ 0
mrns : ↑n * s < ↑m * r → ↑n * u < ↑m * t
this✝ : ↑n * s < ↑m * r
this : ↑n * u < ↑m * t
⊢ ↑n * u * ↑m = ↑n * (u * ↑m)
Tactic:
ring
State after:
no goals