awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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)
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
⊢ 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)

Tactic:
simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]

Premises used: map_sub, apply_ite, preNormEDS'_odd, map_pow, map_mul, preNormEDS'_even, map_one, DFunLike.coe
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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
linarith₁ : 2 * (m + 3) ≤ m + 2 → GT.gt (α := ℤ) 4 0
⊢ m + 2 < 2 * (m + 3)

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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)
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
⊢ 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:
rw [ih _ <| by linarith only]
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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
linarith₁ : 2 * (m + 3) ≤ m + 3 → GT.gt (α := ℤ) 3 0
⊢ m + 3 < 2 * (m + 3)

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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)
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
⊢ 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]
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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 + 5 →
    -1 + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 5) = 0
⊢ m + 5 < 2 * (m + 3)

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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
linarith₁ : 2 * (m + 3) ≤ m + 1 → GT.gt (α := ℤ) 5 0
⊢ m + 1 < 2 * (m + 3)

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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 + 4 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) =
      0
linarith₁ : 2 * (m + 3) ≤ m + 4 → GT.gt (α := ℤ) 2 0
⊢ m + 4 < 2 * (m + 3)

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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 :
  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)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d (2 * (m + 2) + 1)) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (2 * (m + 2) + 1) : S)

Tactic:
simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]

Premises used: map_sub, apply_ite, preNormEDS'_odd, map_pow, map_mul, preNormEDS'_even, map_one, DFunLike.coe
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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)
linarith :
  2 * (m + 2) + 1 ≤ m + 4 →
    -1 + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 4) = 0
⊢ m + 4 < 2 * (m + 2) + 1

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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 :
  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)
⊢ 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)

Tactic:
rw [ih _ <| by linarith only]
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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)
linarith :
  2 * (m + 2) + 1 ≤ m + 2 →
    HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) =
      0
linarith₁ : 2 * (m + 2) + 1 ≤ m + 2 → GT.gt (α := ℤ) 3 0
⊢ m + 2 < 2 * (m + 2) + 1

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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 :
  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) (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)

Tactic:
rw [ih _ <| by linarith only]
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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)
linarith :
  2 * (m + 2) + 1 ≤ m + 1 →
    HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) =
      0
linarith₁ : 2 * (m + 2) + 1 ≤ m + 1 → GT.gt (α := ℤ) 4 0
⊢ m + 1 < 2 * (m + 2) + 1

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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 :
  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)
⊢ 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)

Tactic:
rw [ih _ <| by linarith only]