-- Mathlib/SetTheory/ZFC/Basic.lean
theorem pair_injective : Function.Injective2 pair

Proof state:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ x = x ∧ y = y'

Tactic:
have he : y = x → y = y' := by
  rintro rfl
  simpa [eq_comm] using H {y, y'}

Result:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
⊢ x = x ∧ y = y'

Proof state:
x x' y y' : ZFSet.{u_1}
H : x.pair y = x'.pair y'
⊢ x = x' ∧ y = y'

Tactic:
simp_rw [ZFSet.ext_iff, pair, mem_pair] at H

Result:
x x' y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x' ∧ y = y'

Proof state:
x x' y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x' ∧ y = y'

Tactic:
obtain rfl : x = x' := And.left <| by simpa [or_and_left] using (H {x}).1 (Or.inl rfl)

Result:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ x = x ∧ y = y'

Proof state:
⊢ Function.Injective2 pair

Tactic:
intro x x' y y' H

Result:
x x' y y' : ZFSet.{u_1}
H : x.pair y = x'.pair y'
⊢ x = x' ∧ y = y'

Proof state:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'

Tactic:
refine ⟨rfl, hx.elim he fun hy ↦ Or.elim ?_ he id⟩

Result:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ {x, y} = {x, y'}
hy : {x, y} = {x, y'}
⊢ y = x ∨ y = y'

Proof state:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : {x, y} = {x} ∨ {x, y} = {x, y} ↔ {x, y} = {x} ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'

Tactic:
simp_rw [pair_eq_singleton_iff, true_and, or_true, true_iff] at hx

Result:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'

Proof state:
y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
⊢ y = y'

Tactic:
simpa [eq_comm] using H {y, y'}

Result:
no goals

Proof state:
x x' y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x' ∧ ?m.90349

Tactic:
simpa [or_and_left] using (H {x}).1 (Or.inl rfl)

Result:
no goals

Proof state:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ y = x → y = y'

Tactic:
rintro rfl

Result:
y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
⊢ y = y'

Proof state:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ {x, y} = {x, y'}
hy : {x, y} = {x, y'}
⊢ y = x ∨ y = y'

Tactic:
simpa using ZFSet.ext_iff.1 hy y

Result:
no goals

Proof state:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
⊢ x = x ∧ y = y'

Tactic:
have hx := H {x, y}

Result:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : {x, y} = {x} ∨ {x, y} = {x, y} ↔ {x, y} = {x} ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'