feat: Simp.Config.implicitDefEqProofs (#4595)

This PR implements `Simp.Config.implicitDefEqsProofs`. When `true`
(default: `true`), `simp` will **not** create a proof term for a
rewriting rule associated with an `rfl`-theorem. Rewriting rules are
provided by users by annotating theorems with the attribute `@[simp]`.
If the proof of the theorem is just `rfl` (reflexivity), and
`implicitDefEqProofs := true`, `simp` will **not** create a proof term
which is an application of the annotated theorem.

The default setting does change the existing behavior. Users can use
`simp -implicitDefEqProofs` to force `simp` to create a proof term for
`rfl`-theorems. This can positively impact proof checking time in the
kernel.

This PR also fixes an issue in the `split` tactic that has been exposed
by this feature. It was looking for `split` candidates in proofs and
implicit arguments. See new test for issue exposed by the previous
feature.

---------

Co-authored-by: Kim Morrison <kim@tqft.net>

src/Init/MetaTypes.lean

@@ -224,7 +224,8 @@ structure Config where
   -/
   index             : Bool := true
   /--
-  This option does not have any effect (yet).
+  If `implicitDefEqProofs := true`, `simp` does not create proof terms when the
+  input and output terms are definitionally equal.
   -/
   implicitDefEqProofs : Bool := true
   deriving Inhabited, BEq

src/Lean/Meta/Basic.lean

@@ -229,7 +229,7 @@ structure ParamInfo where
   hasFwdDeps     : Bool       := false
   /-- `backDeps` contains the backwards dependencies. That is, the (0-indexed) position of previous parameters that this one depends on. -/
   backDeps       : Array Nat  := #[]
-  /-- `isProp` is true if the parameter is always a proposition. -/
+  /-- `isProp` is true if the parameter type is always a proposition. -/
   isProp         : Bool       := false
   /--
     `isDecInst` is true if the parameter's type is of the form `Decidable ...`.

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -108,13 +108,19 @@ where
       trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to synthesize instance{indentExpr type}"
       return false
 
+private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
+  if thm.rfl then
+    return (← getConfig).implicitDefEqProofs
+  else
+    return false
+
 private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInfo) (val : Expr) (type : Expr) (e : Expr) (thm : SimpTheorem) (numExtraArgs : Nat) : SimpM (Option Result) := do
   recordTriedSimpTheorem thm.origin
   let rec go (e : Expr) : SimpM (Option Result) := do
     if (← isDefEq lhs e) then
       unless (← synthesizeArgs thm.origin bis xs) do
         return none
-      let proof? ← if thm.rfl then
+      let proof? ← if (← useImplicitDefEqProof thm) then
         pure none
       else
         let proof ← instantiateMVars (mkAppN val xs)

src/Lean/Meta/Tactic/Split.lean

@@ -269,7 +269,7 @@ def mkDiscrGenErrorMsg (e : Expr) : MessageData :=
 def throwDiscrGenError (e : Expr) : MetaM α :=
   throwError (mkDiscrGenErrorMsg e)
 
-def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do
+def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withContext do
   let some app ← matchMatcherApp? e | throwError "internal error in `split` tactic: match application expected{indentExpr e}\nthis error typically occurs when the `split` tactic internal functions have been used in a new meta-program"
   let matchEqns ← Match.getEquationsFor app.matcherName
   let mvarIds ← applyMatchSplitter mvarId app.matcherName app.matcherLevels app.params app.discrs
@@ -278,43 +278,14 @@ def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do
     return (i+1, mvarId::mvarIds)
   return mvarIds.reverse
 
-/-- Return an `if-then-else` or `match-expr` to split. -/
-partial def findSplit? (env : Environment) (e : Expr) (splitIte := true) (exceptionSet : ExprSet := {}) : Option Expr :=
-  go e
-where
-  go (e : Expr) : Option Expr :=
-    if let some target := e.find? isCandidate then
-      if e.isIte || e.isDIte then
-        let cond := target.getArg! 1 5
-        -- Try to find a nested `if` in `cond`
-        go cond |>.getD target
-      else
-        some target
-    else
-      none
-
-  isCandidate (e : Expr) : Bool := Id.run do
-    if exceptionSet.contains e then
-      false
-    else if splitIte && (e.isIte || e.isDIte) then
-      !(e.getArg! 1 5).hasLooseBVars
-    else if let some info := isMatcherAppCore? env e then
-      let args := e.getAppArgs
-      for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
-        if args[i]!.hasLooseBVars then
-          return false
-      return true
-    else
-      false
-
 end Split
 
 open Split
 
-partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (List MVarId)) := commitWhenSome? do
+partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (List MVarId)) := commitWhenSome? do mvarId.withContext do
   let target ← instantiateMVars (← mvarId.getType)
   let rec go (badCases : ExprSet) : MetaM (Option (List MVarId)) := do
-    if let some e := findSplit? (← getEnv) target splitIte badCases then
+    if let some e ← findSplit? target (if splitIte then .both else .match) badCases then
       if e.isIte || e.isDIte then
         return (← splitIfTarget? mvarId).map fun (s₁, s₂) => [s₁.mvarId, s₂.mvarId]
       else
@@ -333,7 +304,7 @@ partial def splitTarget? (mvarId : MVarId) (splitIte := true) : MetaM (Option (L
 
 def splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MVarId)) := commitWhenSome? do
   mvarId.withContext do
-    if let some e := findSplit? (← getEnv) (← instantiateMVars (← inferType (mkFVar fvarId))) then
+    if let some e ← findSplit? (← instantiateMVars (← inferType (mkFVar fvarId))) then
       if e.isIte || e.isDIte then
         return (← splitIfLocalDecl? mvarId fvarId).map fun (mvarId₁, mvarId₂) => [mvarId₁, mvarId₂]
       else

src/Lean/Meta/Tactic/SplitIf.lean

@@ -8,6 +8,124 @@ import Lean.Meta.Tactic.Cases
 import Lean.Meta.Tactic.Simp.Main
 
 namespace Lean.Meta
