awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
pos :
  Even k →
    (HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2 *
              preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) -
            preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) *
              HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1)) 2) *
          1 *
        b =
      HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1) * 1) 2 *
          (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) * b) -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) * b *
          HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1) * 1) 2
neg :
  ¬Even k →
    (HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2 *
              preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) -
            preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) *
              HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1)) 2) *
          b *
        b =
      HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1) * b) 2 *
          (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) * 1) -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) * 1 *
          HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1) * b) 2
⊢ ((HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2 *
            preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) -
          preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) *
            HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1)) 2) *
        if Even k then 1 else b) *
      b =
    HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1) * if ¬Even k then b else 1) 2 *
        (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) * if Even k then b else 1) -
      (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) * if Even k then b else 1) *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1) * if ¬Even k then b else 1) 2

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
h : Even k
⊢ (HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2 *
            preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) -
          preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) *
            HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1)) 2) *
        1 *
      b =
    HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1) * 1) 2 *
        (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) * b) -
      preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) * b *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1) * 1) 2

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
h : ¬Even k
⊢ (HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2 *
            preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) -
          preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) *
            HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1)) 2) *
        b *
      b =
    HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1) * b) 2 *
        (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) * 1) -
      preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) * 1 *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1) * b) 2

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
rw :
  normEDS b c d m *
      (HPow.hPow (β := ℕ) (normEDS b c d (m - 1)) 2 * normEDS b c d (m + 2) -
        normEDS b c d (m - 2) * HPow.hPow (β := ℕ) (normEDS b c d (m + 1)) 2) =
    HPow.hPow (β := ℕ) (normEDS b c d (m - 1)) 2 * normEDS b c d m * normEDS b c d (m + 2) -
      normEDS b c d (m - 2) * normEDS b c d m * HPow.hPow (β := ℕ) (normEDS b c d (m + 1)) 2
⊢ normEDS b c d (2 * m) * b =
    HPow.hPow (β := ℕ) (normEDS b c d (m - 1)) 2 * normEDS b c d m * normEDS b c d (m + 2) -
      normEDS b c d (m - 2) * normEDS b c d m * HPow.hPow (β := ℕ) (normEDS b c d (m + 1)) 2

Tactic:
rw [← normEDS_mul_complEDS₂, mul_assoc, complEDS₂_mul_b]

Premises used: mul_assoc, complEDS₂_mul_b, normEDS_mul_complEDS₂
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
⊢ normEDS b c d m *
      (HPow.hPow (β := ℕ) (normEDS b c d (m - 1)) 2 * normEDS b c d (m + 2) -
        normEDS b c d (m - 2) * HPow.hPow (β := ℕ) (normEDS b c d (m + 1)) 2) =
    HPow.hPow (β := ℕ) (normEDS b c d (m - 1)) 2 * normEDS b c d m * normEDS b c d (m + 2) -
      normEDS b c d (m - 2) * normEDS b c d m * HPow.hPow (β := ℕ) (normEDS b c d (m + 1)) 2

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
simp_rw :
  ((preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) * HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m) 3 *
          if Even m then HPow.hPow (β := ℕ) b 4 else 1) -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) *
            HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1)) 3 *
          if Even m then 1 else HPow.hPow (β := ℕ) b 4) *
      1 =
    (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) * if Even m then b else 1) *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m * if Even m then b else 1) 3 -
      (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) * if ¬Even m then b else 1) *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1) * if ¬Even m then b else 1) 3
⊢ normEDS b c d (2 * m + 1) =
    normEDS b c d (m + 2) * HPow.hPow (β := ℕ) (normEDS b c d m) 3 -
      normEDS b c d (m - 1) * HPow.hPow (β := ℕ) (normEDS b c d (m + 1)) 3

Tactic:
simp_rw [normEDS, preNormEDS_odd, if_neg m.not_even_two_mul_add_one, Int.even_add, Int.even_sub,
    even_two, iff_true, Int.not_even_one, iff_false]

Premises used: iff_false, even_two, Int.not_even_one, iff_true, normEDS, Int.not_even_two_mul_add_one, Int.even_add, preNormEDS_odd, if_neg, Int.even_sub
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
pos :
  Even m →
    (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) *
              HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m) 3 *
            HPow.hPow (β := ℕ) b 4 -
          preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) *
              HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1)) 3 *
            1) *
        1 =
      preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) * b *
          HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m * b) 3 -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) * 1 *
          HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1) * 1) 3
