x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z ∈ pair x y ↔ z ∈ pair x' y'
⊢ x = x' ∧ y = y'
x x' y y' : ZFSet
H : pair x y = pair x' y'
⊢ x = x' ∧ y = y'
have ae := ext_iff.1 H
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x' ∧ y = y'
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z ∈ pair x y ↔ z ∈ pair x' y'
⊢ x = x' ∧ y = y'
simp only [pair, mem_pair] at ae
case inl
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyx : {x, y} = {x}
⊢ x = x ∧ y = y'

case inr
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
⊢ x = x ∧ y = y'
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
⊢ x = x ∧ y = y'
obtain xyx | xyy' := (ae {x, y}).1 (by simp)
case inl
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x'}
⊢ x = x'

case inr
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
⊢ x = x'
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x'
cases' (ae {x}).1 (by simp) with h h
no goals
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ {x} = {x} ∨ {x} = {x, y}
simp
no goals
case inl
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x'}
⊢ x = x'
exact singleton_injective h
case inr
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
m : x' ∈ {x}
⊢ x = x'
case inr
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
⊢ x = x'
have m : x' ∈ ({x} : ZFSet) := by simp [h]
no goals
case inr
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
m : x' ∈ {x}
⊢ x = x'
rw [mem_singleton.mp m]
no goals
x x' y y' : ZFSet
H : pair x y = pair x' y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
h : {x} = {x', y'}
⊢ x' ∈ {x}
simp [h]
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
⊢ x = y'
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ x = y → y = y'
rintro rfl
case inl
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'x : {x, y'} = {x}
⊢ x = y'

case inr
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'xx : {x, y'} = {x, x}
⊢ x = y'
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
⊢ x = y'
cases' (ae {x, y'}).2 (by simp only [eq_self_iff_true, or_true_iff]) with xy'x xy'xx
no goals
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
⊢ {x, y'} = {x} ∨ {x, y'} = {x, y'}
simp only [eq_self_iff_true, or_true_iff]
case inl
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'x : {x, y'} = {x}
⊢ y' = x ∨ y' = y'
case inl
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'x : {x, y'} = {x}
⊢ x = y'
rw [eq_comm, ← mem_singleton, ← xy'x, mem_pair]
no goals
case inl
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'x : {x, y'} = {x}
⊢ y' = x ∨ y' = y'
exact Or.inr rfl
no goals
case inr
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'xx : {x, y'} = {x, x}
⊢ x = y'
simpa [eq_comm] using (ext_iff.1 xy'xx y').1 (by simp)
no goals
x y' : ZFSet
H : pair x x = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, x} ↔ z = {x} ∨ z = {x, y'}
xy'xx : {x, y'} = {x, x}
⊢ y' ∈ {x, y'}
simp
no goals
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
⊢ {x, y} = {x} ∨ {x, y} = {x, y}
simp
case inl
y y' : ZFSet
H : pair y y = pair y y'
ae : ∀ (z : ZFSet), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
he : y = y → y = y'
xyx : {y, y} = {y}
⊢ y = y ∧ y = y'
case inl
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyx : {x, y} = {x}
⊢ x = x ∧ y = y'
obtain rfl := mem_singleton.mp ((ext_iff.1 xyx y).1 <| by simp)
no goals
case inl
y y' : ZFSet
H : pair y y = pair y y'
ae : ∀ (z : ZFSet), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
he : y = y → y = y'
xyx : {y, y} = {y}
⊢ y = y ∧ y = y'
simp [he rfl]
no goals
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyx : {x, y} = {x}
⊢ y ∈ {x, y}
simp
case inr.inl
y y' : ZFSet
H : pair y y = pair y y'
ae : ∀ (z : ZFSet), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
he : y = y → y = y'
xyy' : {y, y} = {y, y'}
⊢ y = y ∧ y = y'

case inr.inr
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
yy' : y = y'
⊢ x = x ∧ y = y'
case inr
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
⊢ x = x ∧ y = y'
obtain rfl | yy' := mem_pair.mp ((ext_iff.1 xyy' y).1 <| by simp)
no goals
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
⊢ y ∈ {x, y}
simp
no goals
case inr.inl
y y' : ZFSet
H : pair y y = pair y y'
ae : ∀ (z : ZFSet), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
he : y = y → y = y'
xyy' : {y, y} = {y, y'}
⊢ y = y ∧ y = y'
simp [he rfl]
no goals
case inr.inr
x y y' : ZFSet
H : pair x y = pair x y'
ae : ∀ (z : ZFSet), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : x = y → y = y'
xyy' : {x, y} = {x, y'}
yy' : y = y'
⊢ x = x ∧ y = y'
simp [yy']