Theorem: LoVe.Alternative.Int.IsCanonical_normalize (LoVe/Lectures/LoVe12_LogicalFoundationsOfMathematics_Demo.lean)

State before:
pn : ℕ × ℕ
⊢ IsCanonical (normalize pn)
Tactic:
cases pn with
| mk p n =>
  simp [Int.normalize]
  cases Classical.em (p ≥ n) with
  | inl hpn =>
    simp [*]
    exact Int.IsCanonical.nonneg
  | inr hpn =>
    simp [*]
    exact Int.IsCanonical.nonpos
State after:
no goals

State before:
case mk
p n : ℕ
⊢ IsCanonical (normalize (p, n))
Tactic:
simp [Int.normalize]
State after:
case mk
p n : ℕ
⊢ IsCanonical (if n ≤ p then (p - n, 0) else (0, n - p))

State before:
case mk
p n : ℕ
⊢ IsCanonical (if n ≤ p then (p - n, 0) else (0, n - p))
Tactic:
cases Classical.em (p ≥ n) with
| inl hpn =>
  simp [*]
  exact Int.IsCanonical.nonneg
| inr hpn =>
  simp [*]
  exact Int.IsCanonical.nonpos
State after:
no goals

State before:
case mk.inl
p n : ℕ
hpn : p ≥ n
⊢ IsCanonical (if n ≤ p then (p - n, 0) else (0, n - p))
Tactic:
simp [*]
State after:
case mk.inl
p n : ℕ
hpn : p ≥ n
⊢ IsCanonical (p - n, 0)

State before:
case mk.inl
p n : ℕ
hpn : p ≥ n
⊢ IsCanonical (p - n, 0)
Tactic:
exact Int.IsCanonical.nonneg
State after:
no goals

State before:
case mk.inr
p n : ℕ
hpn : ¬p ≥ n
⊢ IsCanonical (if n ≤ p then (p - n, 0) else (0, n - p))
Tactic:
simp [*]
State after:
case mk.inr
p n : ℕ
hpn : ¬p ≥ n
⊢ IsCanonical (0, n - p)

State before:
case mk.inr
p n : ℕ
hpn : ¬p ≥ n
⊢ IsCanonical (0, n - p)
Tactic:
exact Int.IsCanonical.nonpos
State after:
no goals