From e1ae12500e69eb3d9ff77e1e224ecb28b8a7d917 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Mon, 13 Jan 2025 16:11:10 +0100
Subject: [PATCH] even better Inhabited instance

---
 src/Std/Data/DHashMap/Lemmas.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index fe193992c3f18..5a51df0241543 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -1073,7 +1073,7 @@ theorem get_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β
 theorem get!_alter [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : Option (β k) → Option (β k)} :
     (m.alter k f).get! k' =
     if heq : k == k' then
-      haveI : Inhabited (β k) := cast (by rw [eq_of_beq heq]) hi
+      haveI : Inhabited (β k) := ⟨cast (congrArg β <| eq_of_beq heq).symm default⟩
       cast (congrArg β (eq_of_beq heq)) <| (f (m.get? k)).get!
     else
       m.get! k' :=
@@ -1402,7 +1402,7 @@ theorem get_modify_self [LawfulBEq α] {k : α} {f : β k → β k} {h : k ∈ m
 theorem get!_modify [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
     (m.modify k f).get! k' =
     if heq : k == k' then
-      haveI : Inhabited (β k) := cast (by rw [eq_of_beq heq]) hi
+      haveI : Inhabited (β k) := ⟨cast (congrArg β <| eq_of_beq heq).symm default⟩
       -- not correct if f does not preserve default: ... f (m.get! k)
       -- possible alternative: write ... (m.getD k (cast ⋯ default))
       m.get? k |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get!