diff --git a/CMakeLists.txt b/CMakeLists.txt
index a6dcfbeb3c..583aaaba0a 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -12,6 +12,8 @@ foreach(var ${vars})
   get_property(currentHelpString CACHE "${var}" PROPERTY HELPSTRING)
   if("${var}" MATCHES "STAGE0_(.*)")
     list(APPEND STAGE0_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
+  elseif("${var}" MATCHES "STAGE1_(.*)")
+    list(APPEND STAGE1_ARGS "-D${CMAKE_MATCH_1}=${${var}}")
   elseif("${currentHelpString}" MATCHES "No help, variable specified on the command line." OR "${currentHelpString}" STREQUAL "")
     list(APPEND CL_ARGS "-D${var}=${${var}}")
     if("${var}" MATCHES "USE_GMP|CHECK_OLEAN_VERSION")
@@ -77,26 +79,29 @@ if (USE_MIMALLOC)
   list(APPEND EXTRA_DEPENDS mimalloc)
 endif()
 
-ExternalProject_add(stage0
-  SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
-  SOURCE_SUBDIR src
-  BINARY_DIR stage0
-  # do not rebuild stage0 when git hash changes; it's not from this commit anyway
-  # (however, CI will override this as we need to embed the githash into the stage 1 library built
-  # by stage 0)
-  CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
-  BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
-  INSTALL_COMMAND ""  # skip install
-  DEPENDS ${EXTRA_DEPENDS}
-)
+if (NOT STAGE1_PREV_STAGE)
+  ExternalProject_add(stage0
+    SOURCE_DIR "${LEAN_SOURCE_DIR}/stage0"
+    SOURCE_SUBDIR src
+    BINARY_DIR stage0
+    # do not rebuild stage0 when git hash changes; it's not from this commit anyway
+    # (however, CI will override this as we need to embed the githash into the stage 1 library built
+    # by stage 0)
+    CMAKE_ARGS -DSTAGE=0 -DUSE_GITHASH=OFF ${PLATFORM_ARGS} ${STAGE0_ARGS}
+    BUILD_ALWAYS ON  # cmake doesn't auto-detect changes without a download method
+    INSTALL_COMMAND ""  # skip install
+    DEPENDS ${EXTRA_DEPENDS}
+  )
+  list(APPEND EXTRA_DEPENDS stage0)
+endif()
 ExternalProject_add(stage1
   SOURCE_DIR "${LEAN_SOURCE_DIR}"
   SOURCE_SUBDIR src
   BINARY_DIR stage1
-  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS}
+  CMAKE_ARGS -DSTAGE=1 -DPREV_STAGE=${CMAKE_BINARY_DIR}/stage0 -DPREV_STAGE_CMAKE_EXECUTABLE_SUFFIX=${STAGE0_CMAKE_EXECUTABLE_SUFFIX} ${CL_ARGS} ${STAGE1_ARGS}
   BUILD_ALWAYS ON
   INSTALL_COMMAND ""
-  DEPENDS stage0
+  DEPENDS ${EXTRA_DEPENDS}
   STEP_TARGETS configure
 )
 ExternalProject_add(stage2
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 0bb3f10af2..c7cdbe667e 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1840,7 +1840,9 @@ theorem Nat.le_of_succ_le_succ {n m : Nat} : LE.le (succ n) (succ m) → LE.le n
 theorem Nat.le_of_lt_succ {m n : Nat} : LT.lt m (succ n) → LE.le m n :=
   le_of_succ_le_succ
 
-protected theorem Nat.eq_or_lt_of_le : {n m: Nat} → LE.le n m → Or (Eq n m) (LT.lt n m)
+set_option linter.missingDocs false in
+-- single generic "theorem" used in `WellFounded` reduction in core
+protected def Nat.eq_or_lt_of_le : {n m: Nat} → LE.le n m → Or (Eq n m) (LT.lt n m)
   | zero,   zero,   _ => Or.inl rfl
   | zero,   succ _, _ => Or.inr (Nat.succ_le_succ (Nat.zero_le _))
   | succ _, zero,   h => absurd h (not_succ_le_zero _)
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index 1ebd8b03ff..1cea065e74 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -40,7 +40,8 @@ noncomputable abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop
 namespace Acc
 variable {α : Sort u} {r : α → α → Prop}
 
-theorem inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
+-- `def` for `WellFounded.fix`
+def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
   h₁.recOn (fun _ ac₁ _ h₂ => ac₁ y h₂) h₂
 
 end Acc
@@ -73,7 +74,8 @@ class WellFoundedRelation (α : Sort u) where
   wf  : WellFounded rel
 
 namespace WellFounded
-theorem apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
+-- `def` for `WellFounded.fix`
+def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
   wf.rec (fun p => p) a
 
 section
@@ -162,10 +164,12 @@ private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x =
     subst x
     apply ih (f y) lt y rfl
 
-theorem accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
+-- `def` for `WellFounded.fix`
+def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
   accAux f ac a rfl
 
-theorem wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
+-- `def` for `WellFounded.fix`
+def wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
   ⟨fun a => accessible f (apply h (f a))⟩
 end InvImage
 
diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index 71620292bc..0ff185de59 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.CoreM
 import Lean.Namespace
+import Lean.Util.CollectAxioms
 
 namespace Lean
 
@@ -44,6 +45,38 @@ where go env
   | .str p _ => if isNamespaceName p then go (env.registerNamespace p) p else env
   | _        => env
 
+private builtin_initialize privateConstKindsExt : MapDeclarationExtension ConstantKind ←
+  mkMapDeclarationExtension
+
+/--
+Returns the kind of the declaration as originally declared instead of as exported. This information
+is stored by `Lean.addDecl` and may be inaccurate if that function was circumvented. Returns `none`
+if the declaration was not found.
+-/
+def getOriginalConstKind? (env : Environment) (declName : Name) : Option ConstantKind := do
+  privateConstKindsExt.find? env declName <|>
+    (env.setExporting false |>.findAsync? declName).map (·.kind)
+
+/--
+Checks whether the declaration was originally declared as a theorem; see also
+`Lean.getOriginalConstKind?`. Returns `false` if the declaration was not found.
+-/
+def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool :=
+  getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false
+
+-- HACK: remove together with MutualDef HACK when `[dsimp]` is introduced
+private def isSimpleRflProof (proof : Expr) : Bool :=
+  if let .lam _ _ proof _ := proof then
+    isSimpleRflProof proof
+  else
+    proof.isAppOfArity ``rfl 2
+
+private def looksLikeRelevantTheoremProofType (type : Expr) : Bool :=
+  if let .forallE _ _ type _ := type then
+    looksLikeRelevantTheoremProofType type
+  else
+    type.isAppOfArity ``WellFounded 2
+
 def addDecl (decl : Declaration) : CoreM Unit := do
   -- register namespaces for newly added constants; this used to be done by the kernel itself
   -- but that is incompatible with moving it to a separate task
@@ -56,19 +89,31 @@ def addDecl (decl : Declaration) : CoreM Unit := do
 
   -- convert `Declaration` to `ConstantInfo` to use as a preliminary value in the environment until
   -- kernel checking has finished; not all cases are supported yet
+  let mut exportedInfo? := none
+  let mut exportedKind? := none
   let (name, info, kind) ← match decl with
-    | .thmDecl thm => pure (thm.name, .thmInfo thm, .thm)
+    | .thmDecl thm =>
+      if (← getEnv).header.isModule && !isSimpleRflProof thm.value &&
+          -- TODO: this is horrible...
+          !looksLikeRelevantTheoremProofType thm.type then
+        exportedInfo? := some <| .axiomInfo { thm with isUnsafe := false }
+        exportedKind? := some .axiom
+      pure (thm.name, .thmInfo thm, .thm)
     | .defnDecl defn => pure (defn.name, .defnInfo defn, .defn)
     | .mutualDefnDecl [defn] => pure (defn.name, .defnInfo defn, .defn)
     | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
     | _ => return (← addSynchronously)
 
-  let env ← getEnv
+  -- preserve original constant kind in extension if different from exported one
+  if exportedKind?.isSome then
+    modifyEnv (privateConstKindsExt.insert · name kind)
+
   -- no environment extension changes to report after kernel checking; ensures we do not
   -- accidentally wait for this snapshot when querying extension states
-  let async ← env.addConstAsync (reportExts := false) name kind
+  let env ← getEnv
+  let async ← env.addConstAsync (reportExts := false) name kind (exportedKind?.getD kind)
   -- report preliminary constant info immediately
-  async.commitConst async.asyncEnv (some info)
+  async.commitConst async.asyncEnv (some info) exportedInfo?
   setEnv async.mainEnv
   let cancelTk ← IO.CancelToken.new
   let checkAct ← Core.wrapAsyncAsSnapshot (cancelTk? := cancelTk) fun _ => do
@@ -103,6 +148,8 @@ where
           let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
             |> ofExceptKernelException
           setEnv env
+          for n in decl.getTopLevelNames do
+            registerAxiomsForDecl n
         catch ex =>
           -- avoid follow-up errors by (trying to) add broken decl as axiom
           addAsAxiom
diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index 5c175072ac..c695a47bee 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -504,6 +504,7 @@ def isDefinition : ConstantInfo → Bool
   | .defnInfo _ => true
   | _           => false
 
+@[deprecated "May be inaccurate for theorems imported under the module system, use `Lean.getOriginalConstKind?` instead" (since := "2025-04-24")]
 def isTheorem : ConstantInfo → Bool
   | .thmInfo _ => true
   | _          => false
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 23987df116..d0ad5ecfe0 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -1062,7 +1062,9 @@ where
     processDeriving headers
   elabAsync header view declId := do
     let env ← getEnv
-    let async ← env.addConstAsync declId.declName .thm
+    -- HACK: should be replaced by new `[dsimp]` attribute
+    let isRflLike := header.value matches `(declVal| := rfl)
+    let async ← env.addConstAsync declId.declName .thm (exportedKind := if isRflLike then .thm else .axiom)
     setEnv async.mainEnv
 
     -- TODO: parallelize header elaboration as well? Would have to refactor auto implicits catch,
@@ -1119,7 +1121,7 @@ where
     Core.logSnapshotTask { stx? := none, task := (← BaseIO.asTask (act ())), cancelTk? := cancelTk }
     applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
     applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
-  finishElab headers := withFunLocalDecls headers fun funFVars => do
+  finishElab headers := withFunLocalDecls headers fun funFVars => withoutExporting do
     for view in views, funFVar in funFVars do
       addLocalVarInfo view.declId funFVar
     let values ← try
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index 0705cbfc71..9deecd7cd5 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -46,9 +46,13 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
 private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) (sig : Bool := true) : CommandElabM MessageData :=
   mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) (sig := sig)
 
-private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
+private def mkOmittedMsg : Option Expr → MessageData
+  | none   => "<not imported>"
+  | some e => e
+
+private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value? : Option Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
   let m ← mkHeader kind id levelParams type safety
-  let m := m ++ " :=" ++ Format.line ++ value
+  let m := m ++ " :=" ++ Format.line ++ mkOmittedMsg value?
   logInfo m
 
 private def printAxiomLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
@@ -157,7 +161,11 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar
 private def printIdCore (id : Name) : CommandElabM Unit := do
   let env ← getEnv
   match env.find? id with
-  | ConstantInfo.axiomInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
+  | ConstantInfo.axiomInfo { levelParams := us, type := t, isUnsafe := u, .. } =>
+    match getOriginalConstKind? env id with
+    | some .defn => printDefLike "def" id us t none (if u then .unsafe else .safe)
+    | some .thm => printDefLike "theorem" id us t none (if u then .unsafe else .safe)
+    | _  => printAxiomLike "axiom" id us t u
   | ConstantInfo.defnInfo  { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s
   | ConstantInfo.thmInfo  { levelParams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
   | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "opaque" id us t u
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 668370a2e6..14a063c82b 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -865,10 +865,11 @@ def PromiseCheckedResult.commitChecked (res : PromiseCheckedResult) (env : Envir
 
 /-- Data transmitted by `AddConstAsyncResult.commitConst`. -/
 private structure ConstPromiseVal where
-  privateConstInfo  : ConstantInfo
-  exportedConstInfo : ConstantInfo
-  exts              : Array EnvExtensionState
-  nestedConsts      : AsyncConsts
+  privateConstInfo     : ConstantInfo
+  exportedConstInfo    : ConstantInfo
+  exts                 : Array EnvExtensionState
+  privateNestedConsts  : AsyncConsts
+  exportedNestedConsts : AsyncConsts
 deriving Nonempty
 
 /--
@@ -951,7 +952,7 @@ def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind)
       -- any value should work here, `base` does not block
       | none   => env.base.extensions)
     consts := constPromise.result?.map (sync := true) fun
-      | some v => .mk v.nestedConsts
+      | some v => .mk v.privateNestedConsts
       | none   => .mk (α := AsyncConsts) default
   }
   let exportedAsyncConst := { privateAsyncConst with
@@ -961,6 +962,9 @@ def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind)
         | some c => c.exportedConstInfo
         | none   => mkFallbackConstInfo constName exportedKind
     }
+    consts := constPromise.result?.map (sync := true) fun
+      | some v => .mk v.exportedNestedConsts
+      | none   => .mk (α := AsyncConsts) default
   }
   return {
     constName, kind
@@ -997,7 +1001,7 @@ given environment. The declaration name and kind must match the original values
 def AddConstAsyncResult.commitConst (res : AddConstAsyncResult) (env : Environment)
     (info? : Option ConstantInfo := none) (exportedInfo? : Option ConstantInfo := none) :
     IO Unit := do
-  let info ← match info? <|> env.find? res.constName with
+  let info ← match info? <|> (env.setExporting false).find? res.constName with
     | some info => pure info
     | none =>
       throw <| .userError s!"AddConstAsyncResult.commitConst: constant {res.constName} not found in async context"
@@ -1016,9 +1020,10 @@ def AddConstAsyncResult.commitConst (res : AddConstAsyncResult) (env : Environme
       throw <| .userError s!"AddConstAsyncResult.commitConst: exported constant has different signature"
   res.constPromise.resolve {
     privateConstInfo := info
-    exportedConstInfo := exportedInfo?.getD info
+    exportedConstInfo := (exportedInfo? <|> (env.setExporting true).find? res.constName).getD info
     exts := env.base.extensions
-    nestedConsts := env.asyncConsts
+    privateNestedConsts := env.privateAsyncConsts
+    exportedNestedConsts := env.exportedAsyncConsts
   }
 
 /--
@@ -1786,8 +1791,9 @@ partial def importModulesCore (imports : Array Import) (forceImportAll := true)
     }
 
 /--
-Return `true` if `cinfo₁` and `cinfo₂` are theorems with the same name, universe parameters,
-and types. We allow different modules to prove the same theorem.
+Returns `true` if `cinfo₁` and `cinfo₂` represent the same theorem/axiom, with `cinfo₁` potentially
+being a richer representation; under the module system, a theorem may be weakened to an axiom when
+exported. We allow different modules to prove the same theorem.
 
 Motivation: We want to generate equational theorems on demand and potentially
 in different files, and we want them to have non-private names.
@@ -1804,13 +1810,15 @@ and theorems are (mostly) opaque in Lean. For `Acc.rec`, we may unfold theorems
 during type-checking, but we are assuming this is not an issue in practice,
 and we are planning to address this issue in the future.
 -/
-private def equivInfo (cinfo₁ cinfo₂ : ConstantInfo) : Bool := Id.run do
-  let .thmInfo tval₁ := cinfo₁ | false
-  let .thmInfo tval₂ := cinfo₂ | false
-  return tval₁.name == tval₂.name
-    && tval₁.type == tval₂.type
-    && tval₁.levelParams == tval₂.levelParams
-    && tval₁.all == tval₂.all
+private def subsumesInfo (cinfo₁ cinfo₂ : ConstantInfo) : Bool :=
+  cinfo₁.name == cinfo₂.name &&
+    cinfo₁.type == cinfo₂.type &&
+    cinfo₁.levelParams == cinfo₂.levelParams &&
+    match cinfo₁, cinfo₂ with
+    | .thmInfo tval₁, .thmInfo tval₂ => tval₁.all == tval₂.all
+    | .thmInfo tval₁, .axiomInfo aval₂ => tval₁.all == [aval₂.name] && !aval₂.isUnsafe
+    | .axiomInfo aval₁, .axiomInfo aval₂ => aval₁.isUnsafe == aval₂.isUnsafe
+    | _, _ => false
 
 /--
 Constructs environment from `importModulesCore` results.
@@ -1836,7 +1844,9 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
         constantMap := constantMap'
         if let some cinfoPrev := cinfoPrev? then
           -- Recall that the map has not been modified when `cinfoPrev? = some _`.
-          unless equivInfo cinfoPrev cinfo do
+          if subsumesInfo cinfo cinfoPrev then
+            constantMap := constantMap.insert cname cinfo
+          else if !subsumesInfo cinfoPrev cinfo then
             throwAlreadyImported s const2ModIdx modIdx cname
       const2ModIdx := const2ModIdx.insertIfNew cname modIdx
     for cname in mod.extraConstNames do
diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
index 655de992aa..7d6f964903 100644
--- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
+++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean
@@ -571,7 +571,8 @@ def mkEMatchTheoremCore (origin : Origin) (levelParams : Array Name) (numParams
 
 private def getProofFor (declName : Name) : MetaM Expr := do
   let info ← getConstInfo declName
-  unless info.isTheorem do
+  -- For theorems, `isProp` has already been checked at declaration time
+  unless wasOriginallyTheorem (← getEnv) declName do
     unless (← isProp info.type) do
       throwError "invalid E-matching theorem `{declName}`, type is not a proposition"
   let us := info.levelParams.map mkLevelParam
@@ -868,7 +869,7 @@ def mkEMatchEqTheoremsForDef? (declName : Name) : MetaM (Option (Array EMatchThe
     mkEMatchEqTheorem eqn (normalizePattern := true)
 
 private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatchTheoremKind) (useLhs := true) : MetaM Unit := do
-  if (← getConstInfo declName).isTheorem then
+  if wasOriginallyTheorem (← getEnv) declName then
     ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs)) attrKind
   else if let some thms ← mkEMatchEqTheoremsForDef? declName then
     unless useLhs do
@@ -880,8 +881,7 @@ private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind
 def EMatchTheorems.eraseDecl (s : EMatchTheorems) (declName : Name) : MetaM EMatchTheorems := do
   let throwErr {α} : MetaM α :=
     throwError "`{declName}` is not marked with the `[grind]` attribute"
-  let info ← getConstInfo declName
-  if !info.isTheorem then
+  if !wasOriginallyTheorem (← getEnv) declName then
     if let some eqns ← getEqnsFor? declName then
        let s := ematchTheoremsExt.getState (← getEnv)
        unless eqns.all fun eqn => s.contains (.decl eqn) do
@@ -904,7 +904,7 @@ def addEMatchAttr (declName : Name) (attrKind : AttributeKind) (thmKind : EMatch
     addGrindEqAttr declName attrKind thmKind (useLhs := false)
   else
     let info ← getConstInfo declName
-    if !info.isTheorem && !info.isCtor && !info.isAxiom then
+    if !wasOriginallyTheorem (← getEnv) declName && !info.isCtor && !info.isAxiom then
       addGrindEqAttr declName attrKind thmKind
     else
       let thm ← mkEMatchTheoremForDecl declName thmKind
diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean
index 783ba97daf..04d0bfd2f0 100644
--- a/src/Lean/Server/Completion/CompletionCollectors.lean
+++ b/src/Lean/Server/Completion/CompletionCollectors.lean
@@ -79,7 +79,7 @@ section Infrastructure
         return CompletionItemKind.enum
       else
         return CompletionItemKind.struct
-    else if constInfo.isTheorem then
+    else if wasOriginallyTheorem env constInfo.name then
       return CompletionItemKind.event
     else if (← isProjectionFn constInfo.name) then
       return CompletionItemKind.field
diff --git a/src/Lean/Util/CollectAxioms.lean b/src/Lean/Util/CollectAxioms.lean
index e95eb79466..50975a554a 100644
--- a/src/Lean/Util/CollectAxioms.lean
+++ b/src/Lean/Util/CollectAxioms.lean
@@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.MonadEnv
-import Lean.Util.FoldConsts
+import Lean.CoreM
 
 namespace Lean
 
-namespace CollectAxioms
+private builtin_initialize exportedAxiomsExt : MapDeclarationExtension (Array Name) ← mkMapDeclarationExtension
 
+namespace CollectAxioms
 
 structure State where
   visited : NameSet    := {}
@@ -18,12 +18,19 @@ structure State where
 
 abbrev M := ReaderT Environment $ StateM State
 
-partial def collect (c : Name) : M Unit := do
+private partial def collect (c : Name) : M Unit := do
   let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM collect
   let s ← get
   unless s.visited.contains c do
     modify fun s => { s with visited := s.visited.insert c }
     let env ← read
+    if let some axioms := exportedAxiomsExt.find? env c then
+      for ax in axioms do
+        if ax == c then
+          modify fun s => { s with axioms := s.axioms.push c }
+        else
+          collect ax
+      return
     -- We should take the constant from the kernel env, which may differ from the one in the elab
     -- env in case of (async) errors.
     match env.checked.get.find? c with
@@ -44,4 +51,8 @@ def collectAxioms [Monad m] [MonadEnv m] (constName : Name) : m (Array Name) :=
   let (_, s) := ((CollectAxioms.collect constName).run env).run {}
   pure s.axioms
 
+def registerAxiomsForDecl (n : Name) : CoreM Unit := do
+  let axioms ← collectAxioms n
+  modifyEnv (exportedAxiomsExt.addEntry · (n, axioms))
+
 end Lean
diff --git a/src/Std/Sat/AIG/RefVec.lean b/src/Std/Sat/AIG/RefVec.lean
index 77f3daae1f..4bac4bfdc0 100644
--- a/src/Std/Sat/AIG/RefVec.lean
+++ b/src/Std/Sat/AIG/RefVec.lean
@@ -73,7 +73,7 @@ def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) :=
 @[simp]
 theorem cast_cast {aig1 aig2 aig3 : AIG α} (s : RefVec aig1 len)
     (h1 : aig1.decls.size ≤ aig2.decls.size) (h2 : aig2.decls.size ≤ aig3.decls.size) :
-    (s.cast h1).cast h2 = s.cast (Nat.le_trans h1 h2) := by rfl
+    (s.cast h1).cast h2 = s.cast (Nat.le_trans h1 h2) := rfl
 
 @[simp]
 theorem get_push_ref_eq (s : RefVec aig len) (ref : AIG.Ref aig) :
diff --git a/tests/pkg/module/Module.lean b/tests/pkg/module/Module.lean
index 4099728865..4a404bcd39 100644
--- a/tests/pkg/module/Module.lean
+++ b/tests/pkg/module/Module.lean
@@ -21,3 +21,18 @@ open Lean
   let _ ← Core.CoreM.toIO (ctx := { fileName := "module.lean", fileMap := default }) (s := { env }) do
     assert! (← findDeclarationRanges? ``f).isSome
     assert! (getModuleDoc? (← getEnv) `Module.Basic).any (·.size == 1)
+
+/-! Theorems should be exported without their bodies -/
+
+/--
+info: theorem t : f = 1 :=
+<not imported>
+-/
+#guard_msgs in
+#print t
+
+/-- error: dsimp made no progress -/
+#guard_msgs in
+example : f = 1 := by dsimp only [t]
+
+example : t = t := by dsimp only [trfl]
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
index 4d76fdd264..4a74d8918a 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/tests/pkg/module/Module/Basic.lean
@@ -6,4 +6,6 @@ module
 def f := 1
 
 /-- A theorem. -/
-theorem t : f = f := rfl
+theorem t : f = 1 := sorry
+
+theorem trfl : f = 1 := rfl