diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean
index d04bf0dc46..6a97c4094d 100644
--- a/src/Lean/Elab/Tactic/Ext.lean
+++ b/src/Lean/Elab/Tactic/Ext.lean
@@ -13,6 +13,9 @@ import Lean.Elab.Tactic.Repeat
 import Lean.Elab.Tactic.BuiltinTactic
 import Lean.Elab.Command
 import Lean.Linter.Basic
+-- These public imports are needed because for now we make `extCore` public.
+public import Lean.Expr
+public import Lean.Elab.Term.TermElabM
 
 /-!
 # Implementation of the `@[ext]` attribute
@@ -296,7 +299,8 @@ in extensionality theorems like `funext`. Returns a list of subgoals.
 This is built on top of `withExtN`, running in `TermElabM` to build the list of new subgoals.
 (And, for each goal, the patterns consumed.)
 -/
-def extCore (g : MVarId) (pats : List (TSyntax `rcasesPat))
+-- This is public as it is used in the implementation of `rcongr` in Batteries.
+public def extCore (g : MVarId) (pats : List (TSyntax `rcasesPat))
     (depth := 100) (failIfUnchanged := true) :
     TermElabM (Nat × Array (MVarId × List (TSyntax `rcasesPat))) := do
   StateT.run (m := TermElabM) (s := #[])
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index b2cc1ac606..8de637c8ae 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -23,6 +23,17 @@ import Lean.Elab.App
 import Lean.Elab.Match
 import Lean.Elab.Tactic.Generalize
 
+public section
+
+register_builtin_option tactic.customEliminators : Bool := {
+  defValue := true
+  group    := "tactic"
+  descr    := "enable using custom eliminators in the 'induction' and 'cases' tactics \
+    defined using the '@[induction_eliminator]' and '@[cases_eliminator]' attributes"
+}
+
+end
+
 namespace Lean.Elab.Tactic
 open Meta
 
@@ -776,13 +787,6 @@ def elabTermForElim (stx : Syntax) : TermElabM Expr := do
     else
       return e
 
-register_builtin_option tactic.customEliminators : Bool := {
-  defValue := true
-  group    := "tactic"
-  descr    := "enable using custom eliminators in the 'induction' and 'cases' tactics \
-    defined using the '@[induction_eliminator]' and '@[cases_eliminator]' attributes"
-}
-
 -- `optElimId` is of the form `("using" term)?`
 def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (induction : Bool) : TacticM ElimInfo := do
   let getBaseName? (elimName : Name) : MetaM (Option Name) := do