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

State before:
x y : ℕ+
⊢ ↑x = ↑y ↔ x = y
Tactic:
simp [PNat.val, Subtype.val_inj]
State after:
no goals