awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
linarith :
  2 * (m + 2) + 1 ≤ m + 3 →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) +
        (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 2 + 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 3) =
      0
linarith₁ : 2 * (m + 2) + 1 ≤ m + 3 → GT.gt (α := ℤ) 2 0
⊢ m + 3 < 2 * (m + 2) + 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
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)
odd 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) (β := ℕ)
            (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) =
    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)
⊢ 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) (β := ℕ) ((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:
rw [ih _ <| by 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
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)
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)
⊢ 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)

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]

Premises used: map_sub, apply_ite, preNormEDS'_odd, map_pow, map_mul, preNormEDS'_even, map_one, DFunLike.coe
-- 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
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)

Tactic:
simp [preNormEDS]

Premises used: preNormEDS
-- 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
n : ℤ
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (complEDS₂ b c d n) : S)
    (complEDS₂ ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) n : S)

Tactic:
simp [complEDS₂, apply_ite f]

Premises used: apply_ite, DFunLike.coe, complEDS₂
-- 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
n : ℤ
⊢ Eq.{v + 1} (α := S) ((f : (a : R) → S) (normEDS b c d n) : S)
    (normEDS ((f : (a : R) → S) b) ((f : (a : R) → S) c) ((f : (a : R) → S) d) n : S)

Tactic:
simp [normEDS, apply_ite f]

Premises used: apply_ite, normEDS, DFunLike.coe
-- 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
k : ℤ
⊢ 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:
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
k : ℤ
⊢ 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:
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
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)
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)
⊢ 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)

Tactic:
simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]

Premises used: map_sub, complEDS'_even, map_complEDS₂, complEDS'_odd, map_pow, map_mul, map_normEDS
-- 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
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)
linarith :
  2 * (m + 1) ≤ m + 1 →
    -1 + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) = 0
⊢ m + 1 < 2 * (m + 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
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)
even 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)
⊢ 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:
rw [ih _ <| by 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
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)
even 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)
⊢ 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:
repeat rw [ih _ <| by 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
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)
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)
⊢ 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)

Tactic:
simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]

Premises used: map_sub, complEDS'_even, map_complEDS₂, complEDS'_odd, map_pow, map_mul, map_normEDS
-- 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
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
linarith₁ : 2 * (m + 1) + 1 ≤ m + 1 → GT.gt (α := ℤ) 2 0
⊢ m + 1 < 2 * (m + 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
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 + 2 →
    -1 + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 2) = 0
⊢ m + 2 < 2 * (m + 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
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)
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)
even :
  ∀ (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)
odd :
  ∀ (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)
⊢ 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)

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]

Premises used: map_sub, complEDS'_even, map_complEDS₂, complEDS'_odd, map_pow, map_mul, map_normEDS
-- 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
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)

Tactic:
simp [complEDS]

Premises used: complEDS
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedDivisionRing F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
p : ℕ
hp : 1 < p
⊢ norm (E := F) ((f : (a : ℕ) → F) p : F) < 1

Tactic:
summable_geometric_iff_norm_lt_one.mp ?_

Premises used: Iff.mp, summable_geometric_iff_norm_lt_one
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedDivisionRing F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
p : ℕ
hp : 1 < p
refine : Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n
⊢ norm (E := F) ((f : (a : ℕ) → F) p : F) < 1

Tactic:
refine summable_geometric_iff_norm_lt_one.mp ?_

Premises used: Iff.mp, summable_geometric_iff_norm_lt_one
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedDivisionRing F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
p : ℕ
hp : 1 < p
simp_rw : Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ (f : (a : ℕ) → F) (p ^ n)
⊢ Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ HPow.hPow (α := F) ((f : (a : ℕ) → F) p : F) n

Tactic:
simp_rw [← map_pow]

Premises used: map_pow
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedDivisionRing F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
p : ℕ
hp : 1 < p
⊢ Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ (f : (a : ℕ) → F) (p ^ n)

Tactic:
hsum.comp_injective <| Nat.pow_right_injective hp

Premises used: Nat.pow_right_injective, Summable.comp_injective
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
F : Type u_1
inst : NormedDivisionRing F
inst_1 : CompleteSpace F
f : ℕ →* F
hsum : Summable (α := F) (⇑f : (a : ℕ) → F)
p : ℕ
hp : 1 < p
⊢ Summable.{u_1, 0} (α := F) fun (n : ℕ) ↦ (f : (a : ℕ) → F) (p ^ n)

Tactic:
exact hsum.comp_injective <| Nat.pow_right_injective hp

Premises used: Nat.pow_right_injective, Summable.comp_injective
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
⊢ T0Space R

Tactic:
MetricSpace.instT0Space

Premises used: MetricSpace.instT0Space
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
empty :
  (Summable (α := ℝ) fun (m : (↑{1} : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑{1} : Type)) ↦ f (↑m : ℕ)) (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
⊢ (Summable (α := ℝ) fun (m : (↑(factoredNumbers ∅) : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑(factoredNumbers ∅) : Type)) ↦ f (↑m : ℕ))
      (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))

Tactic:
rw [factoredNumbers_empty]

Premises used: Nat.factoredNumbers_empty
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
empty :
  (Summable (α := ℝ) fun (m : (↑{1} : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑{1} : Type)) ↦ f (↑m : ℕ)) 1
⊢ (Summable (α := ℝ) fun (m : (↑{1} : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑{1} : Type)) ↦ f (↑m : ℕ)) (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))

Tactic:
simp only [notMem_empty, IsEmpty.forall_iff, forall_const, filter_true_of_mem, prod_empty]

Premises used: Finset.prod_empty, Finset.filter_true_of_mem, Finset.notMem_empty, forall_const, IsEmpty.forall_iff
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
⊢ (Summable (α := ℝ) fun (m : (↑{1} : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑{1} : Type)) ↦ f (↑m : ℕ)) 1

Tactic:
⟨(Set.finite_singleton 1).summable (‖f ·‖), hf₁ ▸ hasSum_singleton 1 f⟩

Premises used: Norm.norm, Set.Finite.summable, Eq.rec, And.intro, OfNat.ofNat, Set.finite_singleton, hasSum_singleton
-- Module: Mathlib.NumberTheory.EulerProduct.Basic
Goal:
R : Type u_1
inst : NormedCommRing R
f : ℕ → R
inst_1 : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable (α := ℝ) fun (n : ℕ) ↦ ‖f (p ^ n)‖
⊢ (Summable (α := ℝ) fun (m : (↑{1} : Type)) ↦ ‖f (↑m : ℕ)‖) ∧
    HasSum.{u_1, 0} (α := R) (fun (m : (↑{1} : Type)) ↦ f (↑m : ℕ)) 1

Tactic:
exact ⟨(Set.finite_singleton 1).summable (‖f ·‖), hf₁ ▸ hasSum_singleton 1 f⟩