awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℕ
nat :
  preNormEDS b c d (↑(2 * (n + 1 + 1) + 1) : ℤ) =
    (preNormEDS b c d (↑(n + 1 + 1 + 2) : ℤ) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑(n + 1 + 1) : ℤ)) 3 *
        if Even n then b else 1) -
      preNormEDS b c d (↑(n + 1) : ℤ) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑(n + 1 + 1 + 1) : ℤ)) 3 *
        if Even n then 1 else b
⊢ preNormEDS b c d (2 * (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 + 2) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1)) 3 *
        if Even n then b else 1) -
      preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 + 1)) 3 *
        if Even n then 1 else b

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

Tactic:
simpa only [preNormEDS_ofNat] using preNormEDS'_odd ..

Premises used: preNormEDS_ofNat, preNormEDS'_odd
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
m : ℕ
neg :
  preNormEDS b c d (HMul.hMul (α := ℤ) 2 (-(↑0 : ℤ)) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (-(↑0 : ℤ))) 3 *
        if Even (α := ℤ) (-(↑0 : ℤ)) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑0 : ℤ)) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1)) 3 *
        if Even (α := ℤ) (-(↑0 : ℤ)) then 1 else b
neg₁ :
  ∀ (m : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (-(↑(m + 1) : ℤ)) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 2) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (-(↑(m + 1) : ℤ))) 3 *
          if Even (α := ℤ) (-(↑(m + 1) : ℤ)) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑(m + 1) : ℤ)) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1)) 3 *
          if Even (α := ℤ) (-(↑(m + 1) : ℤ)) then 1 else b
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (-(↑m : ℤ)) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (-(↑m : ℤ))) 3 *
        if Even (α := ℤ) (-(↑m : ℤ)) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) 3 *
        if Even (α := ℤ) (-(↑m : ℤ)) then 1 else b

Tactic:
rcases m with _ | m
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (-(↑0 : ℤ)) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (-(↑0 : ℤ))) 3 *
        if Even (α := ℤ) (-(↑0 : ℤ)) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑0 : ℤ)) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑0 : ℤ)) 1)) 3 *
        if Even (α := ℤ) (-(↑0 : ℤ)) then 1 else b

Tactic:
simp
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
m : ℕ
⊢ 2 * -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1 = -(HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 1)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
m : ℕ
⊢ -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 2 = -HSub.hSub (α := ℤ) (↑m : ℤ) 1

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
m : ℕ
⊢ -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - 1 = -HAdd.hAdd (α := ℤ) (↑m : ℤ) 2

Tactic:
rfl
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
m : ℕ
⊢ -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1 = -(↑m : ℤ)

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
m : ℕ
neg :
  -((preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑m : ℤ)) 3 *
          if Even (α := ℤ) (↑m : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑m : ℤ) then 1 else b) =
    (-preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1) *
          HPow.hPow (β := ℕ) (-preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 3 *
        if Even (α := ℤ) (↑m : ℤ) then 1 else b) -
      -preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) * HPow.hPow (β := ℕ) (-preNormEDS b c d (↑m : ℤ)) 3 *
        if Even (α := ℤ) (↑m : ℤ) then b else 1
⊢ preNormEDS b c d (HMul.hMul (α := ℤ) 2 (-(↑(m + 1) : ℤ)) + 1) =
    (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 2) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (-(↑(m + 1) : ℤ))) 3 *
        if Even (α := ℤ) (-(↑(m + 1) : ℤ)) then b else 1) -
      preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑(m + 1) : ℤ)) 1) *
          HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑(m + 1) : ℤ)) 1)) 3 *
        if Even (α := ℤ) (-(↑(m + 1) : ℤ)) then 1 else b

Tactic:
simp_rw [Nat.cast_succ, show 2 * -(m + 1 : ℤ) + 1 = -(2 * m + 1) by rfl,
      show -(m + 1 : ℤ) + 2 = -(m - 1) by ring1, show -(m + 1 : ℤ) - 1 = -(m + 2) by rfl,
      show -(m + 1 : ℤ) + 1 = -m by ring1, preNormEDS_neg, even_neg, Int.even_add_one, ite_not, ih]

