-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
m : ℕ
ih :
  ∀ k < 2 * (m + 2) + 1,
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d k) : S)
      (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k : S)
odd odd₁ odd₂ :
  HMul.hMul (β := S)
        (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S)
          (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 2)) : S) 3))
        (if Even m then (f : (a : R) → S) b else 1 : S) -
      HMul.hMul (β := S)
        (HMul.hMul (α := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 1)) : S)
          (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S) 3))
        (if Even m then 1 else (f : (a : R) → S) b : S) =
    HMul.hMul (β := S)
        (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 3))
        (if Even m then (f : (a : R) → S) b else 1 : S) -
      HMul.hMul (β := S)
        (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) 3))
        (if Even m then 1 else (f : (a : R) → S) b : S)
odd₃ :
  HMul.hMul (β := S)
        (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 3))
        (if Even m then (f : (a : R) → S) b else 1 : S) -
      HMul.hMul (β := S)
        (HMul.hMul (α := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 1)) : S)
          (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S) 3))
        (if Even m then 1 else (f : (a : R) → S) b : S) =
    HMul.hMul (β := S)
        (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 3))
        (if Even m then (f : (a : R) → S) b else 1 : S) -
      HMul.hMul (β := S)
        (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) 3))
        (if Even m then 1 else (f : (a : R) → S) b : S)
⊢ HMul.hMul (β := S)
        (HMul.hMul (α := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 4)) : S)
          (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 2)) : S) 3))
        (if Even m then (f : (a : R) → S) b else 1 : S) -
      HMul.hMul (β := S)
        (HMul.hMul (α := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 1)) : S)
          (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S) 3))
        (if Even m then 1 else (f : (a : R) → S) b : S) =
    HMul.hMul (β := S)
        (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 3))
        (if Even m then (f : (a : R) → S) b else 1 : S) -
      HMul.hMul (β := S)
        (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) 3))
        (if Even m then 1 else (f : (a : R) → S) b : S)
have odd₄ : HMul.hMul (β := S)
      (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S)
        (HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 3))
      (if Even m then (f : (a : R) → S) b else 1 : S) -
    HMul.hMul (β := S)
      (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
        (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S) 3))
      (if Even m then 1 else (f : (a : R) → S) b : S) =
  HMul.hMul (β := S)
      (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S)
        (HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 3))
      (if Even m then (f : (a : R) → S) b else 1 : S) -
    HMul.hMul (β := S)
      (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
        (HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) 3))
      (if Even m then 1 else (f : (a : R) → S) b : S)
Tactic: repeat rw [ih _ <| by linarith only]