+
+inductive SplitKind where
+  | ite | match | both
+
+def SplitKind.considerIte : SplitKind → Bool
+  | .ite | .both => true
+  | _ => false
+
+def SplitKind.considerMatch : SplitKind → Bool
+  | .match | .both => true
+  | _ => false
+
+namespace FindSplitImpl
+
+structure Context where
+  exceptionSet : ExprSet := {}
+  kind : SplitKind := .both
+
+unsafe abbrev FindM := ReaderT Context $ StateT (PtrSet Expr) MetaM
+
+/--
+Checks whether `e` is a candidate for `split`.
+Returns `some e'` if a prefix is a candidate.
+Example: suppose `e` is `(if b then f else g) x`, then
+the result is `some e'` where `e'` is the subterm `(if b then f else g)`
+-/
+private def isCandidate? (env : Environment) (ctx : Context) (e : Expr) : Option Expr := Id.run do
+  let ret (e : Expr) : Option Expr :=
+    if ctx.exceptionSet.contains e then none else some e
+  if ctx.kind.considerIte then
+    if e.isAppOf ``ite || e.isAppOf ``dite then
+      let numArgs := e.getAppNumArgs
+      if numArgs >= 5 && !(e.getArg! 1 5).hasLooseBVars then
+        return ret (e.getBoundedAppFn (numArgs - 5))
+  if ctx.kind.considerMatch then
+    if let some info := isMatcherAppCore? env e then
+      let args := e.getAppArgs
+      for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do
+        if args[i]!.hasLooseBVars then
+          return none
+      return ret (e.getBoundedAppFn (args.size - info.arity))
+  return none
+
+@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
+  if (← get).contains e then
+    failure
+  modify fun s => s.insert e
+
+unsafe def visit (e : Expr) : OptionT FindM Expr := do
+  checkVisited e
+  if let some e := isCandidate? (← getEnv) (← read) e then
+    return e
+  else
+    -- We do not look for split candidates in proofs.
+    unless e.hasLooseBVars do
+      if (← isProof e) then
+        failure
+    match e with
+    | .lam _ _ b _ | .proj _ _ b -- We do not look for split candidates in the binder of lambdas.
+    | .mdata _ b       => visit b
+    | .forallE _ d b _ => visit d <|> visit b -- We want to look for candidates at `A → B`
+    | .letE _ _ v b _  => visit v <|> visit b
+    | .app ..          => visitApp? e
+    | _                => failure
+where
+  visitApp? (e : Expr) : FindM (Option Expr) :=
+    e.withApp fun f args => do
+    -- See comment at `Canonicalizer.lean` regarding the case where
+    -- `f` has loose bound variables.
+    let info ← if f.hasLooseBVars then
+      pure {}
+    else
+      getFunInfo f
+    for u : i in [0:args.size] do
+      let arg := args[i]
+      if h : i < info.paramInfo.size then
+        let info := info.paramInfo[i]
+        unless info.isProp do
+          if info.isExplicit then
+            let some found ← visit arg | pure ()
+            return found
+      else
+        let some found ← visit arg | pure ()
+        return found
+    visit f
+
+end FindSplitImpl
+
+/-- Return an `if-then-else` or `match-expr` to split. -/
+partial def findSplit? (e : Expr) (kind : SplitKind := .both) (exceptionSet : ExprSet := {}) : MetaM (Option Expr) := do
+  go (← instantiateMVars e)
+where
+  go (e : Expr) : MetaM (Option Expr) := do
+    if let some target ← find? e then
+      if target.isIte || target.isDIte then
+        let cond := target.getArg! 1 5
+        -- Try to find a nested `if` in `cond`
+        return (← go cond).getD target
+      else
+        return some target
+    else
+      return none
+
+  find? (e : Expr) : MetaM (Option Expr) := do
+    let some candidate ← unsafe FindSplitImpl.visit e { kind, exceptionSet } |>.run' mkPtrSet
+      | return none
+    trace[split.debug] "candidate:{indentExpr candidate}"
+    return some candidate
+
+/-- Return the condition and decidable instance of an `if` expression to case split. -/
+private partial def findIfToSplit? (e : Expr) : MetaM (Option (Expr × Expr)) := do
+  if let some iteApp ← findSplit? e .ite then
+    let cond := iteApp.getArg! 1 5
+    let dec := iteApp.getArg! 2 5
+    return (cond, dec)
+  else
+    return none
+
 namespace SplitIf
 
 /--
@@ -62,19 +180,9 @@ private def discharge? (numIndices : Nat) (useDecide : Bool) : Simp.Discharge :=
 def mkDischarge? (useDecide := false) : MetaM Simp.Discharge :=
   return discharge? (← getLCtx).numIndices useDecide
 
-/-- Return the condition and decidable instance of an `if` expression to case split. -/
-private partial def findIfToSplit? (e : Expr) : Option (Expr × Expr) :=
-  if let some iteApp := e.find? fun e => (e.isIte || e.isDIte) && !(e.getArg! 1 5).hasLooseBVars then
-    let cond := iteApp.getArg! 1 5
-    let dec := iteApp.getArg! 2 5
-    -- Try to find a nested `if` in `cond`
-    findIfToSplit? cond |>.getD (cond, dec)
-  else
-    none
-
-def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := do
+def splitIfAt? (mvarId : MVarId) (e : Expr) (hName? : Option Name) : MetaM (Option (ByCasesSubgoal × ByCasesSubgoal)) := mvarId.withContext do
   let e ← instantiateMVars e
