Theorem: Nat.minus_plus_one (MLIR/Util/Arith.lean)

State before:
a : ℕ
h : a > 0
⊢ a - 1 + 1 = a
Tactic:
cases a
State after:
case zero
h : zero > 0
⊢ zero - 1 + 1 = zero

case succ
n✝ : ℕ
h : succ n✝ > 0
⊢ succ n✝ - 1 + 1 = succ n✝

State before:
case zero
h : zero > 0
⊢ zero - 1 + 1 = zero

case succ
n✝ : ℕ
h : succ n✝ > 0
⊢ succ n✝ - 1 + 1 = succ n✝
Tactic:
simp at h
State after:
case succ
n✝ : ℕ
h : succ n✝ > 0
⊢ succ n✝ - 1 + 1 = succ n✝

State before:
case succ
n✝ : ℕ
h : succ n✝ > 0
⊢ succ n✝ - 1 + 1 = succ n✝
Tactic:
rfl
State after:
no goals