# 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.

source
theorem Mathlib.Tactic.GCongr.imp_trans {a b c : Prop} (h : a → b) :
(b → c) → a → c
source
theorem Mathlib.Tactic.GCongr.imp_right_mono {a b c : Prop} (h : a → b → c) :
(a → b) → a → c
source
theorem Mathlib.Tactic.GCongr.and_right_mono {a b c : Prop} (h : a → b → c) :
a ∧ b → a ∧ c