return to top
source
In this file we add gcongr attribute to lemmas in Lean.Init. We may add lemmas from other files imported by Mathlib/Tactic/GCongr/Core later.
gcongr
Lean.Init
Mathlib/Tactic/GCongr/Core