I see
theorem And.comm : a ∧ b ↔ b ∧ a := by
constructor <;> intro ⟨h₁, h₂⟩ <;> exact ⟨h₂, h₁⟩
in Core.lean but there is no Or.comm to be seen. Where can I find it?
The website mathlib4 docs (https://leanprover-community.github.io/mathlib4_docs/) is currently one of the better ways to answer this sort of question, even if you aren't using mathlib4 and only want core Lean.
In this case there is a declaration Or.comm in the Lean 4 standard library (std), see https://leanprover-community.github.io/mathlib4_docs/Std/Logic.html#Or.comm, which probably means it isn't in core. Using Std should be a relatively lightweight addition to your project, and should contain many of these small useful things that aren't in core but possibly could be.