Commit 2022-03-03 19:28 cdb69d5c

fix(data/set/function): do not use reducible (#12377) Reducible should only be used if the definition if it occurs as an explicit argument in a type class and must reduce during type class search, or if it is a type that should inherit instances. Propositions should only be reducible if they are trivial variants (< and > for example). These reducible attributes here will cause issues in Lean 4. In Lean 4, the simplifier unfold reducible definitions in simp lemmas. This means that tagging an inj_on-theorem with @[simp] creates the simp lemma ?a = ?b (i.e. match anything).