fix: casesOnSameCtor: export if not private (#10273)

This PR tries to do the right thing about the visibility of the
same-ctor-match-construct.

src/Lean/Meta/Constructions/CasesOnSameCtor.lean

@@ -95,13 +95,14 @@ public def mkCasesOnSameCtorHet (declName : Name) (indName : Name) : MetaM Unit
         let e := mkApp e (← mkEqSymm heq)
         mkLambdaFVars (params ++ #[motive] ++ ism1 ++ ism2 ++ #[heq] ++ alts) e
 
-  addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
-    (name        := declName)
-    (levelParams := casesOnInfo.levelParams)
-    (type        := (← inferType e))
-    (value       := e)
-    (hints       := ReducibilityHints.abbrev)
-  ))
+  withExporting (isExporting := !isPrivateName declName) do
+    addAndCompile (.defnDecl (← mkDefinitionValInferringUnsafe
+      (name        := declName)
+      (levelParams := casesOnInfo.levelParams)
+      (type        := (← inferType e))
+      (value       := e)
+      (hints       := ReducibilityHints.abbrev)
+    ))
   modifyEnv fun env => markAuxRecursor env declName
   modifyEnv fun env => addToCompletionBlackList env declName
   modifyEnv fun env => addProtected env declName
@@ -229,7 +230,8 @@ public def mkCasesOnSameCtor (declName : Name) (indName : Name) : MetaM Unit :=
           discrInfos := #[{}, {}, {}]}
 
         -- Compare attributes with `mkMatcherAuxDefinition`
-        addDecl decl
+        withExporting (isExporting := !isPrivateName declName) do
+          addDecl decl
         Elab.Term.elabAsElim.setTag declName
         Match.addMatcherInfo declName matcherInfo
         setInlineAttribute declName