Lean 4中析取交换律（Or.comm）定理位置咨询

在Lean 4里，Or.comm（析取交换律）并不在你查看的Core.lean文件中，它位于**Init.Logic**模块对应的源码文件里。

该定理的实现代码如下：

theorem Or.comm : a ∨ b ↔ b ∨ a := by
  constructor <;> intro h <;> cases h <;> exact Or.inr ‹_› <;> exact Or.inl ‹_›

Lean 4会将不同逻辑类型的定理拆分到不同模块管理，合取（And）相关的部分基础定理放在Core.lean，而析取（Or）的对应交换律等定理被归类到Init.Logic模块，你可以通过导入Init.Logic直接使用该定理，或者查看对应源码文件获取详细实现。

内容的提问来源于stack exchange，提问作者alagris