Forcings predicted by core model theory $+$$ZFC$ results proved by the method of core model theory 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.
 A: The following paper is in the spirit of question 2.

Apter, Arthur W.; Gitman, Victoria; Hamkins, Joel David, Inner models with large cardinal features usually obtained by forcing, Arch. Math. Logic 51, No. 3-4, 257-283 (2012). DOI:10.1007/s00153-011-0264-5, ZBL1250.03104.
Abstract. We construct a variety of inner models exhibiting features usually obtained by forcing over universes with large cardinals. For example, if there is a supercompact cardinal, then there is an inner model with a Laver indestructible supercompact cardinal. If there is a supercompact cardinal, then there is an inner model with a supercompact cardinal $\kappa$ for which $2^\kappa=\kappa^+$, another for which $2^\kappa=\kappa^{++}$ and another in which the least strongly compact cardinal is supercompact. If there is a strongly compact cardinal, then there is an inner model with a strongly compact cardinal, for which the measurable cardinals are bounded below it and another inner model $W$ with a strongly compact cardinal $\kappa$, such that $H_{\kappa^+}^V\subseteq HOD^W$. Similar facts hold for supercompact, measurable and strongly Ramsey cardinals. If a cardinal is supercompact up to a weakly iterable cardinal, then there is an inner model of the Proper Forcing Axiom and another inner model with a supercompact cardinal in which GCH+V=HOD holds. Under the same hypothesis, there is an inner model with level by level equivalence between strong compactness and supercompactness, and indeed, another in which there is level by level inequivalence between strong compactness and supercompactness. If a cardinal is strongly compact up to a weakly iterable cardinal, then there is an inner model in which the least measurable cardinal is strongly compact. If there is a weakly iterable limit $\delta$ of ${\lt}\delta$-supercompact cardinals, then there is an inner model with a proper class of Laver-indestructible supercompact cardinals. We describe three general proof methods, which can be used to prove many similar results.

