Why does `simp` work differently for those two examples?

Stream: new members

[Bbbbbbbbba]

How could I make simp work better for the first example?

import Mathlib

-- Position -> ⟨Left options, Right options⟩
def LoopyGame (Position : Type) := Position → (Set Position) × (Set Position)

namespace LoopyGame

def intro_left {PosG PosH : Type} (game : LoopyGame PosG) : LoopyGame (PosG × PosH) :=
  fun (p, q) => ⟨{(p1, q) | p1 ∈ (game p).1}, {(p1, q) | p1 ∈ (game p).2}⟩

def intro_right {PosG PosH : Type} (game : LoopyGame PosH) : LoopyGame (PosG × PosH) :=
  fun (p, q) => ⟨{(p, q1) | q1 ∈ (game q).1}, {(p, q1) | q1 ∈ (game q).2}⟩

example {PosG} {PosH} (game : LoopyGame PosG) (p p1 : PosG) (q q1 : PosH) (h : (p1, q1) ∈ (game.intro_left (p, q)).1) : p1 ∈ (game p).1 ∧ q1 = q := by
  simp [intro_left] at h
  have ⟨p1_, hp1_⟩ := h
  rw [hp1_.2.1] at hp1_
  exact ⟨hp1_.1, Eq.symm hp1_.2.2⟩

example {PosG} {PosH} (game : LoopyGame PosH) (p p1 : PosG) (q q1 : PosH) (h : (p1, q1) ∈ (game.intro_right (p, q)).1) : q1 ∈ (game q).1 ∧ p1 = p := by
  simp [intro_right] at h
  exact ⟨h.1, Eq.symm h.2⟩

[Bbbbbbbbba]

Also in {(x, y) | ... }, when are x and/or y new variables and when are they existing variables in the context? In the following example Lean understands that both x and y are new variables, which is good in this case, but the same behavior would have been bad in my intro_left and intro_right above.

example (x y : ℕ) (hx : x = 1) (hy : y = 2) : (x, y) ∈ {(y, x) | x = 2 ∧ y = 1} := by
  simp
  exact ⟨hy, hx⟩