awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      HPow.hPow (β := ℕ) (complEDS b c d k (↑n : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * k + 1) *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * k - 1) -
        HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 * normEDS b c d ((↑n : ℤ) * k + 1) *
          normEDS b c d ((↑n : ℤ) * k - 1)
m : ℕ
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑m : ℤ)) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (-(↑m : ℤ))) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) 2 * normEDS b c d (-(↑m : ℤ) * k + 1) *
        normEDS b c d (-(↑m : ℤ) * k - 1)
have neg : complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑0 : ℤ)) + 1) =
  HPow.hPow (β := ℕ) (complEDS b c d k (-(↑0 : ℤ))) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1 * k + 1) *
      normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1 * k - 1) -
    HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1)) 2 * normEDS b c d (-(↑0 : ℤ) * k + 1) *
      normEDS b c d (-(↑0 : ℤ) * k - 1)
Tactic: rcases m with _ | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      HPow.hPow (β := ℕ) (complEDS b c d k (↑n : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * k + 1) *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * k - 1) -
        HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 * normEDS b c d ((↑n : ℤ) * k + 1) *
          normEDS b c d ((↑n : ℤ) * k - 1)
m : ℕ
neg :
  complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑0 : ℤ)) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (-(↑0 : ℤ))) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1)) 2 * normEDS b c d (-(↑0 : ℤ) * k + 1) *
        normEDS b c d (-(↑0 : ℤ) * k - 1)
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑m : ℤ)) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (-(↑m : ℤ))) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) 2 * normEDS b c d (-(↑m : ℤ) * k + 1) *
        normEDS b c d (-(↑m : ℤ) * k - 1)
have neg₁ : ∀ (m : ℕ),
  complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑(m + 1) : ℤ)) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (-(↑(m + 1) : ℤ))) 2 *
          normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1)) 2 *
          normEDS b c d (-(↑(m + 1) : ℤ) * k + 1) *
        normEDS b c d (-(↑(m + 1) : ℤ) * k - 1)
Tactic: rcases m with _ | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      HPow.hPow (β := ℕ) (complEDS b c d k (↑n : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * k + 1) *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * k - 1) -
        HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 * normEDS b c d ((↑n : ℤ) * k + 1) *
          normEDS b c d ((↑n : ℤ) * k - 1)
m : ℕ
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑(m + 1) : ℤ)) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (-(↑(m + 1) : ℤ))) 2 *
          normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1)) 2 *
          normEDS b c d (-(↑(m + 1) : ℤ) * k + 1) *
        normEDS b c d (-(↑(m + 1) : ℤ) * k - 1)
