It seems that there is a marked discrepancy between how one might explain a concept in mathematics, and how one might prove it. Obviously, there are some exceptions, and some particularly elegant proofs merely formalise what we intuitively know. However, more often than not, formal rigour seems to be at the cost of understanding something in a more 'human' way.
To illustrate, here is an elementary example:
Prove $\log_c c^x=x$
Here, my attempt at a formal proof would be:
\begin{align} \log_c c^x &= x\log_c c \text{ (Using the power law)} \\ \log_c c&=1 \text{ as $c^1=c$ by definition} \\ \implies x\log_cc&=x(1)=x \end{align}
I wonder if this proof might be seen as verbose, or overly formal. Would the following also be accepted as a proof?
\begin{align} \log_c c^x &= x\log_c c=x \end{align}
On the other hand, perhaps a mathematician might say that neither of these proofs are formal enough, and that to properly prove $\log_cc^x=x$, one must lay out all of the axioms/definitions that they are using, and build the proof from the ground up.
And finally, here is the way I intuitively understand $\log_c c^x$:
$\log_ca$ means 'to what power must $c$ be raised in order to get $a$?'. Therefore, in the case of $\log_cc^x$, the question becomes 'what power must I raise $c$ to in order to get $c^x$?'. Therefore, the question is easy to answer. It's like writing $c^?=c^x$, where the answer to the question is very obviously $x$.
Unfortunately, I see no way of turning this explanation into a rigorous proof. Perhaps it is already, if you modify it slightly, a rigorous proof.
Here is a way to turn your last intuitive argument into a formal proof ^_^
1 The definition of $\log$
The definition of $\log_ab$ is that it is the number $x$ which you raise $a$ to get $b$.
$$\log_a b = x \quad\equiv\quad a^x = b $$
Taking $x$ to be $\log_a b$ makes the right side true and the left side becomes: $$a^{\log_a b} = b$$
That is, raising $a$ by $\log_a b$ gives $b$ ---which is the desired interface for $\log$.
2 The proof
It is obviously clear that to get $c^x$ from $c$, you just raise $c$ by $x$.That is:
\begin{align} & \log_c (c^x) = x \\ \equiv\quad & c ^ x = c^x & \{\text{ Definition of $\log$ }\} \\ \equiv\quad & \mathsf{true} & \{\text{ reflexivity of equality }\} \end{align}
2 Discovering a Solution
It is not so obviously clear how to get $b^c$ from $a$. Rather than guess and check, let us calculate! Let $x$ be the unknown solution which we are look for.
\begin{align} & \log_a (b^c) = x \\ \equiv\quad & a^x = b^c & \{\text{ Definition of $\log$ }\} \\ \equiv\quad & a^x = (a^{\log_a b})^c & \{\text{ To get to $b$ from $a$, use $\log_ab$ }\} \\ \equiv\quad & a^x = a^{((\log_a b) \cdot c)} & \{\text{ Exponents }\} \\ \equiv\quad & x = ((\log_a b) \cdot c) & \{\text{ Exponents }\} \\ \equiv\quad & x = c \cdot \log_a b & \{\text{Arithmetic }\} \end{align}
Hence, we have calculated the power rule for logarithms.
There were some jumps in the above calculation, and so it could be massively improved, but it's in the right spirit of calculating from definitions.