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.

Author: TwoFX

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

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]

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
 

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