internlm/Lean-Github huggingface dataset:
Theorem: RuesDiffMPeriodic
Proof state before:
n : ℕ+
m k : ℤ
⊢ RuesDiff n m = RuesDiff n (m + k * ↑↑n)
Tactic:
ext1 z
Proof state after:
case h
n : ℕ+
m k : ℤ
z : ℂ
⊢ RuesDiff n m z = RuesDiff n (m + k * ↑↑n) z
Theorem: RuesDiffMPeriodic
Proof state before:
case h
n : ℕ+
m k : ℤ
z : ℂ
⊢ RuesDiff n m z = RuesDiff n (m + k * ↑↑n) z
Tactic:
simp_rw [RuesDiff]
Proof state after:
case h
n : ℕ+
m k : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (k_1 : ℕ), if ↑↑n ∣ ↑k_1 + (m + k * ↑↑n) then z ^ k_1 / ↑k_1.factorial else 0
Theorem: RuesDiffMPeriodic
Proof state before:
case h
n : ℕ+
m k : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (k_1 : ℕ), if ↑↑n ∣ ↑k_1 + (m + k * ↑↑n) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
congr
Proof state after:
case h.e_f
n : ℕ+
m k : ℤ
z : ℂ
⊢ (fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = fun k_1 =>
    if ↑↑n ∣ ↑k_1 + (m + k * ↑↑n) then z ^ k_1 / ↑k_1.factorial else 0
Theorem: RuesDiffMPeriodic
Proof state before:
case h.e_f
n : ℕ+
m k : ℤ
z : ℂ
⊢ (fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = fun k_1 =>
    if ↑↑n ∣ ↑k_1 + (m + k * ↑↑n) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
ext1 K
Proof state after:
case h.e_f.h
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (if ↑↑n ∣ ↑K + m then z ^ K / ↑K.factorial else 0) = if ↑↑n ∣ ↑K + (m + k * ↑↑n) then z ^ K / ↑K.factorial else 0
Theorem: RuesDiffMPeriodic
Proof state before:
case h.e_f.h
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (if ↑↑n ∣ ↑K + m then z ^ K / ↑K.factorial else 0) = if ↑↑n ∣ ↑K + (m + k * ↑↑n) then z ^ K / ↑K.factorial else 0
Tactic:
congr 1
Proof state after:
case h.e_f.h.e_c
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (↑↑n ∣ ↑K + m) = (↑↑n ∣ ↑K + (m + k * ↑↑n))
Theorem: RuesDiffMPeriodic
Proof state before:
case h.e_f.h.e_c
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (↑↑n ∣ ↑K + m) = (↑↑n ∣ ↑K + (m + k * ↑↑n))
Tactic:
rw [Dvd.dvd.addMultiple (↑↑n) (↑K + m) k]
Proof state after:
case h.e_f.h.e_c
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (↑↑n ∣ ↑K + m + k * ↑↑n) = (↑↑n ∣ ↑K + (m + k * ↑↑n))
Theorem: RuesDiffMPeriodic
Proof state before:
case h.e_f.h.e_c
n : ℕ+
m k : ℤ
z : ℂ
K : ℕ
⊢ (↑↑n ∣ ↑K + m + k * ↑↑n) = (↑↑n ∣ ↑K + (m + k * ↑↑n))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
⊢ RuesDiff n m z = ∑ k₀ ∈ range ↑k, RuesDiff (n * k) (↑↑n * ↑k₀ + m) z
Tactic:
simp_rw [RuesDiff]
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑ x ∈ range ↑k, ∑' (k_1 : ℕ), if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑ x ∈ range ↑k, ∑' (k_1 : ℕ), if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
have h₀ : ∀ x ∈ range k, Summable (λ (k_1 : ℕ) => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0) := by
  intros x _
  exact RuesDiffSummable (n * k) _ z
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
h₀ : ∀ x ∈ range ↑k, Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑ x ∈ range ↑k, ∑' (k_1 : ℕ), if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
h₀ : ∀ x ∈ range ↑k, Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑ x ∈ range ↑k, ∑' (k_1 : ℕ), if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
rw [← tsum_sum h₀]
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
h₀ : ∀ x ∈ range ↑k, Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (b : ℕ), ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
h₀ : ∀ x ∈ range ↑k, Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (b : ℕ), ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0
Tactic:
clear h₀
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (b : ℕ), ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
⊢ (∑' (k : ℕ), if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    ∑' (b : ℕ), ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0
Tactic:
congr
Proof state after:
case e_f
n k : ℕ+
m : ℤ
z : ℂ
⊢ (fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = fun b =>
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f
n k : ℕ+
m : ℤ
z : ℂ
⊢ (fun k => if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = fun b =>
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑b + (↑↑n * ↑i + m) then z ^ b / ↑b.factorial else 0
Tactic:
ext1 x
Proof state after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
let f₀ : ℕ → Prop := (λ (i : ℕ) => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m))
Proof state after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
have h₁ : ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j := by
  intros i hir j hjr hi hj
  simp [f₀] at hi hj
  simp only [mem_range] at hir hjr
  clear f₀ z
  rw [←Int.modEq_zero_iff_dvd] at hi hj
  have h₀ := Int.ModEq.sub hi hj
  simp only [add_sub_add_left_eq_sub, add_sub_add_right_eq_sub, sub_self] at h₀
  clear hi hj
  rw [Int.modEq_zero_iff_dvd, (show (↑↑n * ↑i - ↑↑n * ↑j : ℤ) = ↑↑n * (↑i - ↑j) by ring)] at h₀
  have h₁ : (n : ℤ) ≠ 0 := by
    exact Ne.symm (NeZero.ne' (n : ℤ))
  have h₂ : (k : ℤ) ∣ ↑i - ↑j := by exact (mul_dvd_mul_iff_left h₁).mp h₀
  obtain ⟨y, h₃⟩ := h₂
  have h₄ : k * y < k := by
    linarith
  have h₅ : -k < k * y := by
    linarith
  have h₆ : (k : ℤ) > 0 := by
    linarith
  have h₇ : y < 1 := by
    exact (mul_lt_iff_lt_one_right h₆).mp h₄
  nth_rw 1 [(show -(k : ℤ) = ↑↑k * -1 by ring)] at h₅
  have h₈ : -1 < y := by
    exact (mul_lt_mul_left h₆).mp h₅
  have h₉ : y = 0 := by
    linarith
  rw [h₉] at h₃
  simp only [mul_zero] at h₃
  clear n hir hjr m h₀ h₁ h₄ h₅ h₆ h₇ h₈ h₉ y x k
  refine Int.ofNat_inj.mp ?intro.a
  have h₀ := congrArg (λ (k : ℤ) => k + j) h₃
  simp only [sub_add_cancel, zero_add] at h₀
  exact h₀
Proof state after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₁ : ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₁ : ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
have h₂ := Finset.sum_ite_zero (range ↑k) f₀ h₁ (z ^ x / ↑x.factorial)
Proof state after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₁ : ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j
h₂ :
  (∑ i ∈ range ↑k, if f₀ i then z ^ x / ↑x.factorial else 0) = if ∃ i ∈ range ↑k, f₀ i then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₁ : ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j
h₂ :
  (∑ i ∈ range ↑k, if f₀ i then z ^ x / ↑x.factorial else 0) = if ∃ i ∈ range ↑k, f₀ i then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
clear h₁
Proof state after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ i ∈ range ↑k, if f₀ i then z ^ x / ↑x.factorial else 0) = if ∃ i ∈ range ↑k, f₀ i then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ i ∈ range ↑k, if f₀ i then z ^ x / ↑x.factorial else 0) = if ∃ i ∈ range ↑k, f₀ i then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ i ∈ range ↑k, if ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
simp only [PNat.mul_coe, Nat.cast_mul, mem_range, f₀] at h₂ ⊢
Proof state after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    ∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0
Tactic:
rw [h₂]
Proof state after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
h₂ :
  (∑ x_1 ∈ range ↑k, if ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑x_1 + m) then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
clear h₂ f₀
Proof state after:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (if ↑↑n ∣ ↑x + m then z ^ x / ↑x.factorial else 0) =
    if ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m) then z ^ x / ↑x.factorial else 0
Tactic:
congr
Proof state after:
case e_f.h.e_c
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (↑↑n ∣ ↑x + m) = ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (↑↑n ∣ ↑x + m) = ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
rw [←iff_eq_eq]
Proof state after:
case e_f.h.e_c
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ ↑↑n ∣ ↑x + m ↔ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ ↑↑n ∣ ↑x + m ↔ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
constructor
Proof state after:
case e_f.h.e_c.mp
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ ↑↑n ∣ ↑x + m → ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)

case e_f.h.e_c.mpr
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)) → ↑↑n ∣ ↑x + m
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
⊢ ∀ x ∈ range ↑k, Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
intros x _
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
a✝ : x ∈ range ↑k
⊢ Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
a✝ : x ∈ range ↑k
⊢ Summable fun k_1 => if ↑↑(n * k) ∣ ↑k_1 + (↑↑n * ↑x + m) then z ^ k_1 / ↑k_1.factorial else 0
Tactic:
exact RuesDiffSummable (n * k) _ z
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
⊢ ∀ i ∈ range ↑k, ∀ j ∈ range ↑k, f₀ i → f₀ j → i = j
Tactic:
intros i hir j hjr hi hj
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i : ℕ
hir : i ∈ range ↑k
j : ℕ
hjr : j ∈ range ↑k
hi : f₀ i
hj : f₀ j
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i : ℕ
hir : i ∈ range ↑k
j : ℕ
hjr : j ∈ range ↑k
hi : f₀ i
hj : f₀ j
⊢ i = j
Tactic:
simp [f₀] at hi hj
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i : ℕ
hir : i ∈ range ↑k
j : ℕ
hjr : j ∈ range ↑k
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i : ℕ
hir : i ∈ range ↑k
j : ℕ
hjr : j ∈ range ↑k
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
⊢ i = j
Tactic:
simp only [mem_range] at hir hjr
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i j : ℕ
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
hir : i < ↑k
hjr : j < ↑k
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
f₀ : ℕ → Prop := fun i => ↑↑(n * k) ∣ ↑x + (↑↑n * ↑i + m)
i j : ℕ
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
hir : i < ↑k
hjr : j < ↑k
⊢ i = j
Tactic:
clear f₀ z
Proof state after:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
hir : i < ↑k
hjr : j < ↑k
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
hj : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑j + m)
hir : i < ↑k
hjr : j < ↑k
⊢ i = j
Tactic:
rw [←Int.modEq_zero_iff_dvd] at hi hj
Proof state after:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
⊢ i = j
Tactic:
have h₀ := Int.ModEq.sub hi hj
Proof state after:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑x + (↑↑n * ↑i + m) - (↑x + (↑↑n * ↑j + m)) ≡ 0 - 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑x + (↑↑n * ↑i + m) - (↑x + (↑↑n * ↑j + m)) ≡ 0 - 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j
Tactic:
simp only [add_sub_add_left_eq_sub, add_sub_add_right_eq_sub, sub_self] at h₀
Proof state after:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑i - ↑↑n * ↑j ≡ 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
x i j : ℕ
hi : ↑x + (↑↑n * ↑i + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hj : ↑x + (↑↑n * ↑j + m) ≡ 0 [ZMOD ↑↑n * ↑↑k]
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑i - ↑↑n * ↑j ≡ 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j
Tactic:
clear hi hj
Proof state after:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑i - ↑↑n * ↑j ≡ 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑i - ↑↑n * ↑j ≡ 0 [ZMOD ↑↑n * ↑↑k]
⊢ i = j
Tactic:
rw [Int.modEq_zero_iff_dvd, (show (↑↑n * ↑i - ↑↑n * ↑j : ℤ) = ↑↑n * (↑i - ↑j) by ring)] at h₀
Proof state after:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
⊢ i = j
Tactic:
have h₁ : (n : ℤ) ≠ 0 := by
  exact Ne.symm (NeZero.ne' (n : ℤ))
Proof state after:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
⊢ i = j
Tactic:
have h₂ : (k : ℤ) ∣ ↑i - ↑j := by exact (mul_dvd_mul_iff_left h₁).mp h₀
Proof state after:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
h₂ : ↑↑k ∣ ↑i - ↑j
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
h₂ : ↑↑k ∣ ↑i - ↑j
⊢ i = j
Tactic:
obtain ⟨y, h₃⟩ := h₂
Proof state after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
⊢ i = j
Tactic:
have h₄ : k * y < k := by
  linarith
Proof state after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
⊢ i = j
Tactic:
have h₅ : -k < k * y := by
  linarith
Proof state after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
⊢ i = j
Tactic:
have h₆ : (k : ℤ) > 0 := by
  linarith
Proof state after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
⊢ i = j
Tactic:
have h₇ : y < 1 := by
  exact (mul_lt_iff_lt_one_right h₆).mp h₄
Proof state after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ i = j
Tactic:
nth_rw 1 [(show -(k : ℤ) = ↑↑k * -1 by ring)] at h₅
Proof state after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ i = j
Tactic:
have h₈ : -1 < y := by
  exact (mul_lt_mul_left h₆).mp h₅
Proof state after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
⊢ i = j
Tactic:
have h₉ : y = 0 := by
  linarith
Proof state after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
⊢ i = j
Tactic:
rw [h₉] at h₃
Proof state after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * 0
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * 0
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
⊢ i = j
Tactic:
simp only [mul_zero] at h₃
Proof state after:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
h₃ : ↑i - ↑j = 0
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
h₁ : ↑↑n ≠ 0
y : ℤ
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
h₉ : y = 0
h₃ : ↑i - ↑j = 0
⊢ i = j
Tactic:
clear n hir hjr m h₀ h₁ h₄ h₅ h₆ h₇ h₈ h₉ y x k
Proof state after:
case intro
i j : ℕ
h₃ : ↑i - ↑j = 0
⊢ i = j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro
i j : ℕ
h₃ : ↑i - ↑j = 0
⊢ i = j
Tactic:
refine Int.ofNat_inj.mp ?intro.a
Proof state after:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
⊢ ↑i = ↑j