Help with proof of membership

Stream: new members

[nrs]

I'm working on how to do simple proofs revolving around membership, but all my attempts finish in a mess similar to the following: (prove the first members of each pair are unique for a specific list)

def mylist := [("a", "b"), ("c", "d")]
theorem thm : ∀ x y, x ∈ mylist ∧ y ∈ mylist ∧ x ≠ y -> x.fst ≠ y.fst := by
    intro x y
    intro h
    obtain ⟨ha, hb, hc⟩ := h
    cases ha
    all_goals (cases hb; try trivial)
    all_goals (rename_i h; cases h; try trivial; rename_i h; try trivial)
    all_goals (rename_i h; try trivial)
    cases h <;> trivial

Would anyone have suggestions on how I could improve the readability/succinctness of the code? I am trying to eventually prove a theorem that should hold for any finite such list, which would allow me to determine for an arbitrary such list whether or not it has unique keys.

[Luigi Massacci]

import Mathlib.Tactic
def mylist := [("a", "b"), ("c", "d")]
theorem thm : ∀ x y, x ∈ mylist ∧ y ∈ mylist ∧ x ≠ y -> x.fst ≠ y.fst := by
    rw [mylist]; aesop

works, do you have any reason to avoid aesop? If your proof is a whole bunch of cases followed by trivial, letting aesop do that for you is a good idea

[nrs]

Luigi Massacci said:

import Mathlib.Tactic
def mylist := [("a", "b"), ("c", "d")]
theorem thm : ∀ x y, x ∈ mylist ∧ y ∈ mylist ∧ x ≠ y -> x.fst ≠ y.fst := by
    rw [mylist]; aesop

works, do you have any reason to avoid aesop? If your proof is a whole bunch of cases followed by trivial, letting aesop do that for you is a good idea

wow that's nice! I just haven't used aesop a lot, will be looking into it much more from now onwards, ty!