internlm/Lean-Github huggingface dataset:
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_2
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
hh : ↑n * t * s = ↑m * u * s
⊢ ↑n * t = ↑n * t * s / s

case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
hh : ↑n * t * s = ↑m * u * s
⊢ ↑m * u = ↑m * u * s / s
Tactic:
all_goals field_simp
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
hh : ↑n * t * s = ↑m * u * s
⊢ ↑m * u = ↑m * u * s / s
Tactic:
field_simp
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
case hh
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
⊢ ↑n * t * s = ↑m * u * s
Tactic:
convert (congr_arg (fun x => x * u) h) using 1
Proof state after:
case h.e'_2
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
⊢ ↑n * t * s = ↑n * r * u

case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
⊢ ↑m * u * s = ↑m * s * u
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_2
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
⊢ ↑n * t * s = ↑n * r * u
Tactic:
rw [mul_assoc, ← rstu]
Proof state after:
case h.e'_2
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
⊢ ↑n * (r * u) = ↑n * r * u
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_2
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
⊢ ↑n * (r * u) = ↑n * r * u
Tactic:
ring
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r = ↑m * s
⊢ ↑m * u * s = ↑m * s * u
Tactic:
ring
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
case right
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
⊢ (↑n * r < ↑m * s → ↑n * t < ↑m * u) ∧ (↑m * s < ↑n * r → ↑m * u < ↑n * t)
Tactic:
constructor
Proof state after:
case right.left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
⊢ ↑n * r < ↑m * s → ↑n * t < ↑m * u

case right.right
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
⊢ ↑m * s < ↑n * r → ↑m * u < ↑n * t
Theorem: proportion_of_eq_ratio
Proof state before:
case right.left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
⊢ ↑n * r < ↑m * s → ↑n * t < ↑m * u
Tactic:
intro h
Proof state after:
case right.left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ ↑n * t < ↑m * u
Theorem: proportion_of_eq_ratio
Proof state before:
case right.left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ ↑n * t < ↑m * u
Tactic:
suffices hh : (n : ℝ) * t * s < m * u * s
Proof state after:
case right.left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
hh : ↑n * t * s < ↑m * u * s
⊢ ↑n * t < ↑m * u

case hh
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ ↑n * t * s < ↑m * u * s
Theorem: proportion_of_eq_ratio
Proof state before:
case right.left
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
hh : ↑n * t * s < ↑m * u * s
⊢ ↑n * t < ↑m * u
Tactic:
convert mul_lt_mul hh (by simp : (1:ℝ)/s ≤ 1/s) (by positivity)  (by positivity) using 1
Proof state after:
case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
hh : ↑n * t * s < ↑m * u * s
⊢ ↑n * t = ↑n * t * s * (1 / s)

case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
hh : ↑n * t * s < ↑m * u * s
⊢ ↑m * u = ↑m * u * s * (1 / s)
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
hh : ↑n * t * s < ↑m * u * s
⊢ ↑n * t = ↑n * t * s * (1 / s)

case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
hh : ↑n * t * s < ↑m * u * s
⊢ ↑m * u = ↑m * u * s * (1 / s)
Tactic:
all_goals field_simp
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
hh : ↑n * t * s < ↑m * u * s
⊢ 1 / s ≤ 1 / s
Tactic:
simp
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
hh : ↑n * t * s < ↑m * u * s
⊢ 0 < 1 / s
Tactic:
positivity
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
hh : ↑n * t * s < ↑m * u * s
⊢ 0 ≤ ↑m * u * s
Tactic:
positivity
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
hh : ↑n * t * s < ↑m * u * s
⊢ ↑m * u = ↑m * u * s * (1 / s)
Tactic:
field_simp
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
case hh
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ ↑n * t * s < ↑m * u * s
Tactic:
rw [mul_assoc, ← rstu, ← mul_assoc]
Proof state after:
case hh
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ ↑n * r * u < ↑m * u * s
Theorem: proportion_of_eq_ratio
Proof state before:
case hh
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ ↑n * r * u < ↑m * u * s
Tactic:
convert mul_lt_mul h (by simp : u ≤ u) (by positivity) (by positivity) using 1
Proof state after:
case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ ↑m * u * s = ↑m * s * u
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ ↑m * u * s = ↑m * s * u
Tactic:
ring
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ u ≤ u
Tactic:
simp
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ 0 < u
Tactic:
positivity
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑n * r < ↑m * s
⊢ 0 ≤ ↑m * s
Tactic:
positivity
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
case right.right
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
⊢ ↑m * s < ↑n * r → ↑m * u < ↑n * t
Tactic:
intros h
Proof state after:
case right.right
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑m * u < ↑n * t
Theorem: proportion_of_eq_ratio
Proof state before:
case right.right
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑m * u < ↑n * t
Tactic:
suffices hh : (m : ℝ) * u * s < n * t * s
Proof state after:
case right.right
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
hh : ↑m * u * s < ↑n * t * s
⊢ ↑m * u < ↑n * t

