-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
private lemma expDegree_rec (m : ℕ) :
    (expDegree (2 * (m + 3)) = 2 * expDegree (m + 2) + expDegree (m + 3) + expDegree (m + 5) ∧
    expDegree (2 * (m + 3)) = expDegree (m + 1) + expDegree (m + 3) + 2 * expDegree (m + 4)) ∧
    (expDegree (2 * (m + 2) + 1) =
      expDegree (m + 4) + 3 * expDegree (m + 2) + (if Even m then 2 * 3 else 0) ∧
    expDegree (2 * (m + 2) + 1) =
      expDegree (m + 1) + 3 * expDegree (m + 3) + (if Even m then 0 else 2 * 3))

Proof state:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1)) ∧
    ((↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      (↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * if Even m then 0 else 6

Tactic:
push_cast [Nat.even_add_one, ite_not, even_two_mul]

Result:
m : ℕ
⊢ ((2 * ↑m + 6) ^ 2 - 4 =
        2 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
          ((↑m + 5) ^ 2 - if Even m then 1 else 4) ∧
      (2 * ↑m + 6) ^ 2 - 4 =
        ((↑m + 1) ^ 2 - if Even m then 1 else 4) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
          2 * ((↑m + 4) ^ 2 - if Even m then 4 else 1)) ∧
    ((2 * ↑m + 4 + 1) ^ 2 - 1 =
        ((↑m + 4) ^ 2 - if Even m then 4 else 1) + 3 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      (2 * ↑m + 4 + 1) ^ 2 - 1 =
        ((↑m + 1) ^ 2 - if Even m then 1 else 4) + 3 * ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
          2 * if Even m then 0 else 6

Proof state:
m : ℕ
⊢ ((2 * ↑m + 6) ^ 2 - 4 =
        2 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
          ((↑m + 5) ^ 2 - if Even m then 1 else 4) ∧
      (2 * ↑m + 6) ^ 2 - 4 =
        ((↑m + 1) ^ 2 - if Even m then 1 else 4) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
          2 * ((↑m + 4) ^ 2 - if Even m then 4 else 1)) ∧
    ((2 * ↑m + 4 + 1) ^ 2 - 1 =
        ((↑m + 4) ^ 2 - if Even m then 4 else 1) + 3 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      (2 * ↑m + 4 + 1) ^ 2 - 1 =
        ((↑m + 1) ^ 2 - if Even m then 1 else 4) + 3 * ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
          2 * if Even m then 0 else 6

Tactic:
constructor <;> constructor <;> split_ifs <;> ring1

Result:
no goals

Proof state:
m : ℕ
⊢ (WeierstrassCurve.expDegree (2 * (m + 3)) =
        2 * WeierstrassCurve.expDegree (m + 2) + WeierstrassCurve.expDegree (m + 3) +
          WeierstrassCurve.expDegree (m + 5) ∧
      WeierstrassCurve.expDegree (2 * (m + 3)) =
        WeierstrassCurve.expDegree (m + 1) + WeierstrassCurve.expDegree (m + 3) +
          2 * WeierstrassCurve.expDegree (m + 4)) ∧
    (WeierstrassCurve.expDegree (2 * (m + 2) + 1) =
        WeierstrassCurve.expDegree (m + 4) + 3 * WeierstrassCurve.expDegree (m + 2) + if Even m then 2 * 3 else 0) ∧
      WeierstrassCurve.expDegree (2 * (m + 2) + 1) =
        WeierstrassCurve.expDegree (m + 1) + 3 * WeierstrassCurve.expDegree (m + 3) + if Even m then 0 else 2 * 3

Tactic:
push_cast [← @Nat.cast_inj ℤ, ← mul_left_cancel_iff_of_pos (b := (expDegree _ : ℤ)) two_pos,
  mul_add, mul_left_comm (2 : ℤ)]

Result:
m : ℕ
⊢ (2 * ↑(WeierstrassCurve.expDegree (2 * m + 6)) =
        2 * (2 * ↑(WeierstrassCurve.expDegree (m + 2))) + 2 * ↑(WeierstrassCurve.expDegree (m + 3)) +
          2 * ↑(WeierstrassCurve.expDegree (m + 5)) ∧
      2 * ↑(WeierstrassCurve.expDegree (2 * m + 6)) =
        2 * ↑(WeierstrassCurve.expDegree (m + 1)) + 2 * ↑(WeierstrassCurve.expDegree (m + 3)) +
          2 * (2 * ↑(WeierstrassCurve.expDegree (m + 4)))) ∧
    (2 * ↑(WeierstrassCurve.expDegree (2 * m + 4 + 1)) =
        2 * ↑(WeierstrassCurve.expDegree (m + 4)) + 3 * (2 * ↑(WeierstrassCurve.expDegree (m + 2))) +
          2 * if Even m then 6 else 0) ∧
      2 * ↑(WeierstrassCurve.expDegree (2 * m + 4 + 1)) =
        2 * ↑(WeierstrassCurve.expDegree (m + 1)) + 3 * (2 * ↑(WeierstrassCurve.expDegree (m + 3))) +
          2 * if Even m then 0 else 6

Proof state:
m : ℕ
⊢ (2 * ↑(WeierstrassCurve.expDegree (2 * m + 6)) =
        2 * (2 * ↑(WeierstrassCurve.expDegree (m + 2))) + 2 * ↑(WeierstrassCurve.expDegree (m + 3)) +
          2 * ↑(WeierstrassCurve.expDegree (m + 5)) ∧
      2 * ↑(WeierstrassCurve.expDegree (2 * m + 6)) =
        2 * ↑(WeierstrassCurve.expDegree (m + 1)) + 2 * ↑(WeierstrassCurve.expDegree (m + 3)) +
          2 * (2 * ↑(WeierstrassCurve.expDegree (m + 4)))) ∧
    (2 * ↑(WeierstrassCurve.expDegree (2 * m + 4 + 1)) =
        2 * ↑(WeierstrassCurve.expDegree (m + 4)) + 3 * (2 * ↑(WeierstrassCurve.expDegree (m + 2))) +
          2 * if Even m then 6 else 0) ∧
      2 * ↑(WeierstrassCurve.expDegree (2 * m + 4 + 1)) =
        2 * ↑(WeierstrassCurve.expDegree (m + 1)) + 3 * (2 * ↑(WeierstrassCurve.expDegree (m + 3))) +
          2 * if Even m then 0 else 6

Tactic:
repeat rw [expDegree_cast <| by omega]

Result:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1)) ∧
    ((↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (↑(m + 4) ^ 2 - if Even (m + 4) then 4 else 1) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) +
          2 * if Even m then 6 else 0) ∧
      (↑(2 * m + 4 + 1) ^ 2 - if Even (2 * m + 4 + 1) then 4 else 1) =
        (↑(m + 1) ^ 2 - if Even (m + 1) then 4 else 1) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * if Even m then 0 else 6