neg :
  ¬Even m →
    (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) *
              HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m) 3 *
            1 -
          preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) *
              HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1)) 3 *
            HPow.hPow (β := ℕ) b 4) *
        1 =
      preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) * 1 *
          HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m * 1) 3 -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) * b *
          HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1) * b) 3
⊢ ((preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) * HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m) 3 *
          if Even m then HPow.hPow (β := ℕ) b 4 else 1) -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) *
            HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1)) 3 *
          if Even m then 1 else HPow.hPow (β := ℕ) b 4) *
      1 =
    (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) * if Even m then b else 1) *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m * if Even m then b else 1) 3 -
      (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) * if ¬Even m then b else 1) *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1) * if ¬Even m then b else 1) 3

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
h : Even m
⊢ (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) * HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m) 3 *
          HPow.hPow (β := ℕ) b 4 -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) *
            HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1)) 3 *
          1) *
      1 =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) * b *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m * b) 3 -
      preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) * 1 *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1) * 1) 3

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
h : ¬Even m
⊢ (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) * HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m) 3 *
          1 -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) *
            HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1)) 3 *
          HPow.hPow (β := ℕ) b 4) *
      1 =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 2) * 1 *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d m * 1) 3 -
      preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m - 1) * b *
        HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (m + 1) * b) 3

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n : ℕ
h : (k : ℕ) → k < HMul.hMul (α := ℕ) 2 0 → P k
⊢ P (HMul.hMul (α := ℕ) 2 0)

Tactic:
exacts [zero, two, four, even _ h]
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 3) → P k) → P (2 * (m + 3))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 2) + 1 → P k) → P (2 * (m + 2) + 1)
n : ℕ
h : (k : ℕ) → k < HMul.hMul (α := ℕ) 2 0 + 1 → P k
⊢ P (HMul.hMul (α := ℕ) 2 0 + 1)

Tactic:
exacts [one, three, odd _ h]
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
a : P (x + 1)
a₁ : P (x + 2)
a₂ : P (x + 3)
a₃ : P (x + 4)
a₄ : P (x + 5)
⊢ P (2 * (x + 3))

Tactic:
apply even
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
linarith :
  2 * (x + 3) ≤ x + 1 →
    HMul.hMul (α := ℤ) 5 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) =
      0
linarith₁ : 2 * (x + 3) ≤ x + 1 → GT.gt (α := ℤ) 5 0
⊢ x + 1 < 2 * (x + 3)

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
⊢ P (x + 1)

Tactic:
exact ih _ <| by linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
linarith :
  2 * (x + 3) ≤ x + 2 →
    HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 2) =
      0
linarith₁ : 2 * (x + 3) ≤ x + 2 → GT.gt (α := ℤ) 4 0
⊢ x + 2 < 2 * (x + 3)

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
⊢ P (x + 2)

Tactic:
exact ih _ <| by linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
linarith :
  2 * (x + 3) ≤ x + 3 →
    HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 3) =
      0
linarith₁ : 2 * (x + 3) ≤ x + 3 → GT.gt (α := ℤ) 3 0
⊢ x + 3 < 2 * (x + 3)

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
⊢ P (x + 3)

Tactic:
exact ih _ <| by linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
linarith :
  2 * (x + 3) ≤ x + 4 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 4) =
      0
linarith₁ : 2 * (x + 3) ≤ x + 4 → GT.gt (α := ℤ) 2 0
⊢ x + 4 < 2 * (x + 3)

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
⊢ P (x + 4)

Tactic:
exact ih _ <| by linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
linarith :
  2 * (x + 3) ≤ x + 5 →
    -1 + HSub.hSub (α := ℤ) 0 (↑x : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 5) = 0
⊢ x + 5 < 2 * (x + 3)

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 3) → P k
⊢ P (x + 5)

Tactic:
exact ih _ <| by linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
a : P (x + 1)
a₁ : P (x + 2)
a₂ : P (x + 3)
a₃ : P (x + 4)
⊢ P (2 * (x + 2) + 1)