case hh
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑m * u * s < ↑n * t * s
Theorem: proportion_of_eq_ratio
Proof state before:
case right.right
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
hh : ↑m * u * s < ↑n * t * s
⊢ ↑m * u < ↑n * t
Tactic:
convert mul_lt_mul hh (by simp : (1:ℝ)/s ≤ 1/s) (by positivity) (by positivity) using 1
Proof state after:
case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
hh : ↑m * u * s < ↑n * t * s
⊢ ↑m * u = ↑m * u * s * (1 / s)

case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
hh : ↑m * u * s < ↑n * t * s
⊢ ↑n * t = ↑n * t * s * (1 / s)
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
hh : ↑m * u * s < ↑n * t * s
⊢ ↑m * u = ↑m * u * s * (1 / s)

case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
hh : ↑m * u * s < ↑n * t * s
⊢ ↑n * t = ↑n * t * s * (1 / s)
Tactic:
all_goals field_simp
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
hh : ↑m * u * s < ↑n * t * s
⊢ 1 / s ≤ 1 / s
Tactic:
simp
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
hh : ↑m * u * s < ↑n * t * s
⊢ 0 < 1 / s
Tactic:
positivity
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
hh : ↑m * u * s < ↑n * t * s
⊢ 0 ≤ ↑n * t * s
Tactic:
positivity
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
hh : ↑m * u * s < ↑n * t * s
⊢ ↑n * t = ↑n * t * s * (1 / s)
Tactic:
field_simp
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
case hh
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑m * u * s < ↑n * t * s
Tactic:
rw [(by ring : (n : ℝ) * t * s = n * (t * s)), ← rstu]
Proof state after:
case hh
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑m * u * s < ↑n * (r * u)
Theorem: proportion_of_eq_ratio
Proof state before:
case hh
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑m * u * s < ↑n * (r * u)
Tactic:
convert mul_lt_mul h (by simp : u ≤ u) (by positivity) (by positivity) using 1
Proof state after:
case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑m * u * s = ↑m * s * u

case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑n * (r * u) = ↑n * r * u
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_3
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑m * u * s = ↑m * s * u

case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑n * (r * u) = ↑n * r * u
Tactic:
all_goals ring
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑n * t * s = ↑n * (t * s)
Tactic:
ring
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ u ≤ u
Tactic:
simp
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ 0 < u
Tactic:
positivity
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ 0 ≤ ↑n * r
Tactic:
positivity
Proof state after:
no goals
Theorem: proportion_of_eq_ratio
Proof state before:
case h.e'_4
r s t u : ℝ
hr : 0 ≤ r
hs : 0 ≤ s
ht : 0 ≤ t
hu : 0 ≤ u
s_ne : s ≠ 0
u_ne : u ≠ 0
n m : ℕ
rstu : r * u = t * s
h : ↑m * s < ↑n * r
⊢ ↑n * (r * u) = ↑n * r * u
Tactic:
ring
Proof state after:
no goals
Theorem: eq_ratio_of_proportion
Proof 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
Proof 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
Theorem: eq_ratio_of_proportion
Proof 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
Proof 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
Theorem: eq_ratio_of_proportion
Proof 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
Proof 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
Theorem: eq_ratio_of_proportion
Proof 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
Proof 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
Theorem: eq_ratio_of_proportion
Proof 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
Proof 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
Theorem: eq_ratio_of_proportion
Proof 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
Proof 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
Theorem: eq_ratio_of_proportion
Proof 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
Proof 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
Theorem: eq_ratio_of_proportion
Proof 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
Proof 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
Theorem: eq_ratio_of_proportion
Proof 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 _
Proof 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
Theorem: eq_ratio_of_proportion
Proof 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
Proof 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)