internlm/Lean-Github huggingface dataset:
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
⊢ ↑i = ↑j
Tactic:
have h₀ := congrArg (λ (k : ℤ) => k + j) h₃
Proof state after:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
h₀ : (fun k => k + ↑j) (↑i - ↑j) = (fun k => k + ↑j) 0
⊢ ↑i = ↑j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
h₀ : (fun k => k + ↑j) (↑i - ↑j) = (fun k => k + ↑j) 0
⊢ ↑i = ↑j
Tactic:
simp only [sub_add_cancel, zero_add] at h₀
Proof state after:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
h₀ : ↑i = ↑j
⊢ ↑i = ↑j
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case intro.a
i j : ℕ
h₃ : ↑i - ↑j = 0
h₀ : ↑i = ↑j
⊢ ↑i = ↑j
Tactic:
exact h₀
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * ↑i - ↑↑n * ↑j
⊢ ↑↑n * ↑i - ↑↑n * ↑j = ↑↑n * (↑i - ↑j)
Tactic:
ring
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
x i j : ℕ
hir : i < ↑k
hjr : j < ↑k
h₀ : ↑↑n * ↑↑k ∣ ↑↑n * (↑i - ↑j)
⊢ ↑↑n ≠ 0
Tactic:
exact Ne.symm (NeZero.ne' (n : ℤ))
Proof state after:
no goals
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
⊢ ↑↑k ∣ ↑i - ↑j
Tactic:
exact (mul_dvd_mul_iff_left h₁).mp h₀
Proof state after:
no goals
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
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
⊢ ↑↑k * y < ↑↑k
Tactic:
linarith
Proof state after:
no goals
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
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
⊢ -↑↑k < ↑↑k * y
Tactic:
linarith
Proof state after:
no goals
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
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
⊢ ↑↑k > 0
Tactic:
linarith
Proof state after:
no goals
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
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
⊢ y < 1
Tactic:
exact (mul_lt_iff_lt_one_right h₆).mp h₄
Proof state after:
no goals
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
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : -↑↑k < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ -↑↑k = ↑↑k * -1
Tactic:
ring
Proof state after:
no goals
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
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
⊢ -1 < y
Tactic:
exact (mul_lt_mul_left h₆).mp h₅
Proof state after:
no goals
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
y : ℤ
h₃ : ↑i - ↑j = ↑↑k * y
h₄ : ↑↑k * y < ↑↑k
h₅ : ↑↑k * -1 < ↑↑k * y
h₆ : ↑↑k > 0
h₇ : y < 1
h₈ : -1 < y
⊢ y = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mp
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ ↑↑n ∣ ↑x + m → ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
intros h₀
Proof state after:
case e_f.h.e_c.mp
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
h₀ : ↑↑n ∣ ↑x + m
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mp
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
h₀ : ↑↑n ∣ ↑x + m
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
obtain ⟨w, h₁⟩ := h₀
Proof state after:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
have h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + (↑↑n * ↑i) := by
  intros i
  ring_nf
Proof state after:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
Tactic:
simp_rw [h₂, h₁]
Proof state after:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑i
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mp.intro
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑i
Tactic:
use ((-w) % k).toNat
Proof state after:
case h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ (-w % ↑↑k).toNat < ↑k ∧ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ (-w % ↑↑k).toNat < ↑k ∧ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat
Tactic:
constructor
Proof state after:
case h.left
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ (-w % ↑↑k).toNat < ↑k

case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
⊢ ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
Tactic:
intros i
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
i : ℕ
⊢ ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
i : ℕ
⊢ ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.left
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ (-w % ↑↑k).toNat < ↑k
Tactic:
refine (Int.toNat_lt' ?h.left.hn).mpr ?h.left.a
Proof state after:
case h.left.hn
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑k ≠ 0

case h.left.a
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ -w % ↑↑k < ↑↑k
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.left.hn
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑k ≠ 0
Tactic:
exact PNat.ne_zero k
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.left.a
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ -w % ↑↑k < ↑↑k
Tactic:
refine Int.emod_lt_of_pos (-w) ?h.left.a.H
Proof state after:
case h.left.a.H
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 < ↑↑k
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.left.a.H
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 < ↑↑k
Tactic:
refine Int.ofNat_pos.mpr ?h.left.a.H.a
Proof state after:
case h.left.a.H.a
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 < ↑k
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.left.a.H.a
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 < ↑k
Tactic:
exact PNat.pos k
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat
Tactic:
have h₃ : ↑(-w % ↑↑k).toNat = (-w % ↑↑k) := by
  refine Int.toNat_of_nonneg ?_
  refine Int.emod_nonneg (-w) ?_
  exact Ne.symm (NeZero.ne' (k : ℤ))
Proof state after:
case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
h₃ : ↑(-w % ↑↑k).toNat = -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
h₃ : ↑(-w % ↑↑k).toNat = -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * ↑(-w % ↑↑k).toNat
Tactic:
rw [h₃]
Proof state after:
case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
h₃ : ↑(-w % ↑↑k).toNat = -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.right
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
h₃ : ↑(-w % ↑↑k).toNat = -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Tactic:
clear h₁ h₂ h₃ m z x
Proof state after:
case h.right
n k : ℕ+
w : ℤ
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.right
n k : ℕ+
w : ℤ
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Tactic:
suffices h₀ : ↑↑k ∣ w + (-w % ↑↑k)
Proof state after:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)

case h₀
n k : ℕ+
w : ℤ
⊢ ↑↑k ∣ w + -w % ↑↑k
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑(-w % ↑↑k).toNat = -w % ↑↑k
Tactic:
refine Int.toNat_of_nonneg ?_
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 ≤ -w % ↑↑k
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ 0 ≤ -w % ↑↑k
Tactic:
refine Int.emod_nonneg (-w) ?_
Proof state after:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑↑k ≠ 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
w : ℤ
h₁ : ↑x + m = ↑↑n * w
h₂ : ∀ (i : ℕ), ↑x + (↑↑n * ↑i + m) = ↑x + m + ↑↑n * ↑i
⊢ ↑↑k ≠ 0
Tactic:
exact Ne.symm (NeZero.ne' (k : ℤ))
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Tactic:
have h₁ := mul_dvd_mul_left (n : ℤ) h₀
Proof state after:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
h₁ : ↑↑n * ↑↑k ∣ ↑↑n * (w + -w % ↑↑k)
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
h₁ : ↑↑n * ↑↑k ∣ ↑↑n * (w + -w % ↑↑k)
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Tactic:
ring_nf at *
Proof state after:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
h₁ : ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h.right
n k : ℕ+
w : ℤ
h₀ : ↑↑k ∣ w + -w % ↑↑k
h₁ : ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
⊢ ↑↑n * ↑↑k ∣ ↑↑n * w + ↑↑n * (-w % ↑↑k)
Tactic:
exact h₁
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h₀
n k : ℕ+
w : ℤ
⊢ ↑↑k ∣ w + -w % ↑↑k
Tactic:
refine Int.dvd_of_emod_eq_zero ?h₀.H
Proof state after:
case h₀.H
n k : ℕ+
w : ℤ
⊢ (w + -w % ↑↑k) % ↑↑k = 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h₀.H
n k : ℕ+
w : ℤ
⊢ (w + -w % ↑↑k) % ↑↑k = 0
Tactic:
have h₀ : (0 : ℤ) = 0 % k := by
  exact rfl
Proof state after:
case h₀.H
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ (w + -w % ↑↑k) % ↑↑k = 0
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h₀.H
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ (w + -w % ↑↑k) % ↑↑k = 0
Tactic:
rw [h₀]
Proof state after:
case h₀.H
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ (w + -w % ↑↑k) % ↑↑k = 0 % ↑↑k
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h₀.H
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ (w + -w % ↑↑k) % ↑↑k = 0 % ↑↑k
Tactic:
refine Eq.symm (Int.ModEq.eq ?h₀.H.a)
Proof state after:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Tactic:
have h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k] := by
  exact Int.mod_modEq (-w) ↑↑k
Proof state after:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Tactic:
have h₂ : w ≡ w [ZMOD ↑↑k] := by exact rfl
Proof state after:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Tactic:
have h₃ := Int.ModEq.add h₂ h₁
Proof state after:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
h₃ : w + -w % ↑↑k ≡ w + -w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
h₃ : w + -w % ↑↑k ≡ w + -w [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Tactic:
simp only [add_right_neg] at h₃
Proof state after:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
h₃ : w + -w % ↑↑k ≡ 0 [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case h₀.H.a
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
h₂ : w ≡ w [ZMOD ↑↑k]
h₃ : w + -w % ↑↑k ≡ 0 [ZMOD ↑↑k]
⊢ 0 ≡ w + -w % ↑↑k [ZMOD ↑↑k]
Tactic:
exact h₃.symm
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
w : ℤ
⊢ 0 = 0 % ↑↑k
Tactic:
exact rfl
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
⊢ -w % ↑↑k ≡ -w [ZMOD ↑↑k]
Tactic:
exact Int.mod_modEq (-w) ↑↑k
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
w : ℤ
h₀ : 0 = 0 % ↑↑k
h₁ : -w % ↑↑k ≡ -w [ZMOD ↑↑k]
⊢ w ≡ w [ZMOD ↑↑k]
Tactic:
exact rfl
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mpr
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
⊢ (∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)) → ↑↑n ∣ ↑x + m
Tactic:
intros h₀
Proof state after:
case e_f.h.e_c.mpr
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
h₀ : ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
⊢ ↑↑n ∣ ↑x + m
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mpr
n k : ℕ+
m : ℤ
z : ℂ
x : ℕ
h₀ : ∃ i < ↑k, ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑i + m)
⊢ ↑↑n ∣ ↑x + m
Tactic:
obtain ⟨w, _, h₂⟩ := h₀
Proof state after:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
⊢ ↑↑n ∣ ↑x + m
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
⊢ ↑↑n ∣ ↑x + m
Tactic:
have h₃ := dvd_of_mul_right_dvd h₂
Proof state after:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
⊢ ↑↑n ∣ ↑x + m
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
⊢ ↑↑n ∣ ↑x + m
Tactic:
have h₄ : (n : ℤ) ∣ ↑↑n * ↑w := by exact Int.dvd_mul_right (↑n) w
Proof state after:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
h₄ : ↑↑n ∣ ↑↑n * ↑w
⊢ ↑↑n ∣ ↑x + m
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
h₄ : ↑↑n ∣ ↑↑n * ↑w
⊢ ↑↑n ∣ ↑x + m
Tactic:
rw [(show ↑x + (↑↑n * ↑w + m) = ↑↑n * ↑w + ↑(x + m) by ring_nf)] at h₃
Proof state after:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑↑n * ↑w + (↑x + m)
h₄ : ↑↑n ∣ ↑↑n * ↑w
⊢ ↑↑n ∣ ↑x + m
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
case e_f.h.e_c.mpr.intro.intro
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑↑n * ↑w + (↑x + m)
h₄ : ↑↑n ∣ ↑↑n * ↑w
⊢ ↑↑n ∣ ↑x + m
Tactic:
exact (Int.dvd_iff_dvd_of_dvd_add h₃).mp h₄
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
⊢ ↑↑n ∣ ↑↑n * ↑w
Tactic:
exact Int.dvd_mul_right (↑n) w
Proof state after:
no goals
Theorem: RuesDiffSumOfRuesDiff
Proof state before:
n k : ℕ+
m : ℤ
z : ℂ
x w : ℕ
left✝ : w < ↑k
h₂ : ↑↑n * ↑↑k ∣ ↑x + (↑↑n * ↑w + m)
h₃ : ↑↑n ∣ ↑x + (↑↑n * ↑w + m)
h₄ : ↑↑n ∣ ↑↑n * ↑w
⊢ ↑x + (↑↑n * ↑w + m) = ↑↑n * ↑w + (↑x + m)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesDiffNthIteratedDeriv
Proof state before:
n : ℕ+
m : ℤ
⊢ iteratedDeriv (↑n) (RuesDiff n m) = RuesDiff n m
Tactic:
rw [RuesDiffIteratedDeriv, RuesDiffMPeriodic n m 1]
Proof state after:
n : ℕ+
m : ℤ
⊢ RuesDiff n (↑↑n + m) = RuesDiff n (m + 1 * ↑↑n)
Theorem: RuesDiffNthIteratedDeriv
Proof state before:
n : ℕ+
m : ℤ
⊢ RuesDiff n (↑↑n + m) = RuesDiff n (m + 1 * ↑↑n)
Tactic:
simp only [one_mul]
Proof state after:
n : ℕ+
m : ℤ
⊢ RuesDiff n (↑↑n + m) = RuesDiff n (m + ↑↑n)
Theorem: RuesDiffNthIteratedDeriv
Proof state before:
n : ℕ+
m : ℤ
⊢ RuesDiff n (↑↑n + m) = RuesDiff n (m + ↑↑n)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k * ↑x / ↑↑n * I)) = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
have h₀ : ∀ (x : ℕ), (2 * ↑π * (↑k * ↑x / ↑↑n * I)) = ↑x * (2 * ↑π * (↑k / ↑↑n * I)) := by
  intros x
  ring_nf
