Theorem: H_P4_2 (FormalBook/Chapter_01.lean)

State before:
x : ℕ
hx : x ≥ 3
hpi3 : π 3 = 2
⊢ ∏ x ∈ Icc 1 x.primeCounting, (↑x + 1) / ↑x = ↑x.primeCounting + 1
Tactic:
rw [prod_Icc_succ_div]
State after:
case hn
x : ℕ
hx : x ≥ 3
hpi3 : π 3 = 2
⊢ 2 ≤ x.primeCounting

State before:
case hn
x : ℕ
hx : x ≥ 3
hpi3 : π 3 = 2
⊢ 2 ≤ x.primeCounting
Tactic:
rw [← hpi3]
State after:
case hn
x : ℕ
hx : x ≥ 3
hpi3 : π 3 = 2
⊢ π 3 ≤ x.primeCounting

State before:
case hn
x : ℕ
hx : x ≥ 3
hpi3 : π 3 = 2
⊢ π 3 ≤ x.primeCounting
Tactic:
refine Monotone.imp monotone_primeCounting ?h
State after:
case h
x : ℕ
hx : x ≥ 3
hpi3 : π 3 = 2
⊢ 3 ≤ x

State before:
case h
x : ℕ
hx : x ≥ 3
hpi3 : π 3 = 2
⊢ 3 ≤ x
Tactic:
linarith
State after:
no goals