Theorem: PNat.natPred_succ (LeanSAT/Upstream/ToMathlib.lean)

State before:
n : ℕ+
⊢ natPred n + 1 = ↑n
Tactic:
match n with
| ⟨_+1,_⟩ => simp
State after:
no goals

State before:
n : ℕ+
n✝ : ℕ
property✝ : 0 < n✝ + 1
⊢ natPred { val := n✝ + 1, property := property✝ } + 1 = ↑{ val := n✝ + 1, property := property✝ }
Tactic:
simp
State after:
no goals