I have two unrelated question.

First question. To motivate the question, let me explain an example. The natural way to force the failure of singular cardinals hypothesis ($SCH$), is to start with a large cardinal $\kappa$, and make it singular while blowing up its power. However, results of core model theory show that if $SCH$ fails at $\kappa,$ then either $\kappa$ is a large cardinal, or it is a singular limit of large cardinals. Motivated by this fact, the long and short extender forcings were developed, showing that the second case can be forced as well.

Now my question is the following:

Question 1. Are there any other example of forcing notions, whose existence is first predicted using core model techniques and then they are discovered?

Second question. Forcing is a powerful tool to prove $ZFC$ results as well, see for example Forcing as a tool to prove theorems, and Examples of ZFC theorems proved via forcing and Proving results about complete Boolean algebras in ZFC using Boolean valued models and Producing finite objects by forcing!.

Surprisingly, one can also use the technique of core model theory to prove $ZFC$ results. One example that I know, is the following result of Woodin: Suppose that $V=L[s]$, where $s$ is an $ω$-sequence of ordinals. Then $GCH$ (and in fact much more) holds. See The universe constructed from a sequence of ordinals.

Question 2. Are there any other example of $ZFC$ results whose prove uses techniques of core model theory. The same question for theories like $ZFC+\phi$, where $\phi$ is the assertion that some large cardinal(s) exist, for which we know a core model exists (so that we can apply the core model techniques).

Remark. I am not interested in results which use some kind of covering in the absence of large cardinals to get some results, like, if there is no measurable cardinal (or even larger cardinals), then square holds at singular cardinals or so on.

I have two unrelated question.

First question. To motivate the question, let me explain an example. The natural way to force the failure of singular cardinals hypothesis ($SCH$), is to start with a large cardinal $\kappa$, and make it singular while blowing up its power. However, results of core model theory show that if $SCH$ fails at $\kappa,$ then either $\kappa$ is a large cardinal, or it is a singular limit of large cardinals. Motivated by this fact, the long and short extender forcings were developed, showing that the second case can be forced as well.

Now my question is the following:

Question 1. Are there any other example of forcing notions, whose existence is first predicted using core model techniques and then they are discovered?

Second question. Forcing is a powerful tool to prove $ZFC$ results as well, see for example Forcing as a tool to prove theorems, and Examples of ZFC theorems proved via forcing and Proving results about complete Boolean algebras in ZFC using Boolean valued models and Producing finite objects by forcing!.

Surprisingly, one can also use the technique of core model theory to prove $ZFC$ results. One example that I know, is the following result of Woodin: Suppose that $V=L[s]$, where $s$ is an $ω$-sequence of ordinals. Then $GCH$ (and in fact much more) holds. See The universe constructed from a sequence of ordinals.

Question 2. Are there any other examples of $ZFC$ results whose proof uses techniques of core model theory. The same question for theories like $ZFC+\phi$, where $\phi$ is the assertion that some large cardinal(s) exist, for which we know a core model exists (so that we can apply the core model techniques).

Remark. I am not interested in results which use some kind of covering in the absence of large cardinals to get some results, like, if there is no measurable cardinal (or even larger cardinals), then square holds at singular cardinals or so on.