have neg : -(HPow.hPow (β := ℕ) (complEDS b c d k (↑m : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2 * normEDS b c d ((↑m : ℤ) * k + 1) *
        normEDS b c d ((↑m : ℤ) * k - 1)) =
  HPow.hPow (β := ℕ) (-complEDS b c d k (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2 * -normEDS b c d ((↑m : ℤ) * k - 1) *
      -normEDS b c d ((↑m : ℤ) * k + 1) -
    HPow.hPow (β := ℕ) (-complEDS b c d k (↑m : ℤ)) 2 * -normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) *
      -normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1)
Tactic: simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
      show (-(m + 1 : ℤ) + 1) = -m by ring1, neg_mul, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add,
      ← neg_add', complEDS_neg, normEDS_neg, ih]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k m : ℤ
⊢ complEDS b c d k (2 * m + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k m) 2 * normEDS b c d ((m + 1) * k + 1) * normEDS b c d ((m + 1) * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (m + 1)) 2 * normEDS b c d (m * k + 1) * normEDS b c d (m * k - 1)
have nat : ∀ (m : ℕ),
  complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (↑m : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2 * normEDS b c d ((↑m : ℤ) * k + 1) *
        normEDS b c d ((↑m : ℤ) * k - 1)
Tactic: induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _
    · simp
    norm_cast
    simpa only [complEDS_ofNat] using complEDS'_odd ..
  | neg ih m =>
    rcases m with _ | m
    · simp
    simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
      show (-(m + 1 : ℤ) + 1) = -m by ring1, neg_mul, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add,
      ← neg_add', complEDS_neg, normEDS_neg, ih]
    ring1
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k m : ℤ
nat :
  ∀ (m : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 1) =
      HPow.hPow (β := ℕ) (complEDS b c d k (↑m : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) -
        HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 2 * normEDS b c d ((↑m : ℤ) * k + 1) *
          normEDS b c d ((↑m : ℤ) * k - 1)
⊢ complEDS b c d k (2 * m + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k m) 2 * normEDS b c d ((m + 1) * k + 1) * normEDS b c d ((m + 1) * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (m + 1)) 2 * normEDS b c d (m * k + 1) * normEDS b c d (m * k - 1)
have neg : ∀
  (ih :
    ∀ (n : ℕ),
      complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
        HPow.hPow (β := ℕ) (complEDS b c d k (↑n : ℤ)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * k + 1) *
            normEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 * k - 1) -
          HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 2 * normEDS b c d ((↑n : ℤ) * k + 1) *
            normEDS b c d ((↑n : ℤ) * k - 1))
  (m : ℕ),
  complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑m : ℤ)) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (-(↑m : ℤ))) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) 2 * normEDS b c d (-(↑m : ℤ) * k + 1) *
        normEDS b c d (-(↑m : ℤ) * k - 1)
Tactic: induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _
    · simp
    norm_cast
    simpa only [complEDS_ofNat] using complEDS'_odd ..
  | neg ih m =>
    rcases m with _ | m
    · simp
    simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
      show (-(m + 1 : ℤ) + 1) = -m by ring1, neg_mul, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add,
      ← neg_add', complEDS_neg, normEDS_neg, ih]
    ring1
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
P : ℕ → Sort u
zero : P 0
one : P 1
even : (m : ℕ) → P (m + 1) → P (2 * (m + 1))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (2 * (m + 1) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 1) → P k
⊢ x + 1 < 2 * (x + 1)
have linarith : 2 * (x + 1) ≤ x + 1 →
  -1 + HSub.hSub (α := ℤ) 0 (↑x : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) = 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
P : ℕ → Sort u
zero : P 0
one : P 1
even : (m : ℕ) → P (m + 1) → P (2 * (m + 1))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (2 * (m + 1) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 1) + 1 → P k
⊢ x + 1 < 2 * (x + 1) + 1
have linarith : 2 * (x + 1) + 1 ≤ x + 1 →
  HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) =
    0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
P : ℕ → Sort u
zero : P 0
one : P 1
even : (m : ℕ) → P (m + 1) → P (2 * (m + 1))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (2 * (m + 1) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 1) + 1 → P k
linarith :
  2 * (x + 1) + 1 ≤ x + 1 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) =
      0
⊢ x + 1 < 2 * (x + 1) + 1
have linarith₁ : 2 * (x + 1) + 1 ≤ x + 1 → GT.gt (α := ℤ) 2 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
P : ℕ → Sort u
zero : P 0
one : P 1
even : (m : ℕ) → P (m + 1) → P (2 * (m + 1))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (2 * (m + 1) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 1) + 1 → P k
⊢ x + 2 < 2 * (x + 1) + 1
have linarith : 2 * (x + 1) + 1 ≤ x + 2 →
  -1 + HSub.hSub (α := ℤ) 0 (↑x : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 2) = 0
Tactic: linarith only
-- 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 + 3),
    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)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d (2 * (m + 3))) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (2 * (m + 3)) : S)
have even : HMul.hMul (β := S)
      (HMul.hMul (β := S) (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 2)) : S) 2)
        ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S))
      ((f : (a : R) → S) (preNormEDS' b c d (m + 5)) : S) -
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 1)) : S)
        ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S) *
      HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 4)) : S) 2 =
  HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 2)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S))
      (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 5) : S) -
    HMul.hMul (α := S) (β := S)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) *
      HPow.hPow (α := S) (β := ℕ)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S) 2
