Lean4
/-- Tries to make a congruence between `lhs` and `rhs` automatically.
1. If they are defeq, returns a trivial congruence.
2. Tries using `Subsingleton.elim`.
3. Tries `proof_irrel_heq` as another effort to avoid doing congruence on proofs.
3. Otherwise throws an error.
Note: `mkAppM` uses `withNewMCtxDepth`, which prevents typeclass inference
from accidentally specializing `Sort _` to `Prop`, which could otherwise happen
because there is a `Subsingleton Prop` instance. -/
def mkDefault (lhs rhs : Expr) : MetaM CongrResult := do
if ← isDefEq lhs rhs then
return { lhs, rhs, pf? := none }
else if let some pf← (observing? <| mkAppM ``Subsingleton.elim #[lhs, rhs]) then
return CongrResult.mk' lhs rhs pf
else if let some pf← (observing? <| mkAppM ``proof_irrel_heq #[lhs, rhs]) then
return CongrResult.mk' lhs rhs pf
throwError "Could not generate congruence between{(indentD lhs)}\nand{indentD rhs}"
