-- 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
k : ℤ
m : ℕ
ih :
  ∀ k_1 < 2 * (m + 1) + 1,
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)
⊢ HMul.hMul (β := S)
        (HMul.hMul (β := S)
          (HPow.hPow (α := S) (β := ℕ)
            (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S) 2)
          (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
              (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) :
            S))
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) :
          S) -
      HMul.hMul (β := S)
        (HMul.hMul (β := S) (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (complEDS' b c d k (m + 2)) : S) 2)
          (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
              (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) :
            S))
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) :
          S) =
    HMul.hMul (β := S)
        (HMul.hMul (β := S)
          (HPow.hPow (α := S) (β := ℕ)
            (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S) 2)
          (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
              (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) :
            S))
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) :
          S) -
      HMul.hMul (β := S)
        (HMul.hMul (β := S)
          (HPow.hPow (α := S) (β := ℕ)
            (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 2) : S) 2)
          (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
              (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) :
            S))
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) :
          S)
have odd : HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S) 2)
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) :
          S))
      (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
          (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) :
        S) -
    HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 2) : S) 2)
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) :
          S))
      (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
          (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) :
        S) =
  HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S) 2)
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) :
          S))
      (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
          (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) :
        S) -
    HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 2) : S) 2)
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) :
          S))
      (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
          (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) :
        S)
Tactic: rw [ih _ <| by linarith only]