Add helper lemma for 3.4.7

[gaearon]

I found 3.4.7 very difficult. It seems like I'm not alone in this.

In particular, it was difficult to think about the dance between Object, Set, existentials, and membership in .powerset. This lemma collapses some of that. See inline comments below for where it shows up.

I think it can also serve as a hint for how to move between the layers.

Playthrough

theorem SetTheory.Set.partial_functions {X Y:Set} :
    ∃ Z:Set, ∀ F:Object, F ∈ Z ↔ ∃ X' Y':Set, X' ⊆ X ∧ Y' ⊆ Y ∧ ∃ f: X' → Y', F = f := by
  use union (Y.powerset.replace (P := fun oY' outer ↦
    outer = union (X.powerset.replace (P := fun oX' inner ↦
      ∃ (X' Y' : Set), oX'.val = X' ∧ oY'.val = Y' ∧ inner = (Y' ^ X': Set)
    ) (by simp_all))
  ) (by simp_all))

  intro F
  constructor
  · intro hF
    rw [union_axiom] at hF
    obtain ⟨S, hFS, hS⟩ := hF
    rw [replacement_axiom] at hS
    obtain ⟨⟨oY', hoY'⟩, hS⟩ := hS
    rw [EmbeddingLike.apply_eq_iff_eq] at hS
    subst hS
    rw [union_axiom] at hFS
    obtain ⟨S, hFS, hS⟩ := hFS
    rw [replacement_axiom] at hS
    obtain ⟨⟨oX', hoX'⟩, X', Y', rfl, rfl, hS⟩ := hS
    rw [EmbeddingLike.apply_eq_iff_eq] at hS
    rw [hS, powerset_axiom] at hFS
    obtain ⟨f, hf⟩ := hFS
    use X', Y'
    simp_all only [mem_powerset'] -- Helps here
    tauto

  · rintro ⟨X', Y', hX', hY', f, rfl⟩
    rw [mem_iUnion]
    use ⟨Y', by simp_all⟩  -- Helps here
    rw [union_axiom]
    use (Y' ^ X')
    constructor
    · rw [powerset_axiom]
      use f
    · rw [replacement_axiom]
      use ⟨X', by simp_all⟩  -- Helps here
      use X', Y'

Maybe there are simpler ways, but I haven't found them!