Try to apply a simp congruence theorem.
Instances For
Try to apply implies_congr.
Instances For
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.
- Applies
congrrecursively up to depthdepth. - If
closePre := true, it will attempt to close new goals usingEq.refl,HEq.refl, andassumptionwith reducible transparency. - If
closePost := true, it will try again on goals on whichcongrfailed to make progress with default transparency.
Instances For
Instances For
def
Lean.MVarId.congrN.go
(closePre : optParam Bool true)
(closePost : optParam Bool true)
(n : Nat)
(mvarId : Lean.MVarId)
:
Equations
- One or more equations did not get rendered due to their size.