Theorem: four_le_seven (PnP2023/Lec_01_11/NatLe.lean)

State before:
⊢ 4 ≤ 7
Tactic:
apply Nat.le_step
State after:
case h

⊢ 4 ≤ 6

State before:
case h

⊢ 4 ≤ 6
Tactic:
apply Nat.le_step
State after:
case h.h

⊢ 4 ≤ 5

State before:
case h.h

⊢ 4 ≤ 5
Tactic:
apply Nat.le_step
State after:
case h.h.h

⊢ 4 ≤ 4

State before:
case h.h.h

⊢ 4 ≤ 4
Tactic:
apply Nat.le_refl
State after:
no goals