diff --git a/RELEASES.md b/RELEASES.md
index f23616684e54..ee28c1a13f5b 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -13,6 +13,8 @@ v4.8.0 (development in progress)
 
 * Lean now generates an error if the type of a theorem is **not** a proposition.
 
+* Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).
+
 * New command `derive_functinal_induction`:
 
   Derived from the definition of a (possibly mutually) recursive function
diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean
index 7e7dc52344f8..053593076b09 100644
--- a/src/Lean/Data/HashMap.lean
+++ b/src/Lean/Data/HashMap.lean
@@ -116,6 +116,22 @@ def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapI
       else
         (expand size' buckets', false)
 
+@[inline] def insertIfNew [beq : BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β × Option β :=
+  match m with
+  | ⟨size, buckets⟩ =>
+    let ⟨i, h⟩ := mkIdx (hash a) buckets.property
+    let bkt    := buckets.val[i]
+    if let some b := bkt.find? a then
+      (m, some b)
+    else
+      let size'    := size + 1
+      let buckets' := buckets.update i (AssocList.cons a b bkt) h
+      if numBucketsForCapacity size' ≤ buckets.val.size then
+        ({ size := size', buckets := buckets' }, none)
+      else
+        (expand size' buckets', none)
+
+
 def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
   match m with
   | ⟨ size, buckets ⟩ =>
@@ -125,9 +141,10 @@ def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α
     else m
 
 inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β → Prop where
-  | mkWff     : ∀ n,                    WellFormed (mkHashMapImp n)
-  | insertWff : ∀ m a b, WellFormed m → WellFormed (insert m a b |>.1)
-  | eraseWff  : ∀ m a,   WellFormed m → WellFormed (erase m a)
+  | mkWff          : ∀ n,                    WellFormed (mkHashMapImp n)
+  | insertWff      : ∀ m a b, WellFormed m → WellFormed (insert m a b |>.1)
+  | insertIfNewWff : ∀ m a b, WellFormed m → WellFormed (insertIfNew m a b |>.1)
+  | eraseWff       : ∀ m a,   WellFormed m → WellFormed (erase m a)
 
 end HashMapImp
 
@@ -156,13 +173,22 @@ def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β :=
     match h:m.insert a b with
     | (m', _) => ⟨ m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption ⟩
 
-/-- Similar to `insert`, but also returns a Boolean flad indicating whether an existing entry has been replaced with `a -> b`. -/
+/-- Similar to `insert`, but also returns a Boolean flag indicating whether an existing entry has been replaced with `a -> b`. -/
 def insert' (m : HashMap α β) (a : α) (b : β) : HashMap α β × Bool :=
   match m with
   | ⟨ m, hw ⟩ =>
     match h:m.insert a b with
     | (m', replaced) => (⟨ m', by have aux := WellFormed.insertWff m a b hw; rw [h] at aux; assumption ⟩, replaced)
 
+/--
+Similar to `insert`, but returns `some old` if the map already had an entry `α → old`.
+If the result is `some old`, the the resulting map is equal to `m`. -/
+def insertIfNew (m : HashMap α β) (a : α) (b : β) : HashMap α β × Option β :=
+  match m with
+  | ⟨ m, hw ⟩ =>
+    match h:m.insertIfNew a b with
+    | (m', old) => (⟨ m', by have aux := WellFormed.insertIfNewWff m a b hw; rw [h] at aux; assumption ⟩, old)
+
 @[inline] def erase (m : HashMap α β) (a : α) : HashMap α β :=
   match m with
   | ⟨ m, hw ⟩ => ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 8c5f6dd6ad23..7d4062ad6288 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -770,6 +770,33 @@ partial def importModulesCore (imports : Array Import) : ImportStateM Unit := do
       moduleNames := s.moduleNames.push i.module
     }
 
+/--
+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.
+
+Motivation: We want to generate equational theorems on demand and potentially
+in different files, and we want them to have non-private names.
+We may add support for other kinds of definitions in the future. For now, theorems are
+sufficient for our purposes.
+
+We may have to revise this design decision and eagerly generate equational theorems when
+we implement the module system.
+
+Remark: we do not check whether the theorem `value` field match. This feature is useful and
+ensures the proofs for equational theorems do not need to be identical. This decision
+relies on the fact that theorem types are propositions, we have proof irrelevance,
+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
+
 /--
   Construct environment from `importModulesCore` results.
 
@@ -788,11 +815,13 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
   for h:modIdx in [0:s.moduleData.size] do
     let mod := s.moduleData[modIdx]'h.upper
     for cname in mod.constNames, cinfo in mod.constants do
-      match constantMap.insert' cname cinfo with
-      | (constantMap', replaced) =>
+      match constantMap.insertIfNew cname cinfo with
+      | (constantMap', cinfoPrev?) =>
         constantMap := constantMap'
-        if replaced then
-          throwAlreadyImported s const2ModIdx modIdx cname
+        if let some cinfoPrev := cinfoPrev? then
+          -- Recall that the map has not been modified when `cinfoPrev? = some _`.
+          unless equivInfo cinfoPrev cinfo do
+            throwAlreadyImported s const2ModIdx modIdx cname
       const2ModIdx := const2ModIdx.insert cname modIdx
     for cname in mod.extraConstNames do
       const2ModIdx := const2ModIdx.insert cname modIdx
diff --git a/tests/pkg/misc/Misc/Boo.lean b/tests/pkg/misc/Misc/Boo.lean
index 406fb8e0c2b8..7fc0c25fa391 100644
--- a/tests/pkg/misc/Misc/Boo.lean
+++ b/tests/pkg/misc/Misc/Boo.lean
@@ -1,3 +1,5 @@
 local infix:50 " ≺ " => LE.le
 
 #check 1 ≺ 2
+
+theorem simple : 10 = 10 := rfl
diff --git a/tests/pkg/misc/Misc/Foo.lean b/tests/pkg/misc/Misc/Foo.lean
index 918d229608ce..ffa0d91271c2 100644
--- a/tests/pkg/misc/Misc/Foo.lean
+++ b/tests/pkg/misc/Misc/Foo.lean
@@ -16,3 +16,5 @@ local macro "my_refl" : tactic =>
   `(tactic| rfl)
 
 def f (x y : Nat) (_h : x = y := by my_refl) := x
+
+theorem simple : 10 = 10 := by decide