awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
rw :
  (have this := ⋯;
    HPow.hPow (β := ℕ) (complEDS' b c d k ((2 * m + 1) / 2 + 1)) 2 *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑((2 * m + 1) / 2 + 1) : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑((2 * m + 1) / 2 + 1) : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS' b c d k ((2 * m + 1) / 2 + 1 + 1)) 2 *
          normEDS b c d ((↑((2 * m + 1) / 2 + 1) : ℤ) * k + 1) *
        normEDS b c d ((↑((2 * m + 1) / 2 + 1) : ℤ) * k - 1)) =
    HPow.hPow (β := ℕ) (complEDS' b c d k (m + 1)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS' b c d k (m + 2)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1)
⊢ complEDS' b c d k (2 * (m + 1) + 1) =
    HPow.hPow (β := ℕ) (complEDS' b c d k (m + 1)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS' b c d k (m + 2)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1)

Tactic:
rw [show 2 * (m + 1) + 1 = 2 * m + 3 by rfl, complEDS', dif_neg m.not_even_two_mul_add_one]

Premises used: dif_neg, complEDS', Nat.not_even_two_mul_add_one
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
⊢ (have this := ⋯;
    HPow.hPow (β := ℕ) (complEDS' b c d k ((2 * m + 1) / 2 + 1)) 2 *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑((2 * m + 1) / 2 + 1) : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑((2 * m + 1) / 2 + 1) : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS' b c d k ((2 * m + 1) / 2 + 1 + 1)) 2 *
          normEDS b c d ((↑((2 * m + 1) / 2 + 1) : ℤ) * k + 1) *
        normEDS b c d ((↑((2 * m + 1) / 2 + 1) : ℤ) * k - 1)) =
    HPow.hPow (β := ℕ) (complEDS' b c d k (m + 1)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS' b c d k (m + 2)) 2 * normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1)

Tactic:
simp [Nat.mul_add_div two_pos, add_assoc]

Premises used: add_assoc, Nat.mul_add_div, two_pos
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
n : ℕ
pos : ∀ (hn : n = 0), complEDS b c d k (↑n : ℤ) = complEDS' b c d k n
neg : ∀ (hn : ¬n = 0), complEDS b c d k (↑n : ℤ) = complEDS' b c d k n
⊢ complEDS b c d k (↑n : ℤ) = complEDS' b c d k n

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : n = 0
⊢ complEDS b c d k (↑n : ℤ) = complEDS' b c d k n

Tactic:
simp [hn, complEDS]

Premises used: complEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : ¬n = 0
⊢ complEDS b c d k (↑n : ℤ) = complEDS' b c d k n

Tactic:
simp [complEDS, Int.sign_natCast_of_ne_zero hn]

Premises used: Int.sign_natCast_of_ne_zero, complEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
⊢ complEDS b c d k 0 = 0

Tactic:
simp [complEDS]

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

Tactic:
simp [complEDS]

Premises used: complEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k n : ℤ
⊢ complEDS b c d k (-n) = -complEDS b c d k n

Tactic:
simp [complEDS]

Premises used: complEDS
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
nat : complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) = complEDS b c d k (↑0 : ℤ) * complEDS₂ b c d ((↑0 : ℤ) * k)
nat₁ :
  ∀ (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑(n + 1) : ℤ)) =
      complEDS b c d k (↑(n + 1) : ℤ) * complEDS₂ b c d ((↑(n + 1) : ℤ) * k)
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑m : ℤ)) = complEDS b c d k (↑m : ℤ) * complEDS₂ b c d ((↑m : ℤ) * k)

Tactic:
rcases m with _ | _
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) = complEDS b c d k (↑0 : ℤ) * complEDS₂ b c d ((↑0 : ℤ) * k)

Tactic:
simp
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
n : ℕ
⊢ complEDS b c d k (↑(2 * (n + 1)) : ℤ) = complEDS b c d k (↑(n + 1) : ℤ) * complEDS₂ b c d ((↑(n + 1) : ℤ) * k)

Tactic:
simpa only [complEDS_ofNat] using complEDS'_even ..

Premises used: complEDS'_even, complEDS_ofNat
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k)
n : ℕ
neg : complEDS b c d k (-HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
neg₁ : -complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = -complEDS b c d k (↑n : ℤ) * complEDS₂ b c d (-(↑n : ℤ) * k)
neg₂ :
  -(complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k)) =
    -complEDS b c d k (↑n : ℤ) * complEDS₂ b c d (-(↑n : ℤ) * k)
neg₃ :
  -(complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k)) =
    -(complEDS b c d k (↑n : ℤ) * complEDS₂ b c d (-((↑n : ℤ) * k)))
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑n : ℤ))) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)

Tactic:
simp_rw [mul_neg, complEDS_neg, ih, neg_mul, complEDS₂_neg]

Premises used: complEDS₂_neg, neg_mul, complEDS_neg, mul_neg
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k m : ℤ
nat :
  ∀ (m : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑m : ℤ)) = complEDS b c d k (↑m : ℤ) * complEDS₂ b c d ((↑m : ℤ) * k)
