Theorem: Nat.min_zero' (Algdata/Init/Nat.lean)

State before:
n : Nat
⊢ min n 0 = 0
Tactic:
rw [Nat.min_def]
State after:
n : Nat
⊢ (if n ≤ 0 then n else 0) = 0

State before:
n : Nat
⊢ (if n ≤ 0 then n else 0) = 0
Tactic:
if h : n ≤ 0
then cases h; exact if_pos Nat.le.refl
else exact if_neg h
State after:
no goals

State before:
n : Nat
h : n ≤ 0
⊢ (if n ≤ 0 then n else 0) = 0
Tactic:
cases h
State after:
case refl

⊢ (if 0 ≤ 0 then 0 else 0) = 0

State before:
case refl

⊢ (if 0 ≤ 0 then 0 else 0) = 0
Tactic:
exact if_pos Nat.le.refl
State after:
no goals

State before:
n : Nat
h : ¬n ≤ 0
⊢ (if n ≤ 0 then n else 0) = 0
Tactic:
exact if_neg h
State after:
no goals