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

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

State before:
m n : Nat
h : m = n
⊢ compare m n = Ordering.eq
Tactic:
cases h
State after:
case refl
m : Nat
⊢ compare m m = Ordering.eq

State before:
case refl
m : Nat
⊢ compare m m = Ordering.eq
Tactic:
simp [compare, instOrdNat, compareOfLessAndEq]
State after:
no goals