mathlib documentation

core.init.meta.congr_tactic

source
meta def tactic.apply_congr_core (clemma : congr_lemma) :
tactic unit

source
meta def tactic.apply_eq_congr_core (tgt : expr) :
tactic unit

source
meta def tactic.apply_heq_congr_core  :
tactic unit

source
meta def tactic.congr_core  :
tactic unit

source
meta def tactic.congr  :
tactic unit