Premises used: Nat.cast_succ, preNormEDS_neg, ite_not, even_neg, Int.even_add_one
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑n : ℤ) then 1 else b
m : ℕ
⊢ -((preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑m : ℤ)) 3 *
          if Even (α := ℤ) (↑m : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑m : ℤ) then 1 else b) =
    (-preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1) *
          HPow.hPow (β := ℕ) (-preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 3 *
        if Even (α := ℤ) (↑m : ℤ) then 1 else b) -
      -preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) * HPow.hPow (β := ℕ) (-preNormEDS b c d (↑m : ℤ)) 3 *
        if Even (α := ℤ) (↑m : ℤ) then b else 1

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
nat :
  ∀ (m : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑m : ℤ)) 3 *
          if Even (α := ℤ) (↑m : ℤ) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (↑m : ℤ) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1)) 3 *
          if Even (α := ℤ) (↑m : ℤ) then 1 else b
neg :
  ∀
    (ih :
      ∀ (n : ℕ),
        preNormEDS b c d (HMul.hMul (α := ℤ) 2 (↑n : ℤ) + 1) =
          (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (↑n : ℤ)) 3 *
              if Even (α := ℤ) (↑n : ℤ) then b else 1) -
            preNormEDS b c d (HSub.hSub (α := ℤ) (↑n : ℤ) 1) *
                HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) 3 *
              if Even (α := ℤ) (↑n : ℤ) then 1 else b)
    (m : ℕ),
    preNormEDS b c d (HMul.hMul (α := ℤ) 2 (-(↑m : ℤ)) + 1) =
      (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 2) * HPow.hPow (β := ℕ) (preNormEDS b c d (-(↑m : ℤ))) 3 *
          if Even (α := ℤ) (-(↑m : ℤ)) then b else 1) -
        preNormEDS b c d (HSub.hSub (α := ℤ) (-(↑m : ℤ)) 1) *
            HPow.hPow (β := ℕ) (preNormEDS b c d (HAdd.hAdd (α := ℤ) (-(↑m : ℤ)) 1)) 3 *
          if Even (α := ℤ) (-(↑m : ℤ)) then 1 else b
⊢ preNormEDS b c d (2 * m + 1) =
    (preNormEDS b c d (m + 2) * HPow.hPow (β := ℕ) (preNormEDS b c d m) 3 * if Even m then b else 1) -
      preNormEDS b c d (m - 1) * HPow.hPow (β := ℕ) (preNormEDS b c d (m + 1)) 3 * if Even m then 1 else b

Tactic:
induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _ | _
    iterate 2 simp
    simp_rw [Nat.cast_succ, Int.add_sub_cancel, Int.even_add_one, not_not, Int.even_coe_nat]
    norm_cast
    simpa only [preNormEDS_ofNat] using preNormEDS'_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 : ℤ) + 2 = -(m - 1) by ring1, show -(m + 1 : ℤ) - 1 = -(m + 2) by rfl,
      show -(m + 1 : ℤ) + 1 = -m by ring1, preNormEDS_neg, even_neg, Int.even_add_one, ite_not, ih]
    ring1

Premises used: Nat.cast_succ, Classical.not_not, preNormEDS_ofNat, preNormEDS'_odd, preNormEDS_neg, Int.add_sub_cancel, ite_not, even_neg, Int.even_add_one, Int.even_coe_nat
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ complEDS₂ b c d 0 = 2

Tactic:
simp [complEDS₂, one_add_one_eq_two]

Premises used: one_add_one_eq_two, complEDS₂
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ complEDS₂ b c d 1 = b

Tactic:
simp [complEDS₂]

Premises used: complEDS₂
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ complEDS₂ b c d 2 = d

Tactic:
simp [complEDS₂]

Premises used: complEDS₂
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ ¬Even (α := ℤ) 3

Tactic:
decide
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ complEDS₂ b c d 3 = preNormEDS (HPow.hPow (β := ℕ) b 4) c d 5 * b - HPow.hPow (β := ℕ) d 2 * b

Tactic:
simp [complEDS₂, if_neg (by decide : ¬Even (3 : ℤ)), sub_mul]

Premises used: sub_mul, if_neg, complEDS₂
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ Even (α := ℤ) 4

Tactic:
decide
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ complEDS₂ b c d 4 =
    HPow.hPow (β := ℕ) c 2 * preNormEDS (HPow.hPow (β := ℕ) b 4) c d 6 -
      HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d 5) 2

Tactic:
simp [complEDS₂, if_pos (by decide : Even (4 : ℤ))]

