mathlib

87fc6828 - feat(data/set/finite): set.finite.induction_on' (#15444)

feat(data/set/finite): set.finite.induction_on' (#15444) This is analogous to `finset.induction_on'`. Discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/induction.20on.20finite.20set