neg :
  ∀
    (ih :
      ∀ (n : ℕ),
        complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑n : ℤ)) = complEDS b c d k (↑n : ℤ) * complEDS₂ b c d ((↑n : ℤ) * k))
    (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (-(↑n : ℤ))) = complEDS b c d k (-(↑n : ℤ)) * complEDS₂ b c d (-(↑n : ℤ) * k)
⊢ complEDS b c d k (2 * m) = complEDS b c d k m * complEDS₂ b c d (m * k)

Tactic:
induction m using Int.negInduction with
  | nat m =>
    rcases m with _ | _
    · simp
    norm_cast
    simpa only [complEDS_ofNat] using complEDS'_even ..
  | neg ih => simp_rw [mul_neg, complEDS_neg, ih, neg_mul, complEDS₂_neg]

Premises used: complEDS₂_neg, complEDS'_even, complEDS_ofNat, neg_mul, complEDS_neg, mul_neg
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
m : ℕ
nat :
  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)
nat₁ :
  ∀ (n : ℕ),
    complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑(n + 1) : ℤ) + 1) =
      HPow.hPow (β := ℕ) (complEDS b c d k (↑(n + 1) : ℤ)) 2 *
            normEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * k + 1) *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * k - 1) -
        HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)) 2 *
            normEDS b c d ((↑(n + 1) : ℤ) * k + 1) *
          normEDS b c d ((↑(n + 1) : ℤ) * 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)

Tactic:
rcases m with _ | _
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
⊢ 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:
simp
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
n : ℕ
nat :
  complEDS b c d k (↑(2 * (n + 1) + 1) : ℤ) =
    HPow.hPow (β := ℕ) (complEDS b c d k (↑(n + 1) : ℤ)) 2 * normEDS b c d ((↑(n + 1 + 1) : ℤ) * k + 1) *
        normEDS b c d ((↑(n + 1 + 1) : ℤ) * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (↑(n + 1 + 1) : ℤ)) 2 * normEDS b c d ((↑(n + 1) : ℤ) * k + 1) *
        normEDS b c d ((↑(n + 1) : ℤ) * k - 1)
⊢ complEDS b c d k (HMul.hMul (α := ℤ) 2 (↑(n + 1) : ℤ) + 1) =
    HPow.hPow (β := ℕ) (complEDS b c d k (↑(n + 1) : ℤ)) 2 *
          normEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * k + 1) *
        normEDS b c d (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1)) 2 *
          normEDS b c d ((↑(n + 1) : ℤ) * k + 1) *
        normEDS b c d ((↑(n + 1) : ℤ) * k - 1)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
n : ℕ
⊢ complEDS b c d k (↑(2 * (n + 1) + 1) : ℤ) =
    HPow.hPow (β := ℕ) (complEDS b c d k (↑(n + 1) : ℤ)) 2 * normEDS b c d ((↑(n + 1 + 1) : ℤ) * k + 1) *
        normEDS b c d ((↑(n + 1 + 1) : ℤ) * k - 1) -
      HPow.hPow (β := ℕ) (complEDS b c d k (↑(n + 1 + 1) : ℤ)) 2 * normEDS b c d ((↑(n + 1) : ℤ) * k + 1) *
        normEDS b c d ((↑(n + 1) : ℤ) * k - 1)

Tactic:
simpa only [complEDS_ofNat] using complEDS'_odd ..

Premises used: complEDS_ofNat, complEDS'_odd
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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)
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)
⊢ 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:
rcases m with _ | m
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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)
⊢ 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:
simp
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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 : ℕ
⊢ 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
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 : ℕ
⊢ -HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1 = -(↑m : ℤ)

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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 :
  -(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)
⊢ 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:
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]

Premises used: Nat.cast_succ, neg_add', neg_sub', neg_mul, complEDS_neg, normEDS_neg, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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 : ℕ
⊢ -(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:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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)
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)
⊢ 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)

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

Premises used: Nat.cast_succ, complEDS_ofNat, complEDS'_odd, neg_add', neg_sub', neg_mul, complEDS_neg, normEDS_neg, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
P : ℕ → Sort u
zero : P 0
one : P 1
even : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) → P k) → P (2 * (m + 1))
odd : (m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) + 1 → P k) → P (2 * (m + 1) + 1)
n : ℕ
h : (k : ℕ) → k < HMul.hMul (α := ℕ) 2 0 → P k
⊢ P (HMul.hMul (α := ℕ) 2 0)

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

Tactic:
exacts [one, odd _ h]
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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
linarith :
  2 * (x + 1) ≤ x + 1 →
    -1 + HSub.hSub (α := ℤ) 0 (↑x : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) = 0
⊢ x + 1 < 2 * (x + 1)

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

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

Tactic:
simp
-- 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
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d 1) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) 1 : S)

Tactic:
simp
-- 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
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d 2) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) 2 : S)

Tactic:
simp
-- 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
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d 3) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) 3 : S)

Tactic:
simp
-- 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
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d 4) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) 4 : S)

Tactic:
simp