Is generalize_proofs an antipattern?

Stream: new members

[Dan Abramov]

I often have to resort to generalize_proofs to pull out some proofs from the otherwise-inscrutable goal in situations like this:

Screenshot 2025-09-05 at 23.22.15.png

And then hopefully it gives me something I can turn into a proof:

Screenshot 2025-09-05 at 23.23.03.png

I was wondering whether this technique is common or considered an anti-pattern. I suspect I'm missing some explicit APIs that would remove a need for this. In particular, it feels fragile to depend on the order of proofs being extracted — it's usually like a grabbag of stuff.

Is my intuition about this right? Should I be grossed out by doing it?

[Ruben Van de Velde]

No, it's fine, as far as I understand it. But you probably don't want to spend too long with Exists.choose terms in your state; hopefully you'll wrap those in a definition and won't need to see them again when you've set up basic api

[Kevin Buzzard]

Why are you doing have := h1.choose_spec rather than obtain ⟨f, this⟩ := hf? Your goal is a Prop (as it should be, in tactic mode) so you don't need AC here.

[Aaron Liu]

probably the choosing was done in some other definition which was then unfolded

[Dan Abramov]

Yeah, this is spilled guts from an abbrev.

noncomputable abbrev SetTheory.Set.pow_fun_equiv {A B : Set} : ↑(A ^ B) ≃ (B → A) where
  toFun F := ((powerset_axiom _).mp F.property).choose
  invFun f := ⟨f, (powerset_axiom _).mpr ⟨f, by simp⟩⟩
  left_inv F := by ext; exact ((powerset_axiom _).mp F.property).choose_spec
  right_inv f := by simp

I've since tweaked the approach to make this a def with a lemma:

noncomputable def SetTheory.Set.pow_fun_equiv {A B : Set} : ↑(A ^ B) ≃ (B → A) where
  toFun F := ((powerset_axiom _).mp F.property).choose
  invFun f := ⟨f, (powerset_axiom _).mpr ⟨f, by simp⟩⟩
  left_inv F := by ext; exact ((powerset_axiom _).mp F.property).choose_spec
  right_inv f := by simp

lemma SetTheory.Set.pow_fun_eq_iff {A B : Set} (x y : ↑(A ^ B)) : x = y ↔ pow_fun_equiv x = pow_fun_equiv y := by
  rw [←pow_fun_equiv.apply_eq_iff_eq]

So now it no longer "spills out" the choice-y guts, and this part of the proof just closes by simp.

[Dan Abramov]

And to answer the question directly, obtain wouldn't help close the goal here because the statements I'd get out of two of those would "talk about" different functions than the ones in my goal's expression. The goal is to bridge them together.

Screenshot 2025-09-06 at 15.37.24.png

Using a def instead of abbrev avoids this problem altogether though because choice stays behind an opaque pow_fun_equiv call.

So this entire section goes away.