From 4fdb452f65b5a8b09463903626b9fca5f199b31b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Fri, 7 Apr 2023 10:11:21 -0600
Subject: [PATCH] instance

---
 src/logic/hydra.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/logic/hydra.lean b/src/logic/hydra.lean
index 97260914248eb..286d1a2434a9a 100644
--- a/src/logic/hydra.lean
+++ b/src/logic/hydra.lean
@@ -136,7 +136,8 @@ begin
 end
 
 /-- `cut_expand r` is well-founded when `r` is. -/
-theorem _root_.well_founded.cut_expand (hr : well_founded r) : well_founded (cut_expand r) :=
-⟨by { letI h := hr.is_irrefl, exact λ s, acc_of_singleton $ λ a _, (hr.apply a).cut_expand }⟩
+instance _root_.is_well_founded.cut_expand [is_well_founded α r] :
+  is_well_founded _ (cut_expand r) :=
+⟨⟨λ s, acc_of_singleton $ λ a _, (is_well_founded.apply r a).cut_expand⟩⟩
 
 end relation