Commit 2023-07-26 08:17 9f14c412

chore(*): add protected to *.insert theorems (#6142) Otherwise code like

theorem ContMDiffWithinAt.mythm (h : x ∈ insert y s) : _ = _

interprets insert as ContMDiffWithinAt.insert, not Insert.insert.