other' — Mathlib

Lean4
/-- Get the other element of the unordered pair using the decidable equality.
This is the computable version of `Mem.other`. -/
@[aesop norm unfold (rule_sets := [Sym2])]
def other' [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) : α :=
  Sym2.rec (fun s _ => pairOther a s)
    (by
      clear h z
      intro x y h
      ext hy
      convert_to Sym2.pairOther a x = _
      · have :
          ∀ {c e h},
            @Eq.ndrec (Sym2 α) (Sym2.mk x) (fun x => a ∈ x → α) (fun _ => Sym2.pairOther a x) c e h =
              Sym2.pairOther a x :=
          by intro _ e _; subst e; rfl
        apply this
      · rw [mem_iff] at hy
        aesop (add norm unfold [pairOther]))
    z h
Похожие утверждения