Theorem: Imo1998P2.clear_denominators (Compfiles/Imo1998P2.lean)

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ (↑b - 1) / (2 * ↑b) ≤ ↑k / ↑a ↔ (b - 1) * a ≤ k * (2 * b)
Tactic:
rw [div_le_div_iff]
State after:
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ (↑b - 1) * ↑a ≤ ↑k * (2 * ↑b) ↔ (b - 1) * a ≤ k * (2 * b)

case b0
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ 0 < 2 * ↑b

case d0
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ 0 < ↑a

State before:
case b0
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ 0 < 2 * ↑b

case d0
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ 0 < ↑a
Tactic:
all_goals simp [ha, hb]
State after:
no goals

State before:
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ (↑b - 1) * ↑a ≤ ↑k * (2 * ↑b) ↔ (b - 1) * a ≤ k * (2 * b)
Tactic:
convert Nat.cast_le (α := ℚ)
State after:
case h.e'_1.h.e'_3
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ (↑b - 1) * ↑a = ↑((b - 1) * a)

case h.e'_1.h.e'_4
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ ↑k * (2 * ↑b) = ↑(k * (2 * b))

State before:
case h.e'_1.h.e'_3
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ (↑b - 1) * ↑a = ↑((b - 1) * a)
Tactic:
aesop
State after:
no goals

State before:
case h.e'_1.h.e'_4
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ ↑k * (2 * ↑b) = ↑(k * (2 * b))
Tactic:
norm_cast
State after:
no goals

State before:
case d0
C : Type u_1
J : Type u_2
r : C → J → Prop
a b k : ℕ
ha : 0 < a
hb : 0 < b
⊢ 0 < ↑a
Tactic:
simp [ha, hb]
State after:
no goals