diff --git a/ExtTreeMapLemmas/DTreeMap.lean b/ExtTreeMapLemmas/DTreeMap.lean
index 73b942d..55d5e86 100644
--- a/ExtTreeMapLemmas/DTreeMap.lean
+++ b/ExtTreeMapLemmas/DTreeMap.lean
@@ -217,7 +217,7 @@ theorem Const.get?_mergeWith [TransCmp cmp] [LawfulEqCmp cmp]
 
 attribute [local instance low] beqOfOrd
 
-theorem Internal.Impl.Const.get?_filter [Ord α] [TransOrd α]
+theorem Internal.Impl.Const.get?_filter_with_getKey_pfilter [Ord α] [TransOrd α]
     (m : DTreeMap.Internal.Impl α (fun _ => β)) (h : m.WF) (f : α → β → Bool) (k : α) :
     Const.get? (m.filter f h.balanced).1 k = (Const.get? m k).pfilter (fun v h' => f (m.getKey k ((contains_eq_isSome_get? h).trans (Option.isSome_of_eq_some h'))) v) := by
   -- This manual proof is usually done by the `simp_to_model` tactic
@@ -226,11 +226,11 @@ theorem Internal.Impl.Const.get?_filter [Ord α] [TransOrd α]
   apply Std.Internal.List.Const.getValue?_filter
   apply h.ordered.distinctKeys
 
-theorem get?_filter {cmp : α → α → Ordering} [TransCmp cmp]
+theorem get?_filter_with_getKey_pfilter {cmp : α → α → Ordering} [TransCmp cmp]
     (m : DTreeMap α (fun _ => β) cmp) (f : α → β → Bool) (k : α) :
     Const.get? (m.filter f) k = (Const.get? m k).pfilter (fun v h' => f (m.getKey k (Const.contains_eq_isSome_get?.trans (Option.isSome_of_eq_some h'))) v) :=
   letI : Ord α := ⟨cmp⟩
-  DTreeMap.Internal.Impl.Const.get?_filter m.inner m.wf _ _
+  DTreeMap.Internal.Impl.Const.get?_filter_with_getKey_pfilter m.inner m.wf _ _
 
 end DTreeMap
 
diff --git a/ExtTreeMapLemmas/ExtDTreeMap.lean b/ExtTreeMapLemmas/ExtDTreeMap.lean
index c77620e..6790eb8 100644
--- a/ExtTreeMapLemmas/ExtDTreeMap.lean
+++ b/ExtTreeMapLemmas/ExtDTreeMap.lean
@@ -5,9 +5,9 @@ namespace Std
 
 attribute [local instance low] beqOfOrd
 
-theorem ExtDTreeMap.get?_filter {cmp : α → α → Ordering} [TransCmp cmp]
+theorem ExtDTreeMap.get?_filter_with_getKey_pfilter {cmp : α → α → Ordering} [TransCmp cmp]
     (m : ExtDTreeMap α (fun _ => β) cmp) (f : α → β → Bool) (k : α) :
-    Const.get? (m.filter f) k = (Const.get? m k).pfilter (fun v h' => f (m.getKey k (Const.contains_eq_isSome_get?.trans (Option.isSome_of_eq_some h'))) v) :=
-  m.inductionOn fun _ => DTreeMap.get?_filter _ _ _
+    Const.get? (m.filter f) k = (Const.get? m k).pfilter (fun v h' => f (m.getKey k (Const.contains_eq_isSome_get?.trans (Option.isSome_of_eq_some h'))) v) := by
+  exact?
 
 end Std
diff --git a/ExtTreeMapLemmas/ExtTreeMap.lean b/ExtTreeMapLemmas/ExtTreeMap.lean
index d62251a..71e4d08 100644
--- a/ExtTreeMapLemmas/ExtTreeMap.lean
+++ b/ExtTreeMapLemmas/ExtTreeMap.lean
@@ -16,7 +16,10 @@ theorem getElem?_pfilter
   {m : ExtTreeMap α β cmp} {f : α → β → Bool} {k : α} :
   (m.filter f)[k]? =
   m[k]?.pfilter (fun v h' => f (m.getKey k (contains_eq_isSome_getElem?.trans (Option.isSome_of_eq_some h'))) v) :=
-  ExtDTreeMap.get?_filter m.inner f k
+  by
+    generalize_proofs at *;
+    -- Apply the hypothesis `h_filter_eq` directly to conclude the proof.
+    apply Std.ExtDTreeMap.get?_filter_with_getKey_pfilter
 
 variable {α β : Type} {cmp : α → α → Ordering}
 variable {k : α} {m m₁ m₂ : Std.ExtTreeMap α β cmp} {f : α → β → β → β}
@@ -108,9 +111,9 @@ lemma toList_ofList [BEq α] [LawfulBEq α] : ofList (toList m) cmp = m := by
   grind
 
 @[simp, grind =]
-lemma getElem?_filter {β : Type} {f : α → β → Bool} {k : α} {m : ExtTreeMap α β cmp} :
+lemma getElem?_filter_with_getKey {β : Type} {f : α → β → Bool} {k : α} {m : ExtTreeMap α β cmp} :
   (m.filter f)[k]? = m[k]?.filter (f k) := by
-  simp [ExtTreeMap.getElem?_pfilter]
+  simp
 
 variable {f : α → β → Bool}
 
diff --git a/lake-manifest.json b/lake-manifest.json
index f5cb61a..d9011b2 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1a5c8fe51b870f5c4ffd6fe44936e09a776d8f3e",
+   "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0-rc2",
+   "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fde3fc21dd68a10791dea22b6f5b53c5a5a5962d",
+   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+   "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,60 +35,60 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "856a8cb8908af109aac3ce13e2b4f866f3d75199",
+   "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2d6d124aedc3023506a67e50bfd5582384d6bd17",
+   "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.63-pre",
+   "inputRev": "v0.0.83",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a1b5d59f433c6ec2b318192bd910c257a3c62be8",
+   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "56047303fce0d07dcae7e3e91b17eef67d11f6f4",
+   "rev": "9312503909aa8e8bb392530145cc1677a6298574",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bfd7f60186ea20946cc36288f83ad3659520f0ce",
+   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "1604206fcd0462da9a241beeac0e2df471647435",
+   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.26.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "ExtTreeMapLemmas",
diff --git a/lakefile.lean b/lakefile.lean
index ffaceda..a62030c 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,7 +4,7 @@ open System Lake DSL
 
 package ExtTreeMapLemmas where version := v!"0.1.0"
 
-require "leanprover-community" / mathlib @ git "v4.22.0-rc2"
+require "leanprover-community" / mathlib @ git "v4.26.0"
 
 @[default_target]
 lean_lib ExtTreeMapLemmas
diff --git a/lean-toolchain b/lean-toolchain
index 52782c4..2654c20 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0-rc2
\ No newline at end of file
+leanprover/lean4:v4.26.0
\ No newline at end of file