fixes

Mathlib/CategoryTheory/Functor/Flat.lean

@@ -82,6 +82,7 @@ theorem RepresentablyFlat.id : RepresentablyFlat (𝟭 C) := inferInstance
 
 theorem RepresentablyCoflat.id : RepresentablyCoflat (𝟭 C) := inferInstance
 
+set_option maxHeartbeats 400000 in
 instance RepresentablyFlat.comp (G : D ⥤ E) [RepresentablyFlat F]
     [RepresentablyFlat G] : RepresentablyFlat (F ⋙ G) := by
   refine ⟨fun X => IsCofiltered.of_cone_nonempty.{0} _ (fun {J} _ _ H => ?_)⟩
@@ -91,6 +92,7 @@ instance RepresentablyFlat.comp (G : D ⥤ E) [RepresentablyFlat F]
       map := fun {j j'} f =>
         StructuredArrow.homMk (H.map f).right (congrArg CommaMorphism.right (c₁.w f)) }
   obtain ⟨c₂⟩ := IsCofiltered.cone_nonempty H₂
+  simp only [H₂] at c₂
   exact ⟨⟨StructuredArrow.mk (c₁.pt.hom ≫ G.map c₂.pt.hom),
     ⟨fun j => StructuredArrow.homMk (c₂.π.app j).right (by simp [← G.map_comp, (c₂.π.app j).w]),
      fun j j' f => by simpa using (c₂.w f).symm⟩⟩⟩

Mathlib/Tactic/SplitIfs.lean

@@ -71,12 +71,21 @@ private def discharge? (e : Expr) : SimpM (Option Expr) := do
     then return some (mkConst `True.intro)
   return none
 
+/-
+#adaptation_note
+
+This is a hacky adaptation for https://github.com/leanprover/lean4/pull/6123.
+It has the side effect of `split_ifs` unfolding lets.
+-/
 /-- Simplifies if-then-else expressions after cases have been split out.
 -/
-private def reduceIfsAt (loc : Location) : TacticM Unit := do
+private def reduceIfsAt (loc : Location) : TacticM Unit := withMainContext do
   let ctx ← SplitIf.getSimpContext
-  let ctx := ctx.setFailIfUnchanged false
-  let _ ← simpLocation ctx (← ({} : Simp.SimprocsArray).add `reduceCtorEq false) discharge? loc
+  let ctx ← Simp.mkContext
+    (config := { ctx.config with zeta := true, zetaDelta := true, failIfUnchanged := false })
+    (simpTheorems := ctx.simpTheorems)
+    (congrTheorems := ctx.congrTheorems)
+  let _ ← simpLocation ctx (← ({} : Simp.SimprocsArray).add ``reduceCtorEq true) discharge? loc
   pure ()
 
 /-- Splits a single if-then-else expression and then reduces the resulting goals.