Theorem: IMOSL.IMO2006N3.f_lt_f_of_g (IMOSLLean4/IMO2006/N3/N3.lean)

State before:
a b : ℕ
h : g a * b < g b * a
⊢ f a < f b
Tactic:
unfold f
State after:
a b : ℕ
h : g a * b < g b * a
⊢ ↑↑(g a) / ↑↑a < ↑↑(g b) / ↑↑b

State before:
a b : ℕ
h : g a * b < g b * a
⊢ ↑↑(g a) / ↑↑a < ↑↑(g b) / ↑↑b
Tactic:
rcases a with _ | a
State after:
case zero
b : ℕ
h : g 0 * b < g b * 0
⊢ ↑↑(g 0) / ↑↑0 < ↑↑(g b) / ↑↑b

case succ
b a : ℕ
h : g (a + 1) * b < g b * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g b) / ↑↑b

State before:
case succ
b a : ℕ
h : g (a + 1) * b < g b * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g b) / ↑↑b
Tactic:
rcases b with _ | b
State after:
case succ.zero
a : ℕ
h : g (a + 1) * 0 < g 0 * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g 0) / ↑↑0

case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g (b + 1)) / ↑↑(b + 1)

State before:
case zero
b : ℕ
h : g 0 * b < g b * 0
⊢ ↑↑(g 0) / ↑↑0 < ↑↑(g b) / ↑↑b
Tactic:
rw [g_zero, zero_mul, mul_zero] at h
State after:
case zero
b : ℕ
h : 0 < 0
⊢ ↑↑(g 0) / ↑↑0 < ↑↑(g b) / ↑↑b

State before:
case zero
b : ℕ
h : 0 < 0
⊢ ↑↑(g 0) / ↑↑0 < ↑↑(g b) / ↑↑b
Tactic:
exact absurd rfl h.ne
State after:
no goals

State before:
case succ.zero
a : ℕ
h : g (a + 1) * 0 < g 0 * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g 0) / ↑↑0
Tactic:
rw [g_zero, zero_mul, mul_zero] at h
State after:
case succ.zero
a : ℕ
h : 0 < 0
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g 0) / ↑↑0

State before:
case succ.zero
a : ℕ
h : 0 < 0
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g 0) / ↑↑0
Tactic:
exact absurd rfl h.ne
State after:
no goals

State before:
case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g (b + 1)) / ↑↑(b + 1)
Tactic:
have X (n : ℕ) : 0 < (n.succ : ℤ) := Int.natCast_pos.mpr n.succ_pos
State after:
case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
X : ∀ (n : ℕ), 0 < ↑n.succ
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g (b + 1)) / ↑↑(b + 1)

State before:
case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
X : ∀ (n : ℕ), 0 < ↑n.succ
⊢ ↑↑(g (a + 1)) / ↑↑(a + 1) < ↑↑(g (b + 1)) / ↑↑(b + 1)
Tactic:
rw [Rat.div_lt_div_iff_mul_lt_mul (X a) (X b), ← Nat.cast_mul, ← Nat.cast_mul]
State after:
case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
X : ∀ (n : ℕ), 0 < ↑n.succ
⊢ ↑(g (a + 1) * b.succ) < ↑(g (b + 1) * a.succ)

State before:
case succ.succ
a b : ℕ
h : g (a + 1) * (b + 1) < g (b + 1) * (a + 1)
X : ∀ (n : ℕ), 0 < ↑n.succ
⊢ ↑(g (a + 1) * b.succ) < ↑(g (b + 1) * a.succ)
Tactic:
exact Int.ofNat_lt.mpr h
State after:
no goals