HepLean Documentation

Mathlib.Tactic.GCongr

Setup for the gcongr tactic #

The core implementation of the gcongr ("generalized congruence") tactic is in the file Tactic.GCongr.Core. In this file we set it up for use across the library by listing positivity as a first-pass discharger for side goals (gcongr_discharger).