Simple String.split lemma

Stream: new members

[Jeremy Salwen]

Hello, I am new to lean, working on proving a simple lemma in lean4.

lemma String.split_empty (c): String.split "" c = [""]

I tried looking for existing theorems in mathlib, but it seems like there are no existing theorems about String.split? In any case, I thought it should be easy to prove myself.

My first thought was to just expand definitions and it will probably become trivial. I was able to rewrite String.split with "rw [String.split]" But this reveals a helper function String.splitAux that will not be rewritten by rw [String.splitAux] I tried a few other tactics like unfold, simp, and dsimp, but none of them would touch splitAux.

I did notice that String.splitAux is a "partial def" unline String,split https://github.com/leanprover/lean4/blob/0b243f0ca33e1f6a2948c94896b22b2f304ac4c8/src/Init/Data/String/Basic.lean#L188-L196 so perhaps that is why it is not playing nice with theorem proving?

Any advice on what tactics I should use here? Also, is there a general purpose tactic that will just "compute" the expressions? What about a general purpose hammer tactic like in Coq?