Help {generalize, rename} these lemmas for mathlib

Stream: maths

[Mark Gerads]

I needed these simple lemmas, and was unable to find them in the library.
Before these lemmas can be added to mathlib, they need to be generalized.
I would like some help with that. Whoever helps can take full credit by making the GitHub commit if they wish.
Also, the lemmas need to be renamed to mathlib style.

import analysis.special_functions.trigonometric.basic

lemma cpowIntExponentSplitBase (z1 z2:ℂ) (n:ℕ) : (z1 * z2) ^ n = z1 ^ n * z2 ^ n:=
begin
  induction n with n ih,
  simp only [pow_zero, mul_one],
  rw [pow_succ,pow_succ,pow_succ],
  have h: z1 * z1 ^ n * (z2 * z2 ^ n) = z1 * z2 * (z1 ^ n * z2 ^ n),
    ring,
  rw h,
  congr' 1,
end

lemma cpowIntExponentSplitExponent (z1:ℂ) (n k:ℕ) : z1 ^ (n + k) = z1 ^ n * z1 ^ k:=
begin
  induction k with k ih,
  simp only [add_zero, pow_zero, mul_one],
  have h: k.succ =  k + 1,
  simp only [eq_self_iff_true],
  rw [pow_succ, h],
  have h2: n + (k + 1) = (n+k)+1,
  simp only [add_comm, add_assoc],
  rw h2,
  have h3: n + k + 1=(n + k).succ,
  simp only [eq_self_iff_true],
  rw [h3, pow_succ],
  have h4: z1 ^ n * (z1 * z1 ^ k) = z1 * (z1 ^ n * z1 ^ k),
  ring,
  rw h4,
  congr' 1,
end

lemma cpowIntTimesIntExponent (z1:ℂ) (n k:ℕ) : z1 ^ (n * k) = (z1 ^ n) ^ k:=
begin
  induction k with k ih,
  simp only [mul_zero, pow_zero],
  rw [pow_succ],
  have h: n * k.succ = n*(k+1),
    simp only [eq_self_iff_true],
  rw h,
  have h2: n * (k + 1) = n+n*k,
    ring,
  rw h2,
  have h3:z1 ^ (n + n * k) = z1 ^ n * z1 ^ (n * k),
    exact cpowIntExponentSplitExponent z1 n (n * k),
    rw h3,
  congr' 1,
end

[Alex J. Best]

docs#mul_pow, docs#pow_add, docs#pow_mul I believe. I think will save time if assume that lemmas of this level are in mathlib already (things like this generally are) and look for them with library_search or the naming convention or #Is there code for X? first

[Mark Gerads]

Nice; this will make my file smaller. I tried library_search, but didn't ask at #Is there code for X? .
Maybe library_search!needs to be improved?

[Alex J. Best]

Hmm library search works fine for me for the first one at least. Though I would say the naming convention is even faster

[Mark Gerads]

Interesting. I double-checked that library_search! did not result in anything before making this post. Checking again now, the cause is (deterministic) timeout.

[Jireh Loreaux]

This is the #naming that Alex is referring to. With this consistency in naming, many simple lemmas can be found just by guessing and using the autocomplete feature in VS Code (or in the API documentation). However, if there is something that you think should exist, but can't find, definitely ask in #Is there code for X? first. Simple things especially don't bother to try and reprove.

[Jireh Loreaux]

For example, if you want a lemma to say that a - b - c = a - (b + c), you can easily guess that this will be called docs#sub_sub.

[Alex J. Best]

Ah yes, deterministic timeout isnt a fair per se, just that there are too many lemmas to check with your imports, for the purposes of library search its helpful to set it a bit higher than the default, https://leanprover-community.github.io/tips_and_tricks.html#memory-and-deterministic-timeout.

[Newell Jensen]

Curious what others have set their memory limits at who have done so...

[Newell Jensen]

Or rather, not the exact limits, but if they have found this to actually be beneficial and have noticed a marked difference.

[Mark Gerads]

I changed the Lean settings to have a memory limit of 39000 (most of my RAM), and now library_search! works for all 3 lemmas. I will need to remember this next time I reinstall Linux.

[Newell Jensen]

Mark Gerads said:

I changed the Lean settings to have a memory limit of 39000 (most of my RAM), and now library_search! works for all 3 lemmas. I will need to remember this next time I reinstall Linux.

Good to know! Thanks.

[Jireh Loreaux]

If you are regularly hitting timeouts during development (with the standard heartbeat limit of 100000), in my experience it either means (a) that you are working on some very complicated stuff, or (b) you need to find ways to make your code more efficient and/or idiomatic (e.g., squeezing simps). I just wrote a rather long and complicated proof while using the standard timeout and didn't hit it.

[Alex J. Best]

I dont think the memory limit should affect library search, only the timeout.

[Alex J. Best]

And while that's definitely true Jireh I do find it useful to write a slow proof that works and then speed it up when its done. Something like double the default timeout is normally enough for me

[Mark Gerads]

Alex J. Best said:

I dont think the memory limit should affect library search, only the timeout.

I did not change the timeout, only the memory, so counter-example.

[Jireh Loreaux]

Alex, I see what you mean, and that can be useful in certain circumstances. However, if I'm constantly hitting 100000 heartbeats in a proof that isn't super complex, then I'm spending too much time waiting for Lean to compile every step and I should speed up the proof early anyway to save myself time developing. I guess if you have a very fast machine this is less of an issue, but I'm frequently working on my laptop with only 4 cores.

[Jireh Loreaux]

sometimes having the timeout higher can be useful when squeezing simps though.