chore: tweak subsingleton_of_trichotomous_of_irrefl (#3749)

Match leanprover-community/mathlib#18749

Mathlib/Order/InitialSeg.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Floris van Doorn
 
 ! This file was ported from Lean 3 source module order.initial_seg
-! leanprover-community/mathlib commit 1a313d8bba1bad05faba71a4a4e9742ab5bd9efd
+! leanprover-community/mathlib commit 730c6d4cab72b9d84fcfb9e95e8796e9cd8f40ba
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -131,21 +131,18 @@ theorem trans_apply (f : r ≼i s) (g : s ≼i t) (a : α) : (f.trans g) a = g (
   rfl
 #align initial_seg.trans_apply InitialSeg.trans_apply
 
-theorem unique_of_trichotomous_of_irrefl [IsTrichotomous β s] [IsIrrefl β s] :
-    WellFounded r → Subsingleton (r ≼i s)
-  | ⟨h⟩ =>
-    ⟨fun f g => by
-      ext a
-      induction' h a with a _ IH
-      refine extensional_of_trichotomous_of_irrefl s fun x => ?_
-      simp only [f.init_iff, g.init_iff]
-      exact exists_congr fun y => and_congr_left fun h => IH _ h ▸ Iff.rfl⟩
-#align initial_seg.unique_of_trichotomous_of_irrefl InitialSeg.unique_of_trichotomous_of_irrefl
+instance subsingleton_of_trichotomous_of_irrefl [IsTrichotomous β s] [IsIrrefl β s]
+    [IsWellFounded α r] : Subsingleton (r ≼i s) :=
+  ⟨fun f g => by
+    ext a
+    refine' IsWellFounded.induction r a fun b IH =>
+      extensional_of_trichotomous_of_irrefl s fun x => _
+    rw [f.init_iff, g.init_iff]
+    exact exists_congr fun x => and_congr_left fun hx => IH _ hx ▸ Iff.rfl⟩
+#align initial_seg.subsingleton_of_trichotomous_of_irrefl InitialSeg.subsingleton_of_trichotomous_of_irrefl
 
 instance [IsWellOrder β s] : Subsingleton (r ≼i s) :=
-  ⟨fun a =>
-    @Subsingleton.elim _
-      (unique_of_trichotomous_of_irrefl (@RelEmbedding.wellFounded _ _ r s a IsWellFounded.wf)) a⟩
+  ⟨fun a => by let _ := a.isWellFounded; exact Subsingleton.elim a⟩
 
 protected theorem eq [IsWellOrder β s] (f g : r ≼i s) (a) : f a = g a := by
   rw [Subsingleton.elim f g]