Tactic: simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
-- 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 + 3),
    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)
⊢ m + 2 < 2 * (m + 3)
have linarith : 2 * (m + 3) ≤ m + 2 →
  HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) =
    0
Tactic: linarith only
-- 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 + 3),
    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)
linarith :
  2 * (m + 3) ≤ m + 2 →
    HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) =
      0
⊢ m + 2 < 2 * (m + 3)
have linarith₁ : 2 * (m + 3) ≤ m + 2 → GT.gt (α := ℤ) 4 0
Tactic: linarith only
-- 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 + 3),
    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)
⊢ HMul.hMul (β := S)
        (HMul.hMul (β := S) (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 2)) : S) 2)
          ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S))
        ((f : (a : R) → S) (preNormEDS' b c d (m + 5)) : S) -
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 1)) : S)
          ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S) *
        HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 4)) : S) 2 =
    HMul.hMul (β := S)
        (HMul.hMul (β := S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 2)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S))
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 5) : S) -
      HMul.hMul (α := S) (β := S)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) *
        HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S) 2
have even : HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 2)
        ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S))
      ((f : (a : R) → S) (preNormEDS' b c d (m + 5)) : S) -
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 1)) : S)
        ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S) *
      HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 4)) : S) 2 =
  HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 2)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S))
      (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 5) : S) -
    HMul.hMul (α := S) (β := S)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) *
      HPow.hPow (α := S) (β := ℕ)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S) 2
Tactic: rw [ih _ <| by linarith only]
-- 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 + 3),
    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)
⊢ m + 3 < 2 * (m + 3)
have linarith : 2 * (m + 3) ≤ m + 3 →
  HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) =
    0
Tactic: linarith only
-- 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 + 3),
    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)
linarith :
  2 * (m + 3) ≤ m + 3 →
    HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) =
      0
⊢ m + 3 < 2 * (m + 3)
have linarith₁ : 2 * (m + 3) ≤ m + 3 → GT.gt (α := ℤ) 3 0
Tactic: linarith only
-- 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 + 3),
    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)
⊢ HMul.hMul (β := S)
        (HMul.hMul (β := S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 2)
          ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S))
        ((f : (a : R) → S) (preNormEDS' b c d (m + 5)) : S) -
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 1)) : S)
          ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S) *
        HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 4)) : S) 2 =
    HMul.hMul (β := S)
        (HMul.hMul (β := S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 2)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S))
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 5) : S) -
      HMul.hMul (α := S) (β := S)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) *
        HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S) 2
have even : HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 2)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S))
      ((f : (a : R) → S) (preNormEDS' b c d (m + 5)) : S) -
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 1)) : S)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) *
      HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 4)) : S) 2 =
  HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 2)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S))
      (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 5) : S) -
    HMul.hMul (α := S) (β := S)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) *
      HPow.hPow (α := S) (β := ℕ)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S) 2
Tactic: rw [ih _ <| by linarith only]
-- 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 + 3),
    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)
⊢ m + 5 < 2 * (m + 3)
have linarith : 2 * (m + 3) ≤ m + 5 →
  -1 + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 5) = 0
Tactic: linarith only
-- 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 + 3),
    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)
⊢ m + 1 < 2 * (m + 3)
have linarith : 2 * (m + 3) ≤ m + 1 →
  HMul.hMul (α := ℤ) 5 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) =
    0
Tactic: linarith only
-- 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 + 3),
    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)
linarith :
  2 * (m + 3) ≤ m + 1 →
    HMul.hMul (α := ℤ) 5 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) =
      0
⊢ m + 1 < 2 * (m + 3)
have linarith₁ : 2 * (m + 3) ≤ m + 1 → GT.gt (α := ℤ) 5 0
Tactic: linarith only
-- 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 + 3),
    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)
⊢ m + 4 < 2 * (m + 3)
have linarith : 2 * (m + 3) ≤ m + 4 →
  HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) =
    0
Tactic: linarith only