Ch 3.5 OrderedPair eval APIs

Stream: Analysis I

[Rado Kirov]

Sharing here because I lost a lot of time trying to figure this out. While working on the examples for Cartesian product and OrderedPair, I added this API theorem for fst and snd

theorem SetTheory.Set.fst_eval {X Y: Set} (x: X) (y: Y) :
    fst ⟨OrderedPair.toObject { fst := x, snd := y }, by rw [mem_cartesian]; use x; use y⟩ = x := by sorry

to my surprise it kept failing to make progress on terms like:

↑(fst
      ⟨OrderedPair.toObject
          { fst := ↑(fst (fst t)), snd := OrderedPair.toObject { fst := ↑(snd (fst t)), snd := ↑(snd t) } },
        ⋯⟩

Eventually, I realized the issue is that Lean cannot match y: Y with y = OrderedPair.toObject ... because it needs to find a proof that y is in some subset Y ×ˢ Z. So my very unsatisfying work around is to add 4 more theorems like:

theorem SetTheory.Set.fst_eval_fst_op {X Y: Set} (p: OrderedPair) (h: p.toObject ∈ X) (y: Y) :
  fst ⟨OrderedPair.toObject { fst := p.toObject, snd := y }, by rw [mem_cartesian]; use ⟨ p.toObject, h⟩; use y⟩ = ⟨p.toObject, h⟩ := sorry

but I wonder if there is a better way.

[Rado Kirov]

https://github.com/rkirov/analysis/blob/main/analysis/Analysis/Section_3_5.lean#L192-L242