From 4bf7fa7447eea00cecba8327bb9c9e5f4485f0a7 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 18 Mar 2026 13:59:19 +0000
Subject: [PATCH] chore: fix build after rebootstrap

---
 .../Control/Lawful/MonadLift/Instances.lean   |  4 ++--
 .../Combinators/Monadic/FilterMap.lean        |  7 +++++++
 .../Lemmas/Combinators/Monadic/FilterMap.lean | 19 +++++++++----------
 src/Std/Do/WP/Basic.lean                      |  6 +++---
 src/Std/Do/WP/SimpLemmas.lean                 | 10 +++++-----
 src/Std/Time/Date/Unit/Year.lean              |  2 ++
 6 files changed, 28 insertions(+), 20 deletions(-)

diff --git a/src/Init/Control/Lawful/MonadLift/Instances.lean b/src/Init/Control/Lawful/MonadLift/Instances.lean
index 7454ed9dc9..a15130c871 100644
--- a/src/Init/Control/Lawful/MonadLift/Instances.lean
+++ b/src/Init/Control/Lawful/MonadLift/Instances.lean
@@ -103,11 +103,11 @@ namespace StateRefT'
 instance {ω σ : Type} {m : Type → Type} [Monad m] : LawfulMonadLift m (StateRefT' ω σ m) where
   monadLift_pure _ := by
     simp only [MonadLift.monadLift, pure]
-    unfold StateRefT'.lift ReaderT.pure
+    unfold StateRefT'.lift instMonad._aux_5 ReaderT.pure
     simp only
   monadLift_bind _ _ := by
     simp only [MonadLift.monadLift, bind]
-    unfold StateRefT'.lift ReaderT.bind
+    unfold StateRefT'.lift instMonad._aux_13 ReaderT.bind
     simp only
 
 end StateRefT'
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
index 369053160d..f35b21b00f 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
@@ -168,6 +168,13 @@ instance Map.instIterator {α β γ : Type w} {m : Type w → Type w'} {n : Type
     Iterator (Map α m n lift f) n γ :=
   inferInstanceAs <| Iterator (FilterMap α m n lift _) n γ
 
+theorem Map.instIterator_eq_filterMapInstIterator {α β γ : Type w} {m : Type w → Type w'}
+    {n : Type w → Type w''} [Monad n]
+    [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α} {f : β → PostconditionT n γ} :
+    Map.instIterator (α := α) (β := β) (γ := γ) (m := m) (n := n) (lift := lift) (f := f) =
+      FilterMap.instIterator :=
+  rfl
+
 private def FilterMap.instFinitenessRelation {α β γ : Type w} {m : Type w → Type w'}
     {n : Type w → Type w''} [Monad n] [Iterator α m β] {lift : ⦃α : Type w⦄ → m α → n α}
     {f : β → PostconditionT n (Option γ)} [Finite α m] :
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index 1d7e3b8622..df469f2ce1 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -699,18 +699,16 @@ theorem IterM.toList_map {α β β' : Type w} {m : Type w → Type w'} [Monad m]
     (it : IterM (α := α) m β) :
     (it.map f).toList = (fun x => x.map f) <$> it.toList := by
   rw [← List.filterMap_eq_map, ← toList_filterMap]
-  let t := type_of% (it.map f)
-  let t' := type_of% (it.filterMap (some ∘ f))
+  simp only [map, mapWithPostcondition, InternalCombinators.map, filterMap,
+    filterMapWithPostcondition, InternalCombinators.filterMap]
+  unfold Map
   congr
-  · simp [Map]
-  · simp [Map.instIterator, inferInstanceAs]
+  · simp
+  · rw [Map.instIterator_eq_filterMapInstIterator]
     congr
     simp
-  · simp only [map, mapWithPostcondition, InternalCombinators.map, Function.comp_apply, filterMap,
-    filterMapWithPostcondition, InternalCombinators.filterMap]
-    congr
-    · simp [Map]
-    · simp
+  · simp
+  · simp
 
 @[simp]
 theorem IterM.toList_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
@@ -1310,7 +1308,8 @@ theorem IterM.forIn_mapWithPostcondition
     haveI : MonadLift n o := ⟨monadLift⟩
     forIn (it.mapWithPostcondition f) init g =
       forIn it init (fun out acc => do g (← (f out).run) acc) := by
-  unfold mapWithPostcondition InternalCombinators.map Map.instIterator Map.instIteratorLoop Map
+  unfold mapWithPostcondition InternalCombinators.map Map.instIteratorLoop Map
+  rw [Map.instIterator_eq_filterMapInstIterator]
   rw [← InternalCombinators.filterMap, ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
   simp
 
diff --git a/src/Std/Do/WP/Basic.lean b/src/Std/Do/WP/Basic.lean
index ca1acacd29..dc6e035271 100644
--- a/src/Std/Do/WP/Basic.lean
+++ b/src/Std/Do/WP/Basic.lean
@@ -152,7 +152,7 @@ theorem Except.of_wp_eq {ε α : Type u} {x prog : Except ε α} (h : prog = x)
     (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.error e)⌝⟩) → P x := by
   subst h
   intro hspec
-  simp only [wp, ExceptT.run, Id.run, PredTrans.apply_pushExcept, PredTrans.apply_Pure_pure] at hspec
+  simp only [wp, ExceptT.run, Id.run, PredTrans.apply_pushExcept, PredTrans.apply_Pure_pure, instWP._aux_1] at hspec
   split at hspec <;> exact hspec True.intro
 
 /--
@@ -164,7 +164,7 @@ Useful if you want to prove a property about an expression `prog : Except ε α`
 theorem Except.of_wp {ε α : Type u} {prog : Except ε α} (P : Except ε α → Prop) :
     (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.error e)⌝⟩) → P prog := by
   intro hspec
-  simp only [wp, ExceptT.run, Id.run, PredTrans.apply_pushExcept, PredTrans.apply_Pure_pure] at hspec
+  simp only [wp, ExceptT.run, Id.run, PredTrans.apply_pushExcept, PredTrans.apply_Pure_pure, instWP._aux_1] at hspec
   split at hspec <;> exact hspec True.intro
 
 /--
@@ -176,7 +176,7 @@ theorem Option.of_wp_eq {α : Type u} {x prog : Option α} (h : prog = x) (P : O
     (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x := by
   subst h
   intro hspec
-  simp only [wp, OptionT.run, Id.run, PredTrans.apply_pushOption, PredTrans.apply_Pure_pure] at hspec
+  simp only [wp, OptionT.run, Id.run, PredTrans.apply_pushOption, PredTrans.apply_Pure_pure, instWP._aux_1] at hspec
   split at hspec <;> exact hspec True.intro
 
 /--
diff --git a/src/Std/Do/WP/SimpLemmas.lean b/src/Std/Do/WP/SimpLemmas.lean
index 8758333769..b2ae319e90 100644
--- a/src/Std/Do/WP/SimpLemmas.lean
+++ b/src/Std/Do/WP/SimpLemmas.lean
@@ -422,7 +422,7 @@ theorem throwThe [MonadExceptOf ε m] [WP m ps] :
 @[simp]
 theorem throw_Except :
     wp⟦MonadExceptOf.throw e : Except ε α⟧ Q = Q.2.1 e := by
-  simp [wp, MonadExceptOf.throw, Id.run, ExceptT.run]
+  simp [wp, MonadExceptOf.throw, Id.run, ExceptT.run, Except.instWP._aux_1]
 
 @[simp]
 theorem throw_ExceptT [Monad m] [WPMonad m ps] :
@@ -432,7 +432,7 @@ theorem throw_ExceptT [Monad m] [WPMonad m ps] :
 @[simp]
 theorem throw_Option :
     wp⟦MonadExceptOf.throw e : Option α⟧ Q = Q.2.1 e := by
-  simp [wp, MonadExceptOf.throw, Id.run, OptionT.run]
+  simp [wp, MonadExceptOf.throw, Id.run, OptionT.run, Option.instWP._aux_1]
 
 @[simp]
 theorem throw_OptionT [Monad m] [WPMonad m ps] :
@@ -484,7 +484,7 @@ theorem tryCatchThe [MonadExceptOf ε m] [WP m ps] :
 @[simp]
 theorem tryCatch_Except :
     wp⟦MonadExceptOf.tryCatch x h : Except ε α⟧ Q = wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2) := by
-  simp only [wp, ExceptT.run, Id.run, MonadExceptOf.tryCatch, Except.tryCatch,
+  simp only [wp, Except.instWP._aux_1, ExceptT.run, Id.run, MonadExceptOf.tryCatch, Except.tryCatch,
     PredTrans.apply_pushExcept]
   cases x <;> simp
 
@@ -501,7 +501,7 @@ theorem tryCatch_ExceptT [Monad m] [WPMonad m ps] :
 @[simp]
 theorem tryCatch_Option :
     wp⟦MonadExceptOf.tryCatch x h : Option α⟧ Q = wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2) := by
-  simp only [wp, Id.run, OptionT.run, MonadExceptOf.tryCatch, Option.tryCatch,
+  simp only [wp, Option.instWP._aux_1, Id.run, OptionT.run, MonadExceptOf.tryCatch, Option.tryCatch,
     PredTrans.apply_pushOption]
   cases x <;> simp
 
@@ -590,7 +590,7 @@ theorem orElse_ExceptT [Monad m] [WPMonad m ps] :
 @[simp]
 theorem orElse_Option  :
     wp⟦OrElse.orElse x h : Option α⟧ Q = wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2) := by
-  cases x <;> simp [OrElse.orElse, Option.orElse, wp, Id.run, OptionT.run]
+  cases x <;> simp [OrElse.orElse, Option.orElse, wp, Id.run, OptionT.run, Option.instWP._aux_1]
 
 @[simp]
 theorem orElse_OptionT [Monad m] [WPMonad m ps] :
diff --git a/src/Std/Time/Date/Unit/Year.lean b/src/Std/Time/Date/Unit/Year.lean
index 8e4459043f..a8fd4b0350 100644
--- a/src/Std/Time/Date/Unit/Year.lean
+++ b/src/Std/Time/Date/Unit/Year.lean
@@ -39,10 +39,12 @@ instance : ToString Era where
 @[expose] def Offset : Type := Int
 deriving Repr, DecidableEq, Inhabited, Add, Sub, Neg, LE, LT, ToString
 
+set_option backward.inferInstanceAs.wrap.instances false in
 instance {x y : Offset} : Decidable (x ≤ y) :=
   let x : Int := x
   inferInstanceAs (Decidable (x ≤ y))
 
+set_option backward.inferInstanceAs.wrap.instances false in
 instance {x y : Offset} : Decidable (x < y) :=
   let x : Int := x
   inferInstanceAs (Decidable (x < y))