Splitting up large proofs

Stream: new members

[Niels Voss]

I have a lemma which has a proof that is 146 lines long, and I think I should probably split it into smaller lemmas. The problem is that most of the lemmas that I could split off are one-off algebra proofs that would pretty much have no utility outside of the larger proof. For example, this appears in the middle of my proof (where A is defined as (b^p - 1)/(b - 1) and B is defined as (b^p + 1)/(b + 1)):

    have ha₁ : (b^2 - 1) * ((A*B) - 1) = b*(b^(p-1) - 1)*(b^p + b),
    { apply_fun (λx, x*(b^2 - 1)) at AB_id,
      rw nat.div_mul_cancel hd at AB_id,
      apply_fun (λx, x - (b^2 - 1)) at AB_id,
      nth_rewrite 1 ←one_mul (b^2 - 1) at AB_id,
      rw [←nat.mul_sub_right_distrib, mul_comm] at AB_id,
      calc (b^2 - 1) * (A * B - 1) = b ^ (2 * p) - 1 - (b^2 - 1) : AB_id
        ... = b ^ (2 * p) - (1 + (b^2 - 1))           : by rw nat.sub_sub
        ... = b ^ (2 * p) - (1 + b^2 - 1)             : by rw nat.add_sub_assoc hi_bsquared
        ... = b ^ (2 * p) - (b^2)                     : by rw nat.add_sub_cancel_left
        ... = b ^ (p * 2) - (b^2)                     : by rw mul_comm
        ... = (b ^ p) ^ 2 - (b^2)                     : by rw pow_mul
        ... = (b ^ p + b) * (b ^ p - b)               : by rw nat.sq_sub_sq
        ... = (b ^ p - b) * (b ^ p + b)               : by rw mul_comm
        ... = (b ^ (p - 1 + 1) - b) * (b ^ p + b)     : by rw nat.sub_add_cancel hi_p
        ... = (b * b ^ (p - 1) - b) * (b ^ p + b)     : by rw pow_succ
        ... = (b * b ^ (p - 1) - b * 1) * (b ^ p + b) : by rw mul_one
        ... = b * (b ^ (p - 1) - 1) * (b ^ p + b)     : by rw nat.mul_sub_left_distrib }

Is it generally fine if I move this statement into a new lemma, even though the lemma wouldn't be very useful by itself and would have many hypotheses?

This proof is part of my WIP pull request #17632 (link to specific lemma). I think that the main reason the proof is long is that I'm inexperienced with lean and I could probably shorten the proof without splitting it if I used more tactics.

[Ruben Van de Velde]

I wonder if that subproof could be solved by zify [proofs that b^2, AB and b^(p-1) are > 1], ring

[Ruben Van de Velde]

What makes this part long is the kind of tedious rearrangement that computers actually should be good at - but nat subtraction might complicate things

[Niels Voss]

The zify tactic certainly looks interesting, I wasn't aware that it existed

[Alex J. Best]

You might need tactic#ring_exp too

[Martin Dvořák]

I had no idea about zify either! It sounds it could be a life-changer!

[Niels Voss]

Apparently there is also a tactic called qify which shifts proofs on nat or int to rat, this might help a lot when doing natural number division