From 127fe785a3fc20b75d9e059eb67eb4cab14c30b0 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Fri, 17 Oct 2025 08:48:41 +1100
Subject: [PATCH] chore: add public modifiers in Lean.Elab.Tactic.Ext (#10809)

This PR restores further definitions to `public`, after #10699.
---
 src/Lean/Elab/Tactic/Ext.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean
index 0f5bdcf168..44cd7e3ac5 100644
--- a/src/Lean/Elab/Tactic/Ext.lean
+++ b/src/Lean/Elab/Tactic/Ext.lean
@@ -178,8 +178,7 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do
 ### Attribute
 -/
 
-abbrev extExtension := Meta.Ext.extExtension
-abbrev getExtTheorems := Meta.Ext.getExtTheorems
+open Ext
 
 builtin_initialize registerBuiltinAttribute {
   name := `ext
@@ -220,7 +219,8 @@ builtin_initialize registerBuiltinAttribute {
 -/
 
 /-- Apply a single extensionality theorem to `goal`. -/
-def applyExtTheoremAt (goal : MVarId) : MetaM (List MVarId) := goal.withContext do
+-- Tis is public for now as it is used internally in `aesop`.
+public def applyExtTheoremAt (goal : MVarId) : MetaM (List MVarId) := goal.withContext do
   let tgt ← goal.getType'
   unless tgt.isAppOfArity ``Eq 3 do
     throwError "This extensionality tactic only applies to equalities, not{indentExpr tgt}"