Commit 2026-08-25 15:52 ab64d1cd

View on Github →

chore: don't inductively define sets (#42171) Instead define them as Set.ofPred of inductively-defined predicates. This avoids abusing the defeq Set α := α → Prop. In cases where the set was barely used, I have inlined the definition instead. Generated by Claude Opus, then reviewed and cherry-picked line-by-line by myself. Assisted-by: Claude Opus 4.8

Estimated changes

deleted theorem Hindman.FP.cons
deleted theorem Hindman.FP.head
modified theorem Hindman.FP.mul
modified theorem Hindman.FP.singleton
deleted theorem Hindman.FP.tail
modified inductive Hindman.FP
modified theorem Hindman.FP_drop_subset_FP
modified inductive Hindman.FS
modified theorem NFA.toεNFA_εClosure
modified theorem εNFA.subset_εClosure
added theorem εNFA.εClosure.base
added theorem εNFA.εClosure.step
added def εNFA.εClosure
deleted inductive εNFA.εClosure
added theorem εNFA.εClosure_min
added def generatePiSystem
deleted inductive generatePiSystem
added theorem generatePiSystem_min