HepLean Documentation

Mathlib.Tactic.Attr.Core

Simp tags for core lemmas #

In Lean 4, an attribute declared with register_simp_attr cannot be used in the same file. So, we declare all simp attributes used in Mathlib in Mathlib/Tactic/Attr/Register and tag lemmas from the core library and the Batteries library with these attributes in this file.