awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
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
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ normEDS b c d k * complEDS₂ b c d k = normEDS b c d (2 * k)
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
k : ℤ
⊢ 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
have 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
Tactic: simp_rw [complEDS₂, normEDS, Int.even_add, Int.even_sub, even_two, iff_true, Int.not_even_one,
    iff_false]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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) *
      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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ ((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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
⊢ 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
have 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
Tactic: rw [← normEDS_mul_complEDS₂, mul_assoc, complEDS₂_mul_b]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℤ
⊢ ((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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ ((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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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 (2 * (x + 3))
have a : P (x + 1)
Tactic: apply even
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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)
⊢ P (2 * (x + 3))
have a₁ : P (x + 2)
Tactic: apply even
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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)
⊢ P (2 * (x + 3))
have a₂ : P (x + 3)
Tactic: apply even
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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)
⊢ P (2 * (x + 3))
have a₃ : P (x + 4)
Tactic: apply even
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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)
⊢ P (2 * (x + 3))
have a₄ : P (x + 5)
Tactic: apply even
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
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
⊢ x + 1 < 2 * (x + 3)
have linarith : 2 * (x + 3) ≤ x + 1 →
  HMul.hMul (α := ℤ) 5 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 1) =
    0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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
⊢ x + 1 < 2 * (x + 3)
have linarith₁ : 2 * (x + 3) ≤ x + 1 → GT.gt (α := ℤ) 5 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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
⊢ x + 2 < 2 * (x + 3)
have linarith : 2 * (x + 3) ≤ x + 2 →
  HMul.hMul (α := ℤ) 4 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 2) =
    0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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
⊢ x + 2 < 2 * (x + 3)
have linarith₁ : 2 * (x + 3) ≤ x + 2 → GT.gt (α := ℤ) 4 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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
⊢ x + 3 < 2 * (x + 3)
have linarith : 2 * (x + 3) ≤ x + 3 →
  HMul.hMul (α := ℤ) 3 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 3) =
    0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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
⊢ x + 3 < 2 * (x + 3)
have linarith₁ : 2 * (x + 3) ≤ x + 3 → GT.gt (α := ℤ) 3 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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
⊢ x + 4 < 2 * (x + 3)
have linarith : 2 * (x + 3) ≤ x + 4 →
  HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑x : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 4) =
    0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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
⊢ x + 4 < 2 * (x + 3)
have linarith₁ : 2 * (x + 3) ≤ x + 4 → GT.gt (α := ℤ) 2 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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
⊢ x + 5 < 2 * (x + 3)
have linarith : 2 * (x + 3) ≤ x + 5 →
  -1 + HSub.hSub (α := ℤ) 0 (↑x : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑x : ℤ) 3 - HAdd.hAdd (α := ℤ) (↑x : ℤ) 5) = 0
Tactic: linarith only
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
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 (2 * (x + 2) + 1)
have a : P (x + 1)
Tactic: apply odd