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
S : Type v
inst_1 : CommRing S
f : R →+* S
m : ℕ
ih :
  ∀ k < 2 * (m + 2) + 1,
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d k) : S)
      (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k : S)
⊢ HMul.hMul (β := S)
        (HMul.hMul (α := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 4)) : S)
          (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 2)) : S) 3))
        (if Even m then (f : (a : R) → S) b else 1 : S) -
      HMul.hMul (β := S)
        (HMul.hMul (α := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 1)) : S)
          (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S) 3))
        (if Even m then 1 else (f : (a : R) → S) b : S) =
    HMul.hMul (β := S)
        (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 3))
        (if Even m then (f : (a : R) → S) b else 1 : S) -
      HMul.hMul (β := S)
        (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
          (HPow.hPow (α := S) (β := ℕ)
            (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) 3))
        (if Even m then 1 else (f : (a : R) → S) b : S)
have odd : HMul.hMul (β := S)
      (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S)
        (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 2)) : S) 3))
      (if Even m then (f : (a : R) → S) b else 1 : S) -
    HMul.hMul (β := S)
      (HMul.hMul (α := S) ((f : (a : R) → S) (preNormEDS' b c d (m + 1)) : S)
        (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (preNormEDS' b c d (m + 3)) : S) 3))
      (if Even m then 1 else (f : (a : R) → S) b : S) =
  HMul.hMul (β := S)
      (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 4) : S)
        (HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 2) : S) 3))
      (if Even m then (f : (a : R) → S) b else 1 : S) -
    HMul.hMul (β := S)
      (HMul.hMul (α := S) (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 1) : S)
        (HPow.hPow (α := S) (β := ℕ)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (m + 3) : S) 3))
      (if Even m then 1 else (f : (a : R) → S) b : S)
Tactic: repeat rw [ih _ <| by linarith only]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
n : ℕ
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d n) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) n : S)
have zero : 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: induction n using normEDSRec' with
  | zero => simp
  | one => simp
  | two => simp
  | three => simp
  | four => simp
  | _ _ ih =>
    simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
n : ℕ
zero :
  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)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d n) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) n : S)
have one : 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: induction n using normEDSRec' with
  | zero => simp
  | one => simp
  | two => simp
  | three => simp
  | four => simp
  | _ _ ih =>
    simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
n : ℕ
zero :
  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)
one :
  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)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d n) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) n : S)
have two : 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: induction n using normEDSRec' with
  | zero => simp
  | one => simp
  | two => simp
  | three => simp
  | four => simp
  | _ _ ih =>
    simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
n : ℕ
zero :
  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)
one :
  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)
two :
  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)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d n) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) n : S)
have three : 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: induction n using normEDSRec' with
  | zero => simp
  | one => simp
  | two => simp
  | three => simp
  | four => simp
  | _ _ ih =>
    simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
n : ℕ
zero :
  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)
one :
  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)
two :
  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)
three :
  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)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d n) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) n : S)
have four : 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: induction n using normEDSRec' with
  | zero => simp
  | one => simp
  | two => simp
  | three => simp
  | four => simp
  | _ _ ih =>
    simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
n : ℕ
zero :
  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)
one :
  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)
two :
  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)
three :
  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)
four :
  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)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d n) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) n : S)
have even : ∀ (m : ℕ)
  (ih :
    ∀ k < 2 * (m + 3),
      Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d k) : S)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k : S)),
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d (2 * (m + 3))) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (2 * (m + 3)) : S)
Tactic: induction n using normEDSRec' with
  | zero => simp
  | one => simp
  | two => simp
  | three => simp
  | four => simp
  | _ _ ih =>
    simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
n : ℕ
zero :
  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)
one :
  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)
two :
  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)
three :
  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)
four :
  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)
even :
  ∀ (m : ℕ)
    (ih :
      ∀ k < 2 * (m + 3),
        Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d k) : S)
          (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k : S)),
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d (2 * (m + 3))) : S)
      (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (2 * (m + 3)) : S)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d n) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) n : S)
