Theorem: Nat.compare_lt (Algdata/Init/Nat.lean)

State before:
m n : Nat
⊢ m < n → compare m n = Ordering.lt
Tactic:
intro h
State after:
m n : Nat
h : m < n
⊢ compare m n = Ordering.lt

State before:
m n : Nat
h : m < n
⊢ compare m n = Ordering.lt
Tactic:
simp [compare, instOrdNat, compareOfLessAndEq]
State after:
m n : Nat
h : m < n
⊢ (if m < n then Ordering.lt else if m = n then Ordering.eq else Ordering.gt) = Ordering.lt

State before:
m n : Nat
h : m < n
⊢ (if m < n then Ordering.lt else if m = n then Ordering.eq else Ordering.gt) = Ordering.lt
Tactic:
rw [if_pos h]
State after:
no goals