Bootstrapping results that really bootstrap There is a type of results in TCS usually called bootstrapping results. In general, it is of the form


  If proposition $A$ holds, then proposition $A'$ holds.


where $A$ and $A'$ are propositions that look similar, and $A$ is seemingly "weaker" then $A'$, which is the reason we name this type of results.
Let me give a few concrete examples:


  Theorem. [Chen and Tell, STOC'19] Fix any problem $\Pi \in \{\mathsf{BFE,W_{S_5},W5STCONN}\}$
  . Assume that for every $c&gt;1$ there exist infinitely many $d\in \mathbb{N}$ such that $\mathcal{TC}^0$ circuits of depth $d$ need more than $n^{1+c^{-d}}$ wires to solve the problem $\Pi$. Then for any $d_0,k \in \mathbb{N}$, $\Pi$ cannot be solved by $\mathcal{TC}^0$ circuits of depth $d_0$ and $n^k$ wires, and therefore $\mathcal{TC}^0 \subsetneq \mathcal{NC}^1$.
  
  Theorem. [Gupta et al., FOCS'13] Suppose that computing the permanent requires depth-$3$ arithmetic circuits of size more than $n^{\Omega(\sqrt{n})}$, over fields of characteristic $0$. Then computing the permanent requires arithmetic circuits of superpolynomial size, and therefore Valiant's Conjecture holds.


Well, a more famous but not-so-appropriate example comes from fine-grained complexity:


  Theorem. [Backurs and Indyk, STOC'15] If we can compute EDIT DISTANCE in $O(n^{2-\epsilon})$ time (on the RAM model), then we will get a SAT solver faster than any one that currently exists.


Update. (July 10, 2019) The edit distance example may be a little confusing. Refer to Ryan’s answer for a “standard” example.

As you may have imagined, (to my  best knowledge) all results of this type are proved by taking the contrapositive (I have taken the contrapositive in the edit distance one). So in some sense these are all algorithmic results.

Usually there are two ways to understand a bootstrapping result. 1. We only need to prove $A$ and then apply the result, if we want to prove $A'$; 2. Proving $A$ may be difficult because a priori we think proving $A'$ difficult.

The problem is that, one (or more exactly, I) may be hardly optimistic and take the first understanding, if there does not exist any positive use of bootstrap results after all!
So my question is


  Do we know any bootstrapping result in which $A$ is proven?
A classic result provable by bootstrapping (and applicable to proving real lower bounds) is that in any computational model where we have $TIME(n) \neq TIME(n^c)$ for some constant $c &gt; 1$, we in fact have  $TIME(n) \neq TIME(n^{1+\epsilon})$, for every $\epsilon &gt; 0$.

The idea is that if $TIME(n) = TIME(n^{1+\epsilon})$, we can apply a  padding argument repeatedly to obtain $TIME(n) = TIME(n^c)$ for every constant $c$. You can even use such an argument to slightly improve known time hierarchy theorems in various cases.