def Lean.MVarId.congrN (mvarId : Lean.MVarId) (depth : optParam Nat 1000000) (closePre : optParam Bool true) (closePost : optParam Bool true) :
Given a goal of the form
⊢ f as = f bs,
⊢ (p → q) = (p' → q'), or
⊢ HEq (f as) (f bs), try to apply congruence.
It takes proof irrelevance into account, and the fact that
Decidable p is a subsingleton.
congrrecursively up to depth
closePre := true, it will attempt to close new goals using
assumptionwith reducible transparency.
closePost := true, it will try again on goals on which
congrfailed to make progress with default transparency.