compareSymm — Mathlib

Lean4
/-- Given ``k₁ := (R₁ lhs₁ rhs₁, `R₁)`` and ``k₂ := (R₂ lhs₂ rhs₂, `R₂)``, return `true` if
`R₁ lhs₁ rhs₁` is equivalent to `R₂ lhs₂ rhs₂` modulo the symmetry of `R₁` and `R₂`. -/
def compareSymm : (k₁ k₂ : Expr × Name) → CCM Bool
  | (e₁, n₁), (e₂, n₂) => do
    if n₁ != n₂ then
      return false
    if n₁ == ``Eq || n₁ == ``Iff then
      compareSymmAux e₁.appFn!.appArg! e₁.appArg! e₂.appFn!.appArg! e₂.appArg!
    else
      let some (_, lhs₁, rhs₁) ← e₁.relSidesIfSymm? |
        failure
      let some (_, lhs₂, rhs₂) ← e₂.relSidesIfSymm? |
        failure
      compareSymmAux lhs₁ rhs₁ lhs₂ rhs₂
Похожие утверждения