From 3ce7d4ef5c85db47439cf3a9d8adf280a9dda768 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@lean-fro.org>
Date: Wed, 22 Oct 2025 21:32:26 +0200
Subject: [PATCH] chore: minor optimizations on the critical path (#10900)

This PR optimizes two `String` proofs and makes sure that
`MkIffOfInductiveProp` does not import `Lean.Elab.Tactic`, which
previously pushed it to the very end of the import graph.
---
 src/Init/Data/String/Basic.lean         | 1 +
 src/Init/Data/String/Decode.lean        | 3 ++-
 src/Lean/Elab/MutualInductive.lean      | 1 +
 src/Lean/Meta/MkIffOfInductiveProp.lean | 8 +++++++-
 4 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index 9c91aa7dc2..000e69b90f 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -374,6 +374,7 @@ private theorem ByteArray.utf8Decode?go_eq_utf8Decode?go_extract {b : ByteArray}
       simp only [size_extract, Nat.le_refl, Nat.min_eq_left, Option.map_map, ByteArray.extract_extract]
       have : (fun x => acc ++ x) ∘ (fun x => #[c] ++ x) = fun x => acc.push c ++ x := by funext; simp
       simp [(by omega : i + (b.size - i) = b.size), this]
+termination_by fuel
 
 theorem ByteArray.utf8Decode?_utf8Encode_singleton_append {l : ByteArray} {c : Char} :
     ([c].utf8Encode ++ l).utf8Decode? = l.utf8Decode?.map (#[c] ++ ·) := by
diff --git a/src/Init/Data/String/Decode.lean b/src/Init/Data/String/Decode.lean
index 9d186bcdb2..7be522d5ac 100644
--- a/src/Init/Data/String/Decode.lean
+++ b/src/Init/Data/String/Decode.lean
@@ -1464,7 +1464,8 @@ public theorem ByteArray.isUTF8FirstByte_getElem_zero_utf8EncodeChar_append {c :
 public theorem ByteArray.isUTF8FirstByte_of_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat}
     (h : (utf8DecodeChar? b i).isSome) : (b[i]'(lt_size_of_isSome_utf8DecodeChar? h)).IsUTF8FirstByte := by
   rw [utf8DecodeChar?_eq_utf8DecodeChar?_extract] at h
-  suffices ((b.extract i b.size)[0]'(lt_size_of_isSome_utf8DecodeChar? h)).IsUTF8FirstByte by
+  suffices ((b.extract i b.size)[0]'
+      (by simpa using lt_size_of_isSome_utf8DecodeChar? h)).IsUTF8FirstByte by
     simpa [ByteArray.getElem_extract, Nat.add_zero] using this
   obtain ⟨c, hc⟩ := Option.isSome_iff_exists.1 h
   conv => congr; congr; rw [eq_of_utf8DecodeChar?_eq_some hc]
diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean
index d362c9dcf4..463f13b019 100644
--- a/src/Lean/Elab/MutualInductive.lean
+++ b/src/Lean/Elab/MutualInductive.lean
@@ -15,6 +15,7 @@ import Lean.Elab.ComputedFields
 import Lean.Meta.Constructions.CtorIdx
 import Lean.Meta.Constructions.CtorElim
 import Lean.Meta.IndPredBelow
+import Lean.Meta.Injective
 
 public section
 
diff --git a/src/Lean/Meta/MkIffOfInductiveProp.lean b/src/Lean/Meta/MkIffOfInductiveProp.lean
index eb7320e58b..e1174a9dfa 100644
--- a/src/Lean/Meta/MkIffOfInductiveProp.lean
+++ b/src/Lean/Meta/MkIffOfInductiveProp.lean
@@ -12,7 +12,13 @@ module
 
 prelude
 
-public import Lean.Elab.Tactic
+public import Lean.Meta.Basic
+import Lean.Elab.Term.TermElabM
+import Lean.Elab.Tactic.Basic
+import Lean.Meta.Tactic.Apply
+import Lean.Meta.Tactic.Intro
+import Lean.Meta.Tactic.Cases
+
 
 namespace Lean.Meta