Our arguments, however, are not using any core model theory or fine-structural inner models, but rather just producing the desired inner models directly from the large cardinals themselves. And so this may not be the kind of example you seek.
A: Re question 1, how about Bukovsky-Namba forcing? (Wasn't it isolated after Jensen had shown the covering lemma?)
Re question 2, here is an (almost) ZFC example: Assume boldface $(\omega^2+1)-\Pi^1_1$ determinacy. Either lightface $\Pi^1_3$ uniformization is true, or else there is a real $x$ such that $\Sigma^1_3(x)$ uniformization is true. (Every proof of this I know uses Steel's correctness result for the core model below 1 Woodin cardinal.)
A: Question 1: A good example is Woodin's extender algebra. One reference describing the discovery of the extender algebra is the introduction to Neeman's book The Determinacy of Long Games. I am basically repeating Neeman's account. 
A soft consequence of ${\bf \Delta}^1_2$-determinacy is that the theory of $(\text{HOD}^{L[x]},\omega_2^{L[x]})$ is stable on a Turing cone. Woodin guessed that this has the following inner model theoretic explanation: $ \text{HOD}^{L[x]}$ is an iterated ultrapower (via an iteration tree) of the minimal canonical inner model $M_1$ with a Woodin cardinal, and $\omega^{L[x]}_2$ is the image of $M_1$'s Woodin cardinal. (EDIT: We add that a lot of interesting descriptive set theory, not all due to Woodin, went into this guess: for example, it was conjectured by Kechris-Martin-Solovay in Introduction to Q-Theory that the set $$Q_3 = \{x\in \omega^\omega : x\text{ is }\Delta^1_3\text{ in a countable ordinal}\}$$ is the set of reals in the ultimate inner model with a $\Delta^1_3$ wellorder of the reals, which at that time was believed to have large cardinals at the level of $I_3$ (!). The same paper includes a proof of the following theorem of Martin: assuming ${\bf \Delta}^1_2$-determinacy, for a Turing cone of $x$, $Q_3 = \omega^\omega \cap \text{HOD}^{L[x]}$. Then Woodin, in his work with Shelah, realized that the large cardinal level of this ultimate inner model should actually be exactly one Woodin cardinal, since any significantly stronger hypothesis implies there is no $\Delta^1_3$ wellorder of the reals.)
By Vopenka's theorem, for any real $x$, $x$ is generic over $\text{HOD}^{L[x]}$ for a partial order $\mathbb P \subseteq\omega^{L[x]}_2$. If the guess that on a cone of $x$, $\text{HOD}^{L[x]}$ is an iterate of $M_1$ is correct, then this predicts every real is generic over some iterate of $M_1$. But how could you iterate $M_1$ to make a real generic? Perhaps by imitating the process of comparison by least disagreement from inner model theory, instead constructing an iteration tree that inductively eliminates extenders that "disagree" with the real $x$ being generic. 
This motivated Woodin's definition of the extender algebra, which turns out to work in the coarse context as well: roughly, if $M$ is any iterable model with a Woodin cardinal $\delta$ (fine structural or not), there is a ${<}\delta$-cc partial order $\mathbb Q\subseteq V_\delta^M$, with $\mathbb Q\in M$ such that for any real $x$, there is an iteration tree on $M$ with branch embedding $i : M\to N$ such that $x$ is $N$-generic for $i(\mathbb Q)$.
(The fine-structural identity of $\text{HOD}^{L[x]}$ on a cone is still unknown, but the smaller model $\text{HOD}^{L[x][G]}$ where $G\subseteq \text{Col}(\omega,{<}\kappa)$ is $L[x]$-generic and $\kappa$ is the least inaccessible of $L[x]$ was analyzed by Woodin, building on work of Steel, and is a fine-structural one Woodin model, although it is not an iterate of $M_1$. See Steel-Woodin's paper HOD as a Core Model.)
Question 2: An example in cardinal arithmetic is the following theorem of Shelah, a sketch of which appears in James Cummings's EFI paper, Some Challenges for the Philosophy of Set Theory: if $\kappa$ is the $\omega_1$-th $\aleph$-fixed point then $\kappa^{\aleph_1}$ is less than the $(2^{2^{\aleph_1}})^+$th $\aleph$-fixed point. The proof is by dichotomy, conditioned on whether there is some $A\subseteq (2^{2^{\aleph_1}})^+$ such that there is no inner model $M$ such that $A\in M$ and $M$ has a Ramsey cardinal. If there is some such $A$, one uses covering over $K(A)$. If there is no such $A$, Shelah uses a determinacy result coming from the existence of inner models for Ramsey cardinals over all $A\subseteq (2^{2^{\aleph_1}})^+$.
There are many applications of core model theory at the level of Woodin cardinals in determinacy theory. One is Steel's theorem that PFA implies $\text{AD}^{L(\mathbb R)}$ (see his paper PFA implies $\text{AD}^{L(\mathbb R)}$). This is proved by the core model induction, another discovery of Woodin's. Another example is Sargsyan's result (see his thesis A Tale of Hybrid Mice) that if there is a Woodin limit of Woodin cardinals, then there is a pointclass $\Gamma\subseteq P(\mathbb R)$ such that $L(\mathbb R,\Gamma)$ satisfies $\text{AD}_\mathbb R + \Theta\text{ is regular}$. Before Sargsyan's work, this theory was conjectured to be extremely strong, at least at the level of a supercompact cardinal. There are also Steel's theorems that assuming AD and $V = L(\mathbb R)$, (1) every regular cardinal below $\Theta$ is measurable and (2) $\text{HOD}$ is a model of GCH. The proofs of both theorems involve analyzing HOD as a fine structure model; $\text{HOD}$ is closely related to (but distinct from) the minimal inner model $M_\omega$ with $\omega$ Woodin cardinals, for example, $V_\Theta^\text{HOD}$ is an iterate of $M_\omega|\delta$ where $\delta$ is the least Woodin of $M_\omega$. Again see HOD as a Core Model.