-  if let some (cond, decInst) := findIfToSplit? e then
+  if let some (cond, decInst) ← findIfToSplit? e then
     let hName ← match hName? with
       | none       => mkFreshUserName `h
       | some hName => pure hName
@@ -106,6 +214,7 @@ def splitIfTarget? (mvarId : MVarId) (hName? : Option Name := none) : MetaM (Opt
     let mvarId₁ ← simpIfTarget s₁.mvarId
     let mvarId₂ ← simpIfTarget s₂.mvarId
     if s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂ then
+      trace[split.failure] "`split` tactic failed to simplify target using new hypotheses Goals:\n{mvarId₁}\n{mvarId₂}"
       return none
     else
       return some ({ s₁ with mvarId := mvarId₁ }, { s₂ with mvarId := mvarId₂ })
@@ -118,6 +227,7 @@ def splitIfLocalDecl? (mvarId : MVarId) (fvarId : FVarId) (hName? : Option Name
       let mvarId₁ ← simpIfLocalDecl s₁.mvarId fvarId
       let mvarId₂ ← simpIfLocalDecl s₂.mvarId fvarId
       if s₁.mvarId == mvarId₁ && s₂.mvarId == mvarId₂ then
+        trace[split.failure] "`split` tactic failed to simplify target using new hypotheses Goals:\n{mvarId₁}\n{mvarId₂}"
         return none
       else
         return some (mvarId₁, mvarId₂)

tests/compiler/uset.lean

@@ -7,4 +7,3 @@ structure Point where
 
 def main : IO Unit :=
   IO.println (Point.right ⟨0, 0⟩).x
-

tests/lean/1113.lean

@@ -4,7 +4,7 @@ def foo: {n: Nat} → Fin n → Nat
 
 theorem t3 {f: Fin (n+1)}:
   foo f = 0 := by
-  simp only [←Nat.succ_eq_add_one n] at f
+  dsimp only [←Nat.succ_eq_add_one n] at f -- use `dsimp` to ensure we don't copy `f`
   trace_state
   simp only [←Nat.succ_eq_add_one n, foo]
 

tests/lean/rfl_simp_thm.lean

@@ -3,6 +3,6 @@ def inc (x : Nat) := x + 1
 @[simp] theorem inc_eq : inc x = x + 1 := rfl
 
 theorem ex (a b : Fin (inc n)) (h : a = b) : b = a := by
-  simp only [inc_eq] at a
+  simp +implicitDefEqProofs only [inc_eq] at a
   trace_state
   exact h.symm

tests/lean/run/4595_slowdown.lean

@@ -0,0 +1,288 @@
+-- The final declaration blew up by a factor of about 40x heartbeats on an earlier draft of
+-- https://github.com/leanprover/lean4/pull/4595, so this is here as a regression test.
+
+universe v v₁ v₂ v₃ u u₁ u₂ u₃
+
+section Mathlib.Combinatorics.Quiver.Basic
+
+class Quiver (V : Type u) where
+  Hom : V → V → Sort v
+
+infixr:10 " ⟶ " => Quiver.Hom
+
+structure Prefunctor (V : Type u₁) [Quiver.{v₁} V] (W : Type u₂) [Quiver.{v₂} W] where
+  obj : V → W
+  map : ∀ {X Y : V}, (X ⟶ Y) → (obj X ⟶ obj Y)
+
+end Mathlib.Combinatorics.Quiver.Basic
+
+section Mathlib.CategoryTheory.Category.Basic
+
+namespace CategoryTheory
+
+class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
+  id : ∀ X : obj, Hom X X
+  comp : ∀ {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
+
+scoped notation "𝟙" => CategoryStruct.id
+
+scoped infixr:80 " ≫ " => CategoryStruct.comp
+
+class Category (obj : Type u) extends CategoryStruct.{v} obj : Type max u (v + 1) where
+  id_comp : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f
+  comp_id : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Category.Basic
+
+section Mathlib.CategoryTheory.Functor.Basic
+
+namespace CategoryTheory
+
+structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+    extends Prefunctor C D : Type max v₁ v₂ u₁ u₂ where
+
+infixr:26 " ⥤ " => Functor
+
+namespace Functor
+
+section
+
+variable (C : Type u₁) [Category.{v₁} C]
+
+protected def id : C ⥤ C where
+  obj X := X
+  map f := f
+
+notation "𝟭" => Functor.id
+
+variable {C}
+
+@[simp]
+theorem id_obj (X : C) : (𝟭 C).obj X = X := rfl
+
+@[simp]
+theorem id_map {X Y : C} (f : X ⟶ Y) : (𝟭 C).map f = f := rfl
+
+end
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+  {E : Type u₃} [Category.{v₃} E]
+
+def comp (F : C ⥤ D) (G : D ⥤ E) : C ⥤ E where
+  obj X := G.obj (F.obj X)
+  map f := G.map (F.map f)
+
+infixr:80 " ⋙ " => Functor.comp
+
+@[simp] theorem comp_obj (F : C ⥤ D) (G : D ⥤ E) (X : C) :
+  (F ⋙ G).obj X = G.obj (F.obj X) := rfl
+
+@[simp]
+theorem comp_map (F : C ⥤ D) (G : D ⥤ E) {X Y : C} (f : X ⟶ Y) :
+    (F ⋙ G).map f = G.map (F.map f) := rfl
+
+end Functor
+
+end CategoryTheory
+
+
+end Mathlib.CategoryTheory.Functor.Basic
+
+section Mathlib.CategoryTheory.NatTrans
+
+namespace CategoryTheory
+
+variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
+
+@[ext]
+structure NatTrans (F G : C ⥤ D) : Type max u₁ v₂ where
+  app : ∀ X : C, F.obj X ⟶ G.obj X
+  naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f
+
+protected def NatTrans.id (F : C ⥤ D) : NatTrans F F where
+  app X := 𝟙 (F.obj X)
+  naturality := sorry
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.NatTrans
+
+section Mathlib.CategoryTheory.Iso
+
+namespace CategoryTheory
+
+structure Iso {C : Type u} [Category.{v} C] (X Y : C) where
+  hom : X ⟶ Y
+  inv : Y ⟶ X
+  hom_inv_id : hom ≫ inv = 𝟙 X
+  inv_hom_id : inv ≫ hom = 𝟙 Y
+
+infixr:10 " ≅ " => Iso
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Iso
+
+section Mathlib.CategoryTheory.Functor.Category
+
+namespace CategoryTheory
+
+variable (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.{v₂} D]
+
+namespace Functor
+
+instance category : Category.{max u₁ v₂} (C ⥤ D) where
+  Hom F G := NatTrans F G
+  id F := NatTrans.id F
+  comp α β := sorry
+  id_comp := sorry
+  comp_id := sorry
+
+@[ext]
+theorem ext' {F G : C ⥤ D} {α β : F ⟶ G} (w : α.app = β.app) : α = β := NatTrans.ext w
+
+end Functor
+
+namespace NatTrans
+
+@[simp]
+theorem id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl
+
+@[simp]
+theorem comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :
+    (α ≫ β).app X = α.app X ≫ β.app X := sorry
+
+end NatTrans
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Functor.Category
+
+section Mathlib.CategoryTheory.Idempotents.Karoubi
+
+namespace CategoryTheory
+
+variable (C : Type _) [Category C]
+
+structure Karoubi where
+  X : C
+  p : X ⟶ X
+
+namespace Karoubi
+
+variable {C}
+
+structure Hom (P Q : Karoubi C) where
+  f : P.X ⟶ Q.X
+  comm : f = P.p ≫ f ≫ Q.p
+
+theorem p_comp {P Q : Karoubi C} (f : Hom P Q) : P.p ≫ f.f = f.f := sorry
+
+theorem comp_p {P Q : Karoubi C} (f : Hom P Q) : f.f ≫ Q.p = f.f := sorry
+
+/-- The category structure on the karoubi envelope of a category. -/
+instance : Category (Karoubi C) where
+  Hom := Karoubi.Hom
+  id P := ⟨P.p, sorry⟩
+  comp f g := ⟨f.f ≫ g.f, sorry⟩
+  comp_id := sorry
+  id_comp := sorry
+
+@[simp]
+theorem hom_ext_iff {P Q : Karoubi C} {f g : P ⟶ Q} : f = g ↔ f.f = g.f := sorry
+
+@[ext]
+theorem hom_ext {P Q : Karoubi C} (f g : P ⟶ Q) (h : f.f = g.f) : f = g := sorry
+
+@[simp]
+theorem comp_f {P Q R : Karoubi C} (f : P ⟶ Q) (g : Q ⟶ R) : (f ≫ g).f = f.f ≫ g.f := rfl
+
+@[simp]
+theorem id_f {P : Karoubi C} : Hom.f (𝟙 P) = P.p := rfl
+
+end Karoubi
+
+def toKaroubi : C ⥤ Karoubi C where
+  obj X := ⟨X, 𝟙 X⟩
+  map f := ⟨f, sorry⟩
+
+@[simp] theorem toKaroubi_obj_X (X : C) : ((toKaroubi C).obj X).X = X := rfl
+@[simp] theorem toKaroubi_obj_p (X : C) : ((toKaroubi C).obj X).p = 𝟙 X := rfl
+@[simp] theorem toKaroubi_map_f {X Y : C} (f : X ⟶ Y) : ((toKaroubi C).map f).f = f := rfl
+
+end CategoryTheory
+
+end Mathlib.CategoryTheory.Idempotents.Karoubi
+
+section Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
+
+open CategoryTheory.Category
+open CategoryTheory.Karoubi
+
+namespace CategoryTheory
+namespace Idempotents
+
+variable (C : Type _) [Category C]
+
+theorem idem_f (P : Karoubi (Karoubi C)) : P.p.f ≫ P.p.f = P.p.f := sorry
+
+theorem p_comm_f {P Q : Karoubi (Karoubi C)} (f : P ⟶ Q) : P.p.f ≫ f.f.f = f.f.f ≫ Q.p.f := sorry
+
+def inverse : Karoubi (Karoubi C) ⥤ Karoubi C where
+  obj P := ⟨P.X.X, P.p.f⟩
+  map f := ⟨f.f.f, sorry⟩
+
+theorem inverse_obj_X (P : Karoubi (Karoubi C)) : ((inverse C).obj P).X = P.X.X := rfl
+theorem inverse_obj_p (P : Karoubi (Karoubi C)) : ((inverse C).obj P).p = P.p.f := rfl
+theorem inverse_map_f {X Y : Karoubi (Karoubi C)} (f : X ⟶ Y) : ((inverse C).map f).f = f.f.f := rfl
+
+-- In the original source this is just
+-- ```
+-- def counitIso : inverse C ⋙ toKaroubi (Karoubi C) ≅ 𝟭 (Karoubi (Karoubi C)) where
+--   hom := { app := fun P => { f := { f := P.p.1 } } }
+--   inv := { app := fun P => { f := { f := P.p.1 }  } }
+-- ```
+-- but I've maximally expanded out the autoparams:
+-- it seems the slow down is in the `simp only` tactics, not the automation that finds them.
+
+def counitIso : inverse C ⋙ toKaroubi (Karoubi C) ≅ 𝟭 (Karoubi (Karoubi C)) where
+  hom :=
+    { app := fun P =>
+        { f :=
+            { f := P.p.1
+              comm := by simp only [Functor.comp_obj, toKaroubi_obj_X, inverse_obj_X,
+                Functor.id_obj, inverse_obj_p, comp_p, idem_f] }
+          comm := by simp only [Functor.comp_obj, toKaroubi_obj_X, Functor.id_obj, toKaroubi_obj_p,
+            Karoubi.id_f, inverse_obj_p, hom_ext_iff, inverse_obj_X, comp_f, idem_f] }
+      naturality := by
+        intro X Y f
+        simp only [Functor.comp_obj, Functor.id_obj, Functor.comp_map, toKaroubi_obj_X,
+          Functor.id_map, hom_ext_iff, comp_f, toKaroubi_map_f, inverse_obj_X, inverse_map_f,
+          p_comm_f] }
+  inv :=
+    { app := fun P =>
+        { f :=
+            { f := P.p.1
+              comm := by simp only [Functor.id_obj, Functor.comp_obj, toKaroubi_obj_X,
+                inverse_obj_X, inverse_obj_p, idem_f, p_comp] }
+          comm := by simp only [Functor.id_obj, Functor.comp_obj, toKaroubi_obj_X, toKaroubi_obj_p,
+            Karoubi.id_f, inverse_obj_p, hom_ext_iff, inverse_obj_X, comp_f, idem_f] }
+      naturality := by
+        intro X Y f
+        simp only [Functor.id_obj, Functor.comp_obj, Functor.id_map, toKaroubi_obj_X,
+          Functor.comp_map, hom_ext_iff, comp_f, toKaroubi_map_f, inverse_obj_X, inverse_map_f,
+          p_comm_f]
+    }
+  hom_inv_id := by
+    simp only [Functor.comp_obj, Functor.id_obj, toKaroubi_obj_X]
+    ext x : 4
+    simp only [Functor.comp_obj, toKaroubi_obj_X, inverse_obj_X, NatTrans.comp_app,
+      Functor.id_obj, comp_f, idem_f, NatTrans.id_app, Karoubi.id_f, toKaroubi_obj_p,
+      inverse_obj_p]
+  inv_hom_id := by
+    simp only [Functor.id_obj, Functor.comp_obj, toKaroubi_obj_X]
+    ext x : 4
+    simp only [Functor.id_obj, NatTrans.comp_app, Functor.comp_obj, comp_f, toKaroubi_obj_X,
+      inverse_obj_X, idem_f, NatTrans.id_app, Karoubi.id_f]

tests/lean/run/4595_split.lean

@@ -0,0 +1,13 @@
+example {P} [Decidable P] {f g : Nat → Nat} {x : Nat} : (if P then f else g) x = 37 := by
+  split
+  · guard_target =ₛ  f x = 37
+    sorry
+  · guard_target =ₛ  g x = 37
+    sorry
+
+example {P} [Decidable P] {f g : Nat → Nat} {x : Nat} {b : Bool} : (match b with | true => f | false => g) x = 37 := by
+  split
+  · guard_target =ₛ  f x = 37
+    sorry
+  · guard_target =ₛ  g x = 37
+    sorry

tests/lean/run/implicitRflProofs.lean

@@ -0,0 +1,25 @@
+def f (x : Nat) := x + 1
+
+theorem f_eq (x : Nat) : f (x + 1) = x + 2 := rfl
+
+theorem ex1 : f (f (x + 1)) = x + 3 := by
+  simp -implicitDefEqProofs [f_eq]
+
+/--
+info: theorem ex1 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 :=
+fun {x} =>
+  of_eq_true
+    (Eq.trans (congrArg (fun x_1 => x_1 = x + 3) (Eq.trans (congrArg f (f_eq x)) (f_eq (x + 1)))) (eq_self (x + 1 + 2)))
+-/
+#guard_msgs in
+#print ex1
+
+theorem ex2 : f (f (x + 1)) = x + 3 := by
+  simp +implicitDefEqProofs [f_eq]
+
+/--
+info: theorem ex2 : ∀ {x : Nat}, f (f (x + 1)) = x + 3 :=
+fun {x} => of_eq_true (eq_self (x + 1 + 2))
+-/
+#guard_msgs in
+#print ex2

tests/lean/run/simp2.lean

@@ -4,7 +4,7 @@ def p (x : Prop) := x
  rfl
 
 theorem ex1 (x : Prop) (h : x) : p x := by
-  simp
+  simp +implicitDefEqProofs
   assumption
 
 /--
@@ -14,6 +14,17 @@ fun x h => id h
 #guard_msgs in
 #print ex1
 
+theorem ex1' (x : Prop) (h : x) : p x := by
+  simp -implicitDefEqProofs
+  assumption
+
+/--
+info: theorem ex1' : ∀ (x : Prop), x → p x :=
+fun x h => Eq.mpr (id (lemma1 x)) h
+-/
+#guard_msgs in
+#print ex1'
+
 theorem ex2 (x : Prop) (q : Prop → Prop) (h₁ : x) (h₂ : q x = x) : q x := by
   simp [h₂]
   assumption

tests/lean/run/simp5.lean

@@ -4,15 +4,27 @@ theorem f_Eq {α} (a b : α) : f a b = a :=
   rfl
 
 theorem ex1 (a b c : α) : f (f a b) c = a := by
-  simp [f_Eq]
+  simp -implicitDefEqProofs [f_Eq]
 
 /--
 info: theorem ex1.{u_1} : ∀ {α : Sort u_1} (a b c : α), f (f a b) c = a :=
-fun {α} a b c => of_eq_true (eq_self a)
+fun {α} a b c =>
+  of_eq_true
+    (Eq.trans (congrArg (fun x => x = a) (Eq.trans (congrArg (fun x => f x c) (f_Eq a b)) (f_Eq a c))) (eq_self a))
 -/
 #guard_msgs in
 #print ex1
 
+theorem ex1' (a b c : α) : f (f a b) c = a := by
+  simp +implicitDefEqProofs [f_Eq]
+
+/--
+info: theorem ex1'.{u_1} : ∀ {α : Sort u_1} (a b c : α), f (f a b) c = a :=
+fun {α} a b c => of_eq_true (eq_self a)
+-/
+#guard_msgs in
+#print ex1'
+
 theorem ex2 (p : Nat → Bool) (x : Nat) (h : p x = true) : (if p x then 1 else 2) = 1 := by
   simp [h]
 

tests/lean/run/splitIssue2.lean

@@ -0,0 +1,71 @@
+namespace Batteries
+
+/-- Union-find node type -/
+structure UFNode where
+  /-- Parent of node -/
+  parent : Nat
+
+namespace UnionFind
+
+/-- Parent of a union-find node, defaults to self when the node is a root -/
+def parentD (arr : Array UFNode) (i : Nat) : Nat :=
+  if h : i < arr.size then (arr.get i h).parent else i
+
+/-- Rank of a union-find node, defaults to 0 when the node is a root -/
+def rankD (arr : Array UFNode) (i : Nat) : Nat := 0
+
+theorem parentD_of_not_lt : ¬i < arr.size → parentD arr i = i := sorry
+
+theorem parentD_set {arr : Array UFNode} {x h v i} :
+    parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i := by
+  rw [parentD]
+  sorry
+
+end UnionFind
+
+open UnionFind
+
+structure UnionFind where
+  arr : Array UFNode
+
+namespace UnionFind
+
+/-- Size of union-find structure. -/
+@[inline] abbrev size (self : UnionFind) := self.arr.size
+
+/-- Parent of union-find node -/
+abbrev parent (self : UnionFind) (i : Nat) : Nat := parentD self.arr i
+
+theorem parent_lt (self : UnionFind) (i : Nat) : self.parent i < self.size ↔ i < self.size :=
+  sorry
+
+/-- Rank of union-find node -/
+abbrev rank (self : UnionFind) (i : Nat) : Nat := rankD self.arr i
+
+/-- Maximum rank of nodes in a union-find structure -/
+noncomputable def rankMax (self : UnionFind) := 0
+
+/-- Root of a union-find node. -/
+def root (self : UnionFind) (x : Fin self.size) : Fin self.size :=
+  let y := (self.arr.get x.1 x.2).parent
+  if h : y = x then
+    x
+  else
+    have : self.rankMax - self.rank (self.arr.get x.1 x.2).parent < self.rankMax - self.rank x :=
+      sorry
+    self.root ⟨y, sorry⟩
+termination_by self.rankMax - self.rank x
+
+/-- Root of a union-find node. Returns input if index is out of bounds. -/
+def rootD (self : UnionFind) (x : Nat) : Nat :=
+  if h : x < self.size then self.root ⟨x, h⟩ else x
+
+theorem rootD_parent (self : UnionFind) (x : Nat) : self.rootD (self.parent x) = self.rootD x := by
+  simp only [rootD, Array.length_toList, parent_lt]
+  split
+  · simp only [parentD, ↓reduceDIte, *]
+    conv => rhs; rw [root]
+    split
+    · rw [root, dif_pos] <;> simp_all
+    · simp
+  · simp only [not_false_eq_true, parentD_of_not_lt, *]

tests/lean/run/splitOrderIssue.lean

@@ -0,0 +1,10 @@
+example (b : Bool) : (if (if b then true else true) then 1 else 2) = 1 := by
+  split
+  next h =>
+    guard_target =ₛ (if true = true then 1 else 2) = 1
+    guard_hyp h : b = true
+    simp
+  next h =>
+    guard_target =ₛ (if true = true then 1 else 2) = 1
+    guard_hyp h : ¬b = true
+    simp