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

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.