Commit 2021-09-15 18:42 a4341f91

refactor(data/set/finite): use a custom inductive type (#9164) Currently Lean treats local assumptions h : finite s as local instances, so one needs to do something like

  unfreezingI { lift s to finset α using hs },

I change the definition of set.finite to an inductive predicate that replicates the definition of nonempty and remove unfreezingI here and there. Equivalence to the old definition is given by set.finite_def.