Theorem: nat_min_zero (Katydid/Std/Simp.lean)

State before:
n : Nat
⊢ min 0 n = 0
Tactic:
unfold min
State after:
n : Nat
⊢ instMinNat.1 0 n = 0

State before:
n : Nat
⊢ instMinNat.1 0 n = 0
Tactic:
unfold instMinNat
State after:
n : Nat
⊢ minOfLe.1 0 n = 0

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

State before:
n : Nat
⊢ { min := fun x y => if x ≤ y then x else y }.1 0 n = 0
Tactic:
simp
State after:
no goals