From 999ea7fce24db723ffe6e38854b1ed019bce756b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Fri, 22 Nov 2024 11:20:50 +1100
Subject: [PATCH] fixes

---
 Mathlib/CategoryTheory/Functor/Flat.lean |  2 ++
 Mathlib/Tactic/SplitIfs.lean             | 15 ++++++++++++---
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Functor/Flat.lean b/Mathlib/CategoryTheory/Functor/Flat.lean
index 2d0444d695f18..0cb417530c71d 100644
--- a/Mathlib/CategoryTheory/Functor/Flat.lean
+++ b/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⟩⟩⟩
diff --git a/Mathlib/Tactic/SplitIfs.lean b/Mathlib/Tactic/SplitIfs.lean
index 64e0fa989bcac..1b59dd0b5d68b 100644
--- a/Mathlib/Tactic/SplitIfs.lean
+++ b/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.