Post-merge fixes

leanprover · Jan 21, 2025 · 6c488b1 · 6c488b1
1 parent 54214bf
commit 6c488b1
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/Init/Internal/Order/Lemmas.lean b/src/Init/Internal/Order/Lemmas.lean
@@ -469,8 +469,8 @@ theorem monotone_mapM (xs : Array α) (f : γ → α → m β) (hmono : monotone
     apply monotone_const
 
 @[partial_fixpoint_monotone]
-theorem monotone_mapFinIdxM (xs : Array α) (f : γ → Fin xs.size → α → m β) (hmono : monotone f) :
-    monotone (fun x => xs.mapFinIdxM (f x)) := by
+theorem monotone_mapFinIdxM (xs : Array α) (f : γ → (i : Nat) → α → i < xs.size → m β)
+    (hmono : monotone f) : monotone (fun x => xs.mapFinIdxM (f x)) := by
   suffices ∀ i j (h : i + j = xs.size) r, monotone (fun x => Array.mapFinIdxM.map xs (f x) i j h r) by apply this
   intros i j h r
   induction i, j, h, r using Array.mapFinIdxM.map.induct xs
@@ -479,6 +479,7 @@ theorem monotone_mapFinIdxM (xs : Array α) (f : γ → Fin xs.size → α → m
   case case2 ih =>
     apply monotone_bind
     · dsimp
+      apply monotone_apply
       apply monotone_apply
       apply monotone_apply
       apply hmono