fix: make .congr_simp theorems private

src/Init/Core.lean

@@ -2548,3 +2548,4 @@ class Irrefl (r : α → α → Prop) : Prop where
   irrefl : ∀ a, ¬r a a
 
 end Std
+#print ite.congr_simp

src/Init/Prelude.lean

@@ -629,6 +629,7 @@ structure Subtype {α : Sort u} (p : α → Prop) where
   The proof that `val` satisfies the predicate `p`.
   -/
   property : p val
+realize_const Subtype.mk.congr_simp
 
 set_option linter.unusedVariables.funArgs false in
 /--
@@ -1052,6 +1053,7 @@ or derive `i < arr.size` from some other proposition that we are checking in the
 -/
 @[macro_inline] def dite {α : Sort u} (c : Prop) [h : Decidable c] (t : c → α) (e : Not c → α) : α :=
   h.casesOn e t
+realize_const dite.congr_simp
 
 /-! # if-then-else -/
 
@@ -2261,6 +2263,7 @@ structure Fin (n : Nat) where
   The number `val` is strictly less than the bound `n`.
   -/
   isLt : LT.lt val n
+realize_const Fin.mk.congr_simp
 
 attribute [coe] Fin.val
 

src/Init/SimpLemmas.lean

@@ -13,6 +13,9 @@ public import Init.Core
 public section
 set_option linter.missingDocs true -- keep it documented
 
+realize_const ite.congr_simp
+realize_const Decidable.decide.congr_simp
+
 theorem of_eq_true (h : p = True) : p := h ▸ trivial
 theorem of_eq_false (h : p = False) : ¬ p := fun hp => False.elim (h.mp hp)
 

src/Lean/Elab/PreDefinition/Main.lean

@@ -368,19 +368,23 @@ def addPreDefinitions (docCtx : LocalContext × LocalInstances) (preDefs : Array
                   m!"fail to show termination for{indentD (MessageData.joinSep preDefMsgs Format.line)}\nwith errors\n{msg}")
           catch ex =>
             logException ex
+            let env ← getEnv
+            let missingPreDefs := preDefs.filter (!env.contains ·.declName)
+            if missingPreDefs.isEmpty then
+              continue
             let s ← saveState
             try
               if preDefs.all fun preDef => (preDef.kind matches DefKind.def | DefKind.instance) || preDefs.all fun preDef => preDef.kind == DefKind.abbrev then
                 -- try to add as partial definition
                 withOptions (Elab.async.set · false) do
                   try
-                    addAndCompilePartial docCtx preDefs (useSorry := true)
+                    addAndCompilePartial docCtx missingPreDefs (useSorry := true)
                   catch _ =>
                     -- Compilation failed try again just as axiom
                     s.restore
-                    addSorried docCtx preDefs
-              else if preDefs.all fun preDef => preDef.kind == DefKind.theorem then
-                addSorried docCtx preDefs
+                    addSorried docCtx missingPreDefs
+              else if missingPreDefs.all fun preDef => preDef.kind == DefKind.theorem then
+                addSorried docCtx missingPreDefs
             catch _ => s.restore
 
 builtin_initialize

src/Lean/Meta/CongrTheorems.lean

@@ -411,13 +411,17 @@ builtin_initialize congrKindsExt : MapDeclarationExtension (Array CongrArgKind)
 
 builtin_initialize registerReservedNamePredicate fun env n =>
   match n with
-  | .str p s => (isHCongrReservedNameSuffix s || s == congrSimpSuffix) && env.contains p
+  | .str p s => (isHCongrReservedNameSuffix s || s == congrSimpSuffix) && (env.contains p || (privateToUserName? p |>.any env.contains))
   | _ => false
 
 builtin_initialize
   registerReservedNameAction fun name => do
-    let .str p s := name | return false
-    unless (← getEnv).contains p do return false
+    let mut .str p s := name | return false
+    unless (← getEnv).contains p do
+      if let some p' := privateToUserName? p |>.filter (← getEnv).contains then
+        p := p'
+      else
+        return false
     if isHCongrReservedNameSuffix s then
       let numArgs := (s.drop 7).toNat!
       try MetaM.run' do
@@ -475,7 +479,10 @@ Similar to `mkCongrSimp?`, but uses reserved names to ensure we don't keep creat
 same congruence theorem over and over again.
 -/
 def mkCongrSimpForConst? (declName : Name) (levels : List Level) : MetaM (Option CongrTheorem) := do
-  let thmName := Name.str declName congrSimpSuffix
+  let mut thmName := Name.str declName congrSimpSuffix
+  if !((← getEnv).setExporting true |>.containsOnBranch thmName) && (← getEnv).isImportedConst declName then
+    -- Keep local to current module unless `declName` is public decl from this module.
+    thmName := mkPrivateName (← getEnv) thmName
   try
     unless (← getEnv).containsOnBranch thmName do
       let _ ← executeReservedNameAction thmName