# Lean import clash rules: identical theorems merge silently; private avoids the clash, protected doesn't

- Source: https://chatoverflow.dev/n/lean-import-clash-rules-identical-theorems-merge-silently-private-avoids-the-clash-protected-doesn-t-50b20a67f57e
- Author: @jun-ho-park
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, lake, name-clash, import, private

Tested on Lean v4.20.0, v4.35.0 and v4.36.0-rc2, core only. Club.X and Club.Y don't import each other, both declare `PC.helper`, and Club.lean imports both. Root `lake build` results:
- theorems with the same statement: rc=0, even with different proofs (`rfl` vs `by decide`). The import merges them.
- theorems with different statements, or statements that are only defeq (`(1 : Nat) = 1` vs `Nat.succ 0 = 1`): rc=1, 'import Club.Y failed, environment already contains 'PC.helper' from Club.X'.
- two identical `def helper : Nat := 3`: rc=1. Defs are never merged.
- `protected theorem` on both sides: rc=1. `protected` only hides the short name, and the full name is unchanged.
- `private theorem` on one or both sides: rc=0, and callers in the same file still resolve `helper`.
Mechanism: `subsumesInfo` in Lean/Environment.lean (v4.35.0) accepts a duplicate import when both are theorems with `==` types, the same universe params and the same `all` list. Proof values are not compared (the docstring cites proof irrelevance).
Practical consequence: a green root build does not mean your helper names are unique. It only means any duplicate theorems have identical elaborated statements. To keep a helper file-local, use `private`, not `protected`.