Tactic:
apply odd
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
linarith :
  2 * (x + 2) + 1 ≤ x + 1 →
    HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) =
      0
linarith₁ : 2 * (x + 2) + 1 ≤ x + 1 → GT.gt (α := ℤ) 4 0
⊢ x + 1 < 2 * (x + 2) + 1

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
⊢ P (x + 1)

Tactic:
exact ih _ <| by linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
linarith :
  2 * (x + 2) + 1 ≤ x + 2 →
    HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 2) =
      0
linarith₁ : 2 * (x + 2) + 1 ≤ x + 2 → GT.gt (α := ℤ) 3 0
⊢ x + 2 < 2 * (x + 2) + 1

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
⊢ P (x + 2)

Tactic:
exact ih _ <| by linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
linarith :
  2 * (x + 2) + 1 ≤ x + 3 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 3) =
      0
linarith₁ : 2 * (x + 2) + 1 ≤ x + 3 → GT.gt (α := ℤ) 2 0
⊢ x + 3 < 2 * (x + 2) + 1

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
⊢ P (x + 3)

Tactic:
exact ih _ <| by linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
linarith :
  2 * (x + 2) + 1 ≤ x + 4 →
    -1 + HSub.hSub (α := ℤ) 0 (↑x : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 4) = 0
⊢ x + 4 < 2 * (x + 2) + 1

Tactic:
linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
P : ℕ → Sort u
zero : P 0
one : P 1
two : P 2
three : P 3
four : P 4
even : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (m + 5) → P (2 * (m + 3))
odd : (m : ℕ) → P (m + 1) → P (m + 2) → P (m + 3) → P (m + 4) → P (2 * (m + 2) + 1)
n x : ℕ
ih : (k : ℕ) → k < 2 * (x + 2) + 1 → P k
⊢ P (x + 4)

Tactic:
exact ih _ <| by linarith only
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
rw rw₁ : Eq.{u + 1} (α := R) 0 0
⊢ complEDS' b c d k 0 = 0

Tactic:
rw [complEDS']

Premises used: complEDS'
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
rw rw₁ : Eq.{u + 1} (α := R) 1 1
⊢ complEDS' b c d k 1 = 1

Tactic:
rw [complEDS']

Premises used: complEDS'
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ 2 * (m + 1) = 2 * m + 2

Tactic:
rfl
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
rw : complEDS' b c d k (2 * m + 2) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
rw₁ :
  (if hn : Even (2 * m) then complEDS' b c d k (2 * m / 2 + 1) * complEDS₂ b c d ((↑(2 * m / 2 + 1) : ℤ) * k)
    else
      have this := ⋯;
      HPow.hPow (β := ℕ) (complEDS' b c d k (2 * m / 2 + 1)) 2 *
            normEDS b c d (HAdd.hAdd (α := ℤ) (↑(2 * m / 2 + 1) : ℤ) 1 * k + 1) *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑(2 * m / 2 + 1) : ℤ) 1 * k - 1) -
        HPow.hPow (β := ℕ) (complEDS' b c d k (2 * m / 2 + 1 + 1)) 2 * normEDS b c d ((↑(2 * m / 2 + 1) : ℤ) * k + 1) *
          normEDS b c d ((↑(2 * m / 2 + 1) : ℤ) * k - 1)) =
    complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
rw₂ :
  complEDS' b c d k (2 * m / 2 + 1) * complEDS₂ b c d ((↑(2 * m / 2 + 1) : ℤ) * k) =
    complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
rw₃ :
  complEDS' b c d k (m + 1) * complEDS₂ b c d ((↑(m + 1) : ℤ) * k) =
    complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
rw₄ rw₅ :
  complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) =
    complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)
⊢ complEDS' b c d k (2 * (m + 1)) = complEDS' b c d k (m + 1) * complEDS₂ b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k)

Tactic:
rw [show 2 * (m + 1) = 2 * m + 2 by rfl, complEDS', dif_pos <| even_two_mul m,
    m.mul_div_cancel_left two_pos, Nat.cast_succ]

Premises used: Nat.cast_succ, Nat.mul_div_cancel_left, two_pos, dif_pos, complEDS', even_two_mul
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ 2 * (m + 1) + 1 = 2 * m + 3

Tactic:
rfl