Premises used: if_pos, complEDS₂
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
simp_rw :
  ((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) =
    (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
⊢ complEDS₂ b c d (-k) = complEDS₂ b c d k

Tactic:
simp_rw [complEDS₂, ← neg_add', ← sub_neg_eq_add, ← neg_sub', preNormEDS_neg, even_neg]

Premises used: preNormEDS_neg, neg_add', neg_sub', even_neg, sub_neg_eq_add, complEDS₂
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
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) *
      if Even k then 1 else b) =
    (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

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
rw :
  preNormEDS (HPow.hPow (β := ℕ) b 4) c d 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) *
        if Even k then 1 else b) =
    (HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2 *
            preNormEDS (HPow.hPow (β := ℕ) b 4) c d k *
          preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) * preNormEDS (HPow.hPow (β := ℕ) b 4) c d k *
          HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1)) 2) *
      if Even k then 1 else b
⊢ preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * complEDS₂ b c d k =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even k then 1 else b

Tactic:
rw [complEDS₂, preNormEDS_even]

Premises used: preNormEDS_even, complEDS₂
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
⊢ preNormEDS (HPow.hPow (β := ℕ) b 4) c d 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) *
        if Even k then 1 else b) =
    (HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 1)) 2 *
            preNormEDS (HPow.hPow (β := ℕ) b 4) c d k *
          preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 2) -
        preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k - 2) * preNormEDS (HPow.hPow (β := ℕ) b 4) c d k *
          HPow.hPow (β := ℕ) (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (k + 1)) 2) *
      if Even k then 1 else b

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

Tactic:
simp [normEDS]

Premises used: normEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ normEDS b c d 0 = 0

Tactic:
simp [normEDS]

Premises used: normEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ normEDS b c d 1 = 1

Tactic:
simp [normEDS]

Premises used: normEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ normEDS b c d 2 = b

Tactic:
simp [normEDS]

Premises used: normEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ normEDS b c d 3 = c

Tactic:
simp [normEDS, show ¬Even (3 : ℤ) by decide]

Premises used: normEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ ¬Odd (α := ℤ) 4

Tactic:
decide
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
⊢ normEDS b c d 4 = d * b

Tactic:
simp [normEDS, show ¬Odd (4 : ℤ) by decide]

Premises used: normEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℤ
simp_rw :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (-n) * if Even (-n) then b else 1) =
    -(preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1)
simp_rw₁ :
  (-preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even (-n) then b else 1) =
    -(preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1)
simp_rw₂ :
  (-preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1) =
    -(preNormEDS (HPow.hPow (β := ℕ) b 4) c d n * if Even n then b else 1)
⊢ normEDS b c d (-n) = -normEDS b c d n

Tactic:
simp_rw [normEDS, preNormEDS_neg, even_neg, neg_mul]

Premises used: preNormEDS_neg, normEDS, neg_mul, even_neg
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
simp_rw :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * if Even k then b else 1) * complEDS₂ b c d k =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₁ :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d k * complEDS₂ b c d k * if Even k then b else 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₂ :
  ((preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even k then 1 else b) * if Even k then b else 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₃ :
  preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * ((if Even k then 1 else b) * if Even k then b else 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₄ :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even k then 1 * b else b * 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₅ :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even k then b else b * 1) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₆ :
  (preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even k then b else b) =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
simp_rw₇ :
  preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * b =
    preNormEDS (HPow.hPow (β := ℕ) b 4) c d (2 * k) * if Even (2 * k) then b else 1
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)

Tactic:
simp_rw [normEDS, mul_right_comm, preNormEDS_mul_complEDS₂, mul_assoc, apply_ite₂, one_mul,
    mul_one, ite_self, if_pos <| even_two_mul k]

Premises used: apply_ite₂, ite_self, mul_assoc, normEDS, if_pos, even_two_mul, preNormEDS_mul_complEDS₂, mul_right_comm, mul_one, one_mul
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
⊢ normEDS b c d k ∣ normEDS b c d (2 * k)

Tactic:
⟨complEDS₂ .., (normEDS_mul_complEDS₂ ..).symm⟩

Premises used: Exists.intro, Eq.symm, normEDS_mul_complEDS₂, complEDS₂
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
simp_rw :
  ((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
⊢ complEDS₂ b c d k * b =
    HPow.hPow (β := ℕ) (normEDS b c d (k - 1)) 2 * normEDS b c d (k + 2) -
      normEDS b c d (k - 2) * HPow.hPow (β := ℕ) (normEDS b c d (k + 1)) 2

Tactic:
simp_rw [complEDS₂, normEDS, 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.even_add, Int.even_sub, complEDS₂