-- Mathlib/SetTheory/ZFC/Basic.lean
private lemma toSet_equiv_aux {s : Set ZFSet.{u}} (hs : Small.{u} s) :
  (mk <| PSet.mk (Shrink s) fun x ↦ ((equivShrink s).symm x).1.out).toSet = s

Proof state:
case h.refine_1
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ (Quotient.out x ∈ PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)) → x ∈ s

Tactic:
rintro ⟨b, h2⟩

Result:
case h.refine_1.intro
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
b : (PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)).Type
h2 : (Quotient.out x).Equiv ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)).Func b)
⊢ x ∈ s

Proof state:
case h
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ (Quotient.out x ∈ PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)) ↔ x ∈ s

Tactic:
refine ⟨?_, fun xs ↦ ⟨equivShrink s (Subtype.mk x xs), ?_⟩⟩

Result:
case h.refine_1
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ (Quotient.out x ∈ PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)) → x ∈ s

case h.refine_2
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
xs : x ∈ s
⊢ (Quotient.out x).Equiv
    ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)).Func ((equivShrink ↑s) ⟨x, xs⟩))

Proof state:
case h.refine_1.intro
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
b : (PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)).Type
h2 : x = mk ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)).Func b)
⊢ x ∈ s

Tactic:
simp [h2]

Result:
no goals

Proof state:
case h.refine_2
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
xs : x ∈ s
⊢ (Quotient.out x).Equiv
    ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)).Func ((equivShrink ↑s) ⟨x, xs⟩))

Tactic:
simp [PSet.Equiv.refl]

Result:
no goals

Proof state:
case h
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ x ∈ (mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x))).toSet ↔ x ∈ s

Tactic:
rw [mem_toSet, ← mk_out x, mk_mem_iff, mk_out]

Result:
case h
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ (Quotient.out x ∈ PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)) ↔ x ∈ s

Proof state:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
⊢ (mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x))).toSet = s

Tactic:
ext x

Result:
case h
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
⊢ x ∈ (mk (PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x))).toSet ↔ x ∈ s

Proof state:
case h.refine_1.intro
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
b : (PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)).Type
h2 : (Quotient.out x).Equiv ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)).Func b)
⊢ x ∈ s

Tactic:
rw [← ZFSet.eq, ZFSet.mk_out] at h2

Result:
case h.refine_1.intro
s : Set ZFSet.{u}
hs : Small.{u, u + 1} ↑s
x : ZFSet.{u}
b : (PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)).Type
h2 : x = mk ((PSet.mk (Shrink.{u, u + 1} ↑s) fun x => Quotient.out ↑((equivShrink ↑s).symm x)).Func b)
⊢ x ∈ s