Theorem: nat_zero_min (Katydid/Std/Lists.lean)

State before:
n : ℕ
⊢ min n 0 = 0
Tactic:
cases n with
| zero =>
  simp
| succ n =>
  unfold min
  unfold instMinNat
  unfold minOfLe
  simp only [nonpos_iff_eq_zero, ite_false]
State after:
no goals

State before:
case zero

⊢ min zero 0 = 0
Tactic:
simp
State after:
no goals

State before:
case succ
n : ℕ
⊢ min (succ n) 0 = 0
Tactic:
unfold min
State after:
case succ
n : ℕ
⊢ instMinNat.1 (succ n) 0 = 0

State before:
case succ
n : ℕ
⊢ instMinNat.1 (succ n) 0 = 0
Tactic:
unfold instMinNat
State after:
case succ
n : ℕ
⊢ minOfLe.1 (succ n) 0 = 0

State before:
case succ
n : ℕ
⊢ minOfLe.1 (succ n) 0 = 0
Tactic:
unfold minOfLe
State after:
case succ
n : ℕ
⊢ { min := fun x y => if x ≤ y then x else y }.1 (succ n) 0 = 0

State before:
case succ
n : ℕ
⊢ { min := fun x y => if x ≤ y then x else y }.1 (succ n) 0 = 0
Tactic:
simp only [nonpos_iff_eq_zero, ite_false]
State after:
no goals