have odd : ∀ (m : ℕ)
  (ih :
    ∀ k < 2 * (m + 2) + 1,
      Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d k) : S)
        (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k : S)),
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (preNormEDS' b c d (2 * (m + 2) + 1)) : S)
    (preNormEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (2 * (m + 2) + 1) : S)
Tactic: induction n using normEDSRec' with
  | zero => simp
  | one => simp
  | two => simp
  | three => simp
  | four => simp
  | _ _ ih =>
    simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
m : ℕ
ih :
  ∀ k_1 < 2 * (m + 1),
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k (2 * (m + 1))) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (2 * (m + 1)) : S)
have even : HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (complEDS' b c d k (m + 1)) : S)
    (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) :
      S) =
  HMul.hMul (α := S) (β := S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S)
    (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) :
      S)
Tactic: simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
m : ℕ
ih :
  ∀ k_1 < 2 * (m + 1),
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)
⊢ m + 1 < 2 * (m + 1)
have linarith : 2 * (m + 1) ≤ m + 1 →
  -1 + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 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
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
m : ℕ
ih :
  ∀ k_1 < 2 * (m + 1),
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (complEDS' b c d k (m + 1)) : S)
      (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) :
        S) =
    HMul.hMul (α := S) (β := S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S)
      (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) :
        S)
have even : HMul.hMul (α := S) (β := S) (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S)
    (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) :
      S) =
  HMul.hMul (α := S) (β := S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S)
    (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) :
      S)
Tactic: rw [ih _ <| by linarith only]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
m : ℕ
ih :
  ∀ k_1 < 2 * (m + 1),
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (complEDS' b c d k (m + 1)) : S)
      (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) :
        S) =
    HMul.hMul (α := S) (β := S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S)
      (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) :
        S)
have even : HMul.hMul (α := S) (β := S) (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S)
    (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) :
      S) =
  HMul.hMul (α := S) (β := S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S)
    (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k) :
      S)
Tactic: repeat rw [ih _ <| by linarith only]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
m : ℕ
ih :
  ∀ k_1 < 2 * (m + 1) + 1,
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k (2 * (m + 1) + 1)) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (2 * (m + 1) + 1) : S)
have odd : HMul.hMul (β := S)
      (HMul.hMul (β := S) (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (complEDS' b c d k (m + 1)) : S) 2)
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) :
          S))
      (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
          (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) :
        S) -
    HMul.hMul (β := S)
      (HMul.hMul (β := S) (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) (complEDS' b c d k (m + 2)) : S) 2)
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) :
          S))
      (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
          (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) :
        S) =
  HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 1) : S) 2)
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k + 1) :
          S))
      (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
          (HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 * k - 1) :
        S) -
    HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HPow.hPow (α := S) (β := ℕ)
          (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k (m + 2) : S) 2)
        (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
            (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k + 1) :
          S))
      (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d)
          (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 * k - 1) :
        S)
Tactic: simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
m : ℕ
ih :
  ∀ k_1 < 2 * (m + 1) + 1,
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)
⊢ m + 1 < 2 * (m + 1) + 1
have linarith : 2 * (m + 1) + 1 ≤ m + 1 →
  HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
      (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 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
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
m : ℕ
ih :
  ∀ k_1 < 2 * (m + 1) + 1,
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)
linarith :
  2 * (m + 1) + 1 ≤ m + 1 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) =
      0
⊢ m + 1 < 2 * (m + 1) + 1
have linarith₁ : 2 * (m + 1) + 1 ≤ m + 1 → 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
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
m : ℕ
ih :
  ∀ k_1 < 2 * (m + 1) + 1,
    Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k k_1) : S)
      (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k k_1 : S)
⊢ m + 2 < 2 * (m + 1) + 1
have linarith : 2 * (m + 1) + 1 ≤ m + 2 →
  -1 + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 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
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
n : ℕ
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k n) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k n : S)
have zero : Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k 0) : S)
  (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k 0 : S)
Tactic: induction n using complEDSRec' with
  | zero => simp
  | one => simp
  | _ _ ih =>
    simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
S : Type v
inst_1 : CommRing S
f : R →+* S
k : ℤ
n : ℕ
zero :
  Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k 0) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k 0 : S)
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k n) : S)
    (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k n : S)
have one : Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS' b c d k 1) : S)
  (complEDS' ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) k 1 : S)
Tactic: induction n using complEDSRec' with
  | zero => simp
  | one => simp
  | _ _ ih =>
    simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]
    repeat rw [ih _ <| by linarith only]
Cleared hypotheses: n