postCongr! — Mathlib

Lean4
/-- A pass to clean up after `Lean.MVarId.preCongr!` and `Lean.MVarId.congrCore!`. -/
def postCongr! (config : Congr!.Config) (mvarId : MVarId) : MetaM (Option MVarId) := do
  let some mvarId ← mvarId.preCongr! config.closePost |
    return none
  let mvarId ← mvarId.propext
  if config.closePost then
      -- `preCongr` sees `p = q`, but now we've put it back into `p ↔ q` form.

    if ← mvarId.assumptionCore then
      return none
  if config.etaExpand then
    if let some (_, lhs, rhs) := (← withReducible mvarId.getType').eq? then
      let lhs' ← Meta.etaExpand lhs
      let rhs' ← Meta.etaExpand rhs
      return ← mvarId.change (← mkEq lhs' rhs')
  return mvarId
Похожие утверждения