Lean4
/-- Convert a goal into an `Eq` goal if possible (since we have a better shot at those).
Also, if `tryClose := true`, then try to close the goal using an assumption, `Subsingleton.Elim`,
or definitional equality. -/
def preCongr! (mvarId : MVarId) (tryClose : Bool) : MetaM (Option MVarId) := do
-- Next, turn `HEq` and `Iff` into `Eq`
let mvarId ← mvarId.heqOfEq
if tryClose then
-- This is a good time to check whether we have a relevant hypothesis.
if ← mvarId.assumptionCore then
return none
let mvarId ← mvarId.iffOfEq
if tryClose then
-- Now try definitional equality. No need to try `mvarId.hrefl` since we already did `heqOfEq`.
-- We allow synthetic opaque metavariables to be assigned to fill in `x = _` goals that might
-- appear (for example, due to using `convert` with placeholders).
try
withAssignableSyntheticOpaque mvarId.refl;
return none
catch _ =>
pure
()
-- Now we go for (heterogeneous) equality via subsingleton considerations
if ← Lean.Meta.fastSubsingletonElim mvarId then
return none
if ← mvarId.proofIrrelHeq then
return none
return some mvarId
