Theorem: HTPI.neb_phi (HTPILib/Chap8Part2.lean)

State before:
m : ℕ
⊢ num_elts_below (Set_rp_below m) m (phi m)
Tactic:
rewrite [phi_def]
State after:
m : ℕ
⊢ num_elts_below (Set_rp_below m) m (num_rp_below m m)

State before:
m : ℕ
⊢ num_elts_below (Set_rp_below m) m (num_rp_below m m)
Tactic:
have h1 : m ≤ m := by linarith
State after:
m : ℕ
h1 : m ≤ m
⊢ num_elts_below (Set_rp_below m) m (num_rp_below m m)

State before:
m : ℕ
h1 : m ≤ m
⊢ num_elts_below (Set_rp_below m) m (num_rp_below m m)
Tactic:
show num_elts_below (Set_rp_below m) m (num_rp_below m m) from
  neb_nrpb m h1
State after:
no goals

State before:
m : ℕ
⊢ m ≤ m
Tactic:
linarith
State after:
no goals