fix: use Nat.lt_wfRel.wf instead of IsWellFounded.fix.proof_1 in Part…

…ENat.lt_wf (#2348)

Simplifies the proof and makes it more closely match the [mathlib3 version](https://github.com/leanprover-community/mathlib/blob/e7286cac412124bcb9114d1403c43c8a0f644f09/src/data/nat/part_enat.lean#L490-L496).

Avoids using the `proof_1` lemma, which is automatically generated [by this code in core](https://github.com/leanprover/lean4/blob/c826168cfa79d421c0723d5fbdd840595c29fe3a/src/Lean/Meta/AbstractNestedProofs.lean#L67-L69). It's probably bad style to directly use such things.

Mathlib/Data/Nat/PartENat.lean

@@ -754,15 +754,11 @@ noncomputable def withTopAddEquiv : PartENat ≃+ ℕ∞ :=
 
 end WithTopEquiv
 
--- Porting note: `Nat.lt_wfRel` changed in core,
--- the last line of the mathlib3 proof was:
--- `exact InvImage.wf _ (WithTop.wellFounded_lt Nat.lt_wfRel)`
 theorem lt_wf : @WellFounded PartENat (· < ·) := by
   classical
     change WellFounded fun a b : PartENat => a < b
     simp_rw [← withTopEquiv_lt]
-    refine InvImage.wf _ (WithTop.wellFounded_lt ?_)
-    exact IsWellFounded.fix.proof_1 fun y x => y < x
+    exact InvImage.wf _ (WithTop.wellFounded_lt Nat.lt_wfRel.wf)
 #align part_enat.lt_wf PartENat.lt_wf
 
 instance : WellFoundedLT PartENat :=