Add a helper lemma for Exercise 3.5.1

[gaearon]

It's easy to get lost in this proof because simplifying with existing mem_singleton and mem_pair will give you a weaker assertion than necessary. So I propose this lemma to nudge the reader towards the right path.

I also imported Set because it was confusing and annoying otherwise inside OrderedPair theorems.

Playthrough

/-- Helper lemma for Exercise 3.5.1 -/
lemma SetTheory.Set.pair_eq_singleton_iff {a b c: Object} : {a, b} = ({c}: Set) ↔
    a = c ∧ b = c := by
  constructor
  · intro h
    rw [ext_iff] at h
    have : ∀ x, x = c → x = b := by specialize h b; simp_all
    simp_all
  rintro (rfl | rfl)
  simp_all

/-- Exercise 3.5.1 -/
def OrderedPair.toObject : OrderedPair ↪ Object where
  toFun p := ({ (({p.fst}:Set):Object), (({p.fst, p.snd}:Set):Object) }:Set)
  inj' := by
    intro p1 p2 hp
    simp only [EmbeddingLike.apply_eq_iff_eq, ext_iff, mem_pair] at hp
    rw [OrderedPair.eq]
    have hfst_eq : p1.fst = p2.fst := by
      obtain (_ | hp2) := (hp ({p1.fst}: Set)).mp (Or.inl rfl)
      · simp_all [ext_iff]
      symm at hp2
      simp_all [pair_eq_singleton_iff] -- Used here
    use hfst_eq
    obtain hp1 := (hp ({p1.fst, p1.snd}: Set)).mp (Or.inr rfl)
    simp_all only [EmbeddingLike.apply_eq_iff_eq]
    by_cases h : p1.snd = p2.fst
    · simp_all [pair_eq_singleton_iff] -- And here
    have : {p2.fst, p1.snd} ≠ ({p2.fst}: Set) := by intro h; simp_all [pair_eq_singleton_iff] -- And here
    simp only [this, false_or] at hp1
    have := pair_eq_pair hp1
    simp_all

[gaearon]

Clarified comment because the second part is later on