Documentation

Mathlib.Tactic.GCongr.CoreAttrs

gcongr attributes for lemmas up in the import chain #

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.

theorem imp_trans {a b c : Prop} (h : ab) :
(bc)ac
theorem imp_trans' {a b c : Prop} (h : bc) :
(ab)ac