Setup for the gcongr tactic #
The core implementation of the gcongr ("generalized congruence") tactic is in the file
Tactic.GCongr.Core.
theorem
Mathlib.Tactic.GCongr.imp_mono
{a b c d : Prop}
(h₁ : c → a)
(h₂ : c → b → d)
:
(a → b) → c → d
A version of imp_imp_imp that has an extra hypothesis c in the b → d hypothesis.
We also use assumption to discharge side goals.
In a further downstream file, positivity will also be registered as a discharger.
From that point, positivity will be tried before assumption is: that is perfectly fine.
We register gcongr with the hint tactic.