doc(tactic/explode): expand doc string (#3271)
Explanation copied from @digama0's Zulip message [here](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.23explode.20error/near/202396813). Also removed a redundant function and added some type ascriptions.
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