Proof state after:
n : ℕ+
k : ℤ
h₀ : ∀ (x : ℕ), 2 * ↑π * (↑k * ↑x / ↑↑n * I) = ↑x * (2 * ↑π * (↑k / ↑↑n * I))
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k * ↑x / ↑↑n * I)) = if ↑↑n ∣ k then ↑↑n else 0
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
h₀ : ∀ (x : ℕ), 2 * ↑π * (↑k * ↑x / ↑↑n * I) = ↑x * (2 * ↑π * (↑k / ↑↑n * I))
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k * ↑x / ↑↑n * I)) = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
simp_rw [h₀, Complex.exp_nat_mul]
Proof state after:
n : ℕ+
k : ℤ
h₀ : ∀ (x : ℕ), 2 * ↑π * (↑k * ↑x / ↑↑n * I) = ↑x * (2 * ↑π * (↑k / ↑↑n * I))
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
h₀ : ∀ (x : ℕ), 2 * ↑π * (↑k * ↑x / ↑↑n * I) = ↑x * (2 * ↑π * (↑k / ↑↑n * I))
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
clear h₀
Proof state after:
n : ℕ+
k : ℤ
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
have hem := Classical.em (↑↑n ∣ k)
Proof state after:
n : ℕ+
k : ℤ
hem : ↑↑n ∣ k ∨ ¬↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
hem : ↑↑n ∣ k ∨ ¬↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
have h₂ : (n : ℂ) ≠ 0 := by exact Ne.symm (NeZero.ne' (n : ℂ))
Proof state after:
n : ℕ+
k : ℤ
hem : ↑↑n ∣ k ∨ ¬↑↑n ∣ k
h₂ : ↑↑n ≠ 0
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
hem : ↑↑n ∣ k ∨ ¬↑↑n ∣ k
h₂ : ↑↑n ≠ 0
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
rcases hem with hemt | hemf
Proof state after:
case inl
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0

case inr
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemf : ¬↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
⊢ ∀ (x : ℕ), 2 * ↑π * (↑k * ↑x / ↑↑n * I) = ↑x * (2 * ↑π * (↑k / ↑↑n * I))
Tactic:
intros x
Proof state after:
n : ℕ+
k : ℤ
x : ℕ
⊢ 2 * ↑π * (↑k * ↑x / ↑↑n * I) = ↑x * (2 * ↑π * (↑k / ↑↑n * I))
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
x : ℕ
⊢ 2 * ↑π * (↑k * ↑x / ↑↑n * I) = ↑x * (2 * ↑π * (↑k / ↑↑n * I))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
hem : ↑↑n ∣ k ∨ ¬↑↑n ∣ k
⊢ ↑↑n ≠ 0
Tactic:
exact Ne.symm (NeZero.ne' (n : ℂ))
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
case inl
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
h₁ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = ∑ x ∈ range ↑n, 1
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = if ↑↑n ∣ k then ↑↑n else 0
Tactic:
rw [h₁, if_pos hemt]
Proof state after:
case inl
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
h₁ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = ∑ x ∈ range ↑n, 1
⊢ ∑ x ∈ range ↑n, 1 = ↑↑n
Theorem: RouGeometricSumEqIte
Proof state before:
case inl
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
h₁ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = ∑ x ∈ range ↑n, 1
⊢ ∑ x ∈ range ↑n, 1 = ↑↑n
Tactic:
simp only [sum_const, card_range, nsmul_eq_mul, mul_one]
Proof state after:
no goals
Theorem: RouGeometricSumEqIte
Proof state before:
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
⊢ ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = ∑ x ∈ range ↑n, 1
Tactic:
congr
Proof state after:
case e_f
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
⊢ (fun x => cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x) = fun x => 1
Theorem: RouGeometricSumEqIte
Proof state before:
case e_f
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
⊢ (fun x => cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x) = fun x => 1
Tactic:
ext1 x
Proof state after:
case e_f.h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
x : ℕ
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 1
Theorem: RouGeometricSumEqIte
Proof state before:
case e_f.h
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
hemt : ↑↑n ∣ k
x : ℕ
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 1
Tactic:
obtain ⟨k₂, kDiv⟩ := hemt
Proof state after:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 1
Theorem: RouGeometricSumEqIte
Proof state before:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑k / ↑↑n * I)) ^ x = 1
Tactic:
rw [kDiv]
Proof state after:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑(↑↑n * k₂) / ↑↑n * I)) ^ x = 1
Theorem: RouGeometricSumEqIte
Proof state before:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑(↑↑n * k₂) / ↑↑n * I)) ^ x = 1
Tactic:
field_simp
Proof state after:
case e_f.h.intro
n : ℕ+
k : ℤ
h₂ : ↑↑n ≠ 0
x : ℕ
k₂ : ℤ
kDiv : k = ↑↑n * k₂
⊢ cexp (2 * ↑π * (↑k₂ * I)) ^ x = 1