I don't usually start with a statement I want and then look to prove it, it's more like I explore various derivations to see where they lead (probably with some kind of hunches), and then some of them end up in an interesting place.

You can work this way in Lean. You need to have a goal to make the engine happy, but there's no need for the goal to be true -- you can just do something like

    have h : ∀x, ∀y, x = y := by
      -- h is not true, but in the attempt to prove it,
      -- we can do whatever we want.
      -- If we find something interesting, we can redefine h