internlm/Lean-Github huggingface dataset:
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₄ : ∀ (x : ℕ), ↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I)) / ↑↑n
Tactic:
simp_rw [h₄]
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₄ : ∀ (x : ℕ), ↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₄ : ∀ (x : ℕ), ↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Tactic:
clear h₄
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Tactic:
have h₅ := RouGeometricSumEqIte n (↑k + m)
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Tactic:
have h₆ : ∀ (x : ℕ), (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I) = (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) := by
  intros x
  simp only [Int.cast_add, Int.cast_natCast]
  ring_nf
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) =
    (z ^ k / ↑k.factorial * ∑ x ∈ range ↑n, cexp (2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I)) / ↑↑n
Tactic:
simp_rw [h₆, h₅]
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (z ^ k / ↑k.factorial * if ↑↑n ∣ ↑k + m then ↑↑n else 0) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (z ^ k / ↑k.factorial * if ↑↑n ∣ ↑k + m then ↑↑n else 0) / ↑↑n
Tactic:
simp only [mul_ite, mul_zero]
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Tactic:
have hem := Classical.em (↑↑n ∣ ↑k + m)
Proof state after:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hem : ↑↑n ∣ ↑k + m ∨ ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hem : ↑↑n ∣ ↑k + m ∨ ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Tactic:
rcases hem with hemt | hemf
Proof state after:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n

case e_f.h.inr
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemf : ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ ∀ (k : ℕ),
    cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) =
      ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial
Tactic:
intros k
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
⊢ cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) = ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
⊢ cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) = ∑' (k_1 : ℕ), (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ k_1 / ↑k_1.factorial
Tactic:
exact ExpTsumForm (z * cexp (2 * ↑π * (↑k / ↑↑n) * I))
Proof state after:
no goals
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ ∀ x ∈ range ↑n,
    Summable fun x_1 =>
      (z * cexp (2 * ↑π * (↑x / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)
Tactic:
intros k _
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
a✝ : k ∈ range ↑n
⊢ Summable fun x_1 => (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑k / ↑↑n) * I)
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
a✝ : k ∈ range ↑n
⊢ Summable fun x_1 => (z * cexp (2 * ↑π * (↑k / ↑↑n) * I)) ^ x_1 / ↑x_1.factorial * cexp (↑m * 2 * ↑π * (↑k / ↑↑n) * I)
Tactic:
exact Summable.smul_const (ExpTaylorSeriesSummable (z * cexp (2 * ↑π * (↑k / ↑↑n) * I))) _
Proof state after:
no goals
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
⊢ ∀ (b x : ℕ),
    z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I) =
      z ^ b / ↑b.factorial * (cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I))
Tactic:
intros b x
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
b x : ℕ
⊢ z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I) =
    z ^ b / ↑b.factorial * (cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I))
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
b x : ℕ
⊢ z ^ b * cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) / ↑b.factorial * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I) =
    z ^ b / ↑b.factorial * (cexp (↑b * (2 * ↑π * (↑x / ↑↑n) * I)) * cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I))
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
⊢ ∀ (x : ℕ), ↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I
Tactic:
intros x
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
k x : ℕ
⊢ ↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
k x : ℕ
⊢ ↑k * (2 * ↑π * (↑x / ↑↑n) * I) + ↑m * 2 * ↑π * (↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
⊢ ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
Tactic:
intros x
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
x : ℕ
⊢ 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
x : ℕ
⊢ 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
Tactic:
simp only [Int.cast_add, Int.cast_natCast]
Proof state after:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
x : ℕ
⊢ 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n * I)
Theorem: RuesDiffEqualsExpSum
Proof state before:
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
x : ℕ
⊢ 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n * I)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Tactic:
simp_rw [if_pos hemt]
Proof state after:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ z ^ k / ↑k.factorial = z ^ k / ↑k.factorial * ↑↑n / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ z ^ k / ↑k.factorial = z ^ k / ↑k.factorial * ↑↑n / ↑↑n
Tactic:
ring_nf
Proof state after:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ z ^ k * (↑k.factorial)⁻¹ = z ^ k * (↑k.factorial)⁻¹ * ↑↑n * (↑↑n)⁻¹
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h.inl
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemt : ↑↑n ∣ ↑k + m
⊢ z ^ k * (↑k.factorial)⁻¹ = z ^ k * (↑k.factorial)⁻¹ * ↑↑n * (↑↑n)⁻¹
Tactic:
simp only [ne_eq, Nat.cast_eq_zero, PNat.ne_zero, not_false_eq_true, mul_inv_cancel_right₀]
Proof state after:
no goals
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h.inr
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemf : ¬↑↑n ∣ ↑k + m
⊢ (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial else 0) = (if ↑↑n ∣ ↑k + m then z ^ k / ↑k.factorial * ↑↑n else 0) / ↑↑n
Tactic:
simp_rw [if_neg hemf]
Proof state after:
case e_f.h.inr
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemf : ¬↑↑n ∣ ↑k + m
⊢ 0 = 0 / ↑↑n
Theorem: RuesDiffEqualsExpSum
Proof state before:
case e_f.h.inr
n : ℕ+
m : ℤ
z : ℂ
k : ℕ
h₅ : ∑ x ∈ range ↑n, cexp (2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)) = if ↑↑n ∣ ↑k + m then ↑↑n else 0
h₆ : ∀ (x : ℕ), 2 * ↑π * ((↑k + ↑m) * ↑x / ↑↑n) * I = 2 * ↑π * (↑(↑k + m) * ↑x / ↑↑n * I)
hemf : ¬↑↑n ∣ ↑k + m
⊢ 0 = 0 / ↑↑n
Tactic:
simp only [zero_div]
Proof state after:
no goals
Theorem: RuesNMthIteratedDeriv
Proof state before:
n m : ℕ+
⊢ iteratedDeriv (↑m) (Rues n) = RuesDiff n ↑↑m
Tactic:
rw [←RuesDiffM0EqualsRues, RuesDiffIteratedDeriv]
Proof state after:
n m : ℕ+
⊢ RuesDiff n (↑↑m + 0) = RuesDiff n ↑↑m
Theorem: RuesNMthIteratedDeriv
Proof state before:
n m : ℕ+
⊢ RuesDiff n (↑↑m + 0) = RuesDiff n ↑↑m
Tactic:
simp only [add_zero]
Proof state after:
no goals
Theorem: RuesDiffMod
Proof state before:
n : ℕ+
m : ℤ
⊢ RuesDiff n m = RuesDiff n (m % ↑↑n)
Tactic:
rw [RuesDiffMPeriodic n (m % n) (m / n)]
Proof state after:
n : ℕ+
m : ℤ
⊢ RuesDiff n m = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)
Theorem: RuesDiffMod
Proof state before:
n : ℕ+
m : ℤ
⊢ RuesDiff n m = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)
Tactic:
nth_rw 1 [←Int.ediv_add_emod' m n]
Proof state after:
n : ℕ+
m : ℤ
⊢ RuesDiff n (m / ↑↑n * ↑↑n + m % ↑↑n) = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)
Theorem: RuesDiffMod
Proof state before:
n : ℕ+
m : ℤ
⊢ RuesDiff n (m / ↑↑n * ↑↑n + m % ↑↑n) = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)
Tactic:
suffices h₀ : m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
Proof state after:
n : ℕ+
m : ℤ
h₀ : m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
⊢ RuesDiff n (m / ↑↑n * ↑↑n + m % ↑↑n) = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)

case h₀
n : ℕ+
m : ℤ
⊢ m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
Theorem: RuesDiffMod
Proof state before:
n : ℕ+
m : ℤ
h₀ : m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
⊢ RuesDiff n (m / ↑↑n * ↑↑n + m % ↑↑n) = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)

case h₀
n : ℕ+
m : ℤ
⊢ m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
Tactic:
exact congrArg (RuesDiff n) h₀
Proof state after:
case h₀
n : ℕ+
m : ℤ
⊢ m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
Theorem: RuesDiffMod
Proof state before:
case h₀
n : ℕ+
m : ℤ
⊢ m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ExpPiMulIHalf
Proof state before:
⊢ cexp (↑(π / 2) * I) = I
Tactic:
rw [exp_mul_I]
Proof state after:
⊢ (↑(π / 2)).cos + (↑(π / 2)).sin * I = I
Theorem: ExpPiMulIHalf
Proof state before:
⊢ (↑(π / 2)).cos + (↑(π / 2)).sin * I = I
Tactic:
simp only [ofReal_div, ofReal_ofNat, Complex.cos_pi_div_two, Complex.sin_pi_div_two, one_mul,
  zero_add]
Proof state after:
no goals
Theorem: ExpToNatPowersOfI
Proof state before:
k : ℕ
⊢ cexp (↑π * I * ↑k / 2) = I ^ k
Tactic:
induction' k with K Kih
Proof state after:
case zero

⊢ cexp (↑π * I * ↑0 / 2) = I ^ 0

case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * ↑(K + 1) / 2) = I ^ (K + 1)
Theorem: ExpToNatPowersOfI
Proof state before:
case zero

⊢ cexp (↑π * I * ↑0 / 2) = I ^ 0
Tactic:
simp only [Nat.zero_eq, CharP.cast_eq_zero, mul_zero, zero_div, Complex.exp_zero, pow_zero]
Proof state after:
no goals
Theorem: ExpToNatPowersOfI
Proof state before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * ↑(K + 1) / 2) = I ^ (K + 1)
Tactic:
simp_rw [Nat.cast_succ]
Proof state after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * (↑K + 1) / 2) = I ^ (K + 1)
Theorem: ExpToNatPowersOfI
Proof state before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * (↑K + 1) / 2) = I ^ (K + 1)
Tactic:
have h₀ : ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I := by
  simp only [ofReal_div, ofReal_ofNat]
  ring_nf
Proof state after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₀ : ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I
⊢ cexp (↑π * I * (↑K + 1) / 2) = I ^ (K + 1)
Theorem: ExpToNatPowersOfI
Proof state before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₀ : ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I
⊢ cexp (↑π * I * (↑K + 1) / 2) = I ^ (K + 1)
Tactic:
rw [h₀]
Proof state after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₀ : ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I
⊢ cexp (↑π * I * ↑K / 2 + ↑(π / 2) * I) = I ^ (K + 1)
Theorem: ExpToNatPowersOfI
Proof state before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₀ : ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I
⊢ cexp (↑π * I * ↑K / 2 + ↑(π / 2) * I) = I ^ (K + 1)
Tactic:
clear h₀
Proof state after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * ↑K / 2 + ↑(π / 2) * I) = I ^ (K + 1)
Theorem: ExpToNatPowersOfI
Proof state before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ cexp (↑π * I * ↑K / 2 + ↑(π / 2) * I) = I ^ (K + 1)
Tactic:
rw [Complex.exp_add, Kih, ExpPiMulIHalf]
Proof state after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ I ^ K * I = I ^ (K + 1)
Theorem: ExpToNatPowersOfI
Proof state before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ I ^ K * I = I ^ (K + 1)
Tactic:
have h₂ := zpow_add₀ I_ne_zero K 1
Proof state after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ ↑K * I ^ 1
⊢ I ^ K * I = I ^ (K + 1)
Theorem: ExpToNatPowersOfI
Proof state before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ ↑K * I ^ 1
⊢ I ^ K * I = I ^ (K + 1)
Tactic:
simp only [zpow_natCast, zpow_one] at h₂
Proof state after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ K * I
⊢ I ^ K * I = I ^ (K + 1)
Theorem: ExpToNatPowersOfI
Proof state before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ K * I
⊢ I ^ K * I = I ^ (K + 1)
Tactic:
rw [←h₂]
Proof state after:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ K * I
⊢ I ^ (↑K + 1) = I ^ (K + 1)
Theorem: ExpToNatPowersOfI
Proof state before:
case succ
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
h₂ : I ^ (↑K + 1) = I ^ K * I
⊢ I ^ (↑K + 1) = I ^ (K + 1)
Tactic:
exact rfl
Proof state after:
no goals
Theorem: ExpToNatPowersOfI
Proof state before:
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑(π / 2) * I
Tactic:
simp only [ofReal_div, ofReal_ofNat]
Proof state after:
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑π / 2 * I
Theorem: ExpToNatPowersOfI
Proof state before:
K : ℕ
Kih : cexp (↑π * I * ↑K / 2) = I ^ K
⊢ ↑π * I * (↑K + 1) / 2 = ↑π * I * ↑K / 2 + ↑π / 2 * I
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesNEqualsExpSum
Proof state before:
n : ℕ+
z : ℂ
⊢ Rues n z = (∑ m ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑m / ↑↑n) * I))) / ↑↑n
Tactic:
rw [←RuesDiffM0EqualsRues, RuesDiffEqualsExpSum]
Proof state after:
n : ℕ+
z : ℂ
⊢ (∑ k₀ ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k₀ / ↑↑n) * I)) / ↑↑n =
    (∑ m ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑m / ↑↑n) * I))) / ↑↑n
Theorem: RuesNEqualsExpSum
Proof state before:
n : ℕ+
z : ℂ
⊢ (∑ k₀ ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k₀ / ↑↑n) * I)) / ↑↑n =
    (∑ m ∈ range ↑n, cexp (z * cexp (2 * ↑π * (↑m / ↑↑n) * I))) / ↑↑n
Tactic:
congr
Proof state after:
case e_a.e_f
n : ℕ+
z : ℂ
⊢ (fun k₀ => cexp (z * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k₀ / ↑↑n) * I)) = fun m =>
    cexp (z * cexp (2 * ↑π * (↑m / ↑↑n) * I))
Theorem: RuesNEqualsExpSum
Proof state before:
case e_a.e_f
n : ℕ+
z : ℂ
⊢ (fun k₀ => cexp (z * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k₀ / ↑↑n) * I)) = fun m =>
    cexp (z * cexp (2 * ↑π * (↑m / ↑↑n) * I))
Tactic:
ext1 k
Proof state after:
case e_a.e_f.h
n : ℕ+
z : ℂ
k : ℕ
⊢ cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k / ↑↑n) * I) = cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I))
Theorem: RuesNEqualsExpSum
Proof state before:
case e_a.e_f.h
n : ℕ+
z : ℂ
k : ℕ
⊢ cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I) + ↑0 * 2 * ↑π * (↑k / ↑↑n) * I) = cexp (z * cexp (2 * ↑π * (↑k / ↑↑n) * I))
Tactic:
simp only [Int.cast_zero, zero_mul, add_zero]
Proof state after:
no goals
Theorem: RuesZ0Equals1
Proof state before:
n : ℕ+
⊢ Rues n 0 = 1
Tactic:
rw [RuesNEqualsExpSum]
Proof state after:
n : ℕ+
⊢ (∑ m ∈ range ↑n, cexp (0 * cexp (2 * ↑π * (↑m / ↑↑n) * I))) / ↑↑n = 1
Theorem: RuesZ0Equals1
Proof state before:
n : ℕ+
⊢ (∑ m ∈ range ↑n, cexp (0 * cexp (2 * ↑π * (↑m / ↑↑n) * I))) / ↑↑n = 1
Tactic:
simp only [zero_mul, Complex.exp_zero, sum_const, card_range, nsmul_eq_mul, mul_one, ne_eq,
  Nat.cast_eq_zero, PNat.ne_zero, not_false_eq_true, div_self]
Proof state after:
no goals
Theorem: RuesN1EqualsExp
Proof state before:
⊢ Rues 1 = cexp
Tactic:
ext1 z
Proof state after:
case h
z : ℂ
⊢ Rues 1 z = cexp z
Theorem: RuesN1EqualsExp
Proof state before:
case h
z : ℂ
⊢ Rues 1 z = cexp z
Tactic:
rw [Rues, ExpTsumForm]
Proof state after:
case h
z : ℂ
⊢ ∑' (k : ℕ), z ^ (↑1 * k) / ↑(↑1 * k).factorial = ∑' (k : ℕ), z ^ k / ↑k.factorial
Theorem: RuesN1EqualsExp
Proof state before:
case h
z : ℂ
⊢ ∑' (k : ℕ), z ^ (↑1 * k) / ↑(↑1 * k).factorial = ∑' (k : ℕ), z ^ k / ↑k.factorial
Tactic:
simp only [PNat.one_coe, one_mul]
Proof state after:
no goals
Theorem: RuesN2EqualsCosh
Proof state before:
⊢ Rues 2 = Complex.cosh
Tactic:
ext1 z
Proof state after:
case h
z : ℂ
⊢ Rues 2 z = z.cosh
Theorem: RuesN2EqualsCosh
Proof state before:
case h
z : ℂ
⊢ Rues 2 z = z.cosh
Tactic:
rw [RuesNEqualsExpSum, Complex.cosh]
Proof state after:
case h
z : ℂ
⊢ (∑ m ∈ range ↑2, cexp (z * cexp (2 * ↑π * (↑m / ↑↑2) * I))) / ↑↑2 = (cexp z + cexp (-z)) / 2
Theorem: RuesN2EqualsCosh
Proof state before:
case h
z : ℂ
⊢ (∑ m ∈ range ↑2, cexp (z * cexp (2 * ↑π * (↑m / ↑↑2) * I))) / ↑↑2 = (cexp z + cexp (-z)) / 2
Tactic:
have h₀ : range (2 : ℕ+) = {0, 1} := by
  rfl
Proof state after:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ (∑ m ∈ range ↑2, cexp (z * cexp (2 * ↑π * (↑m / ↑↑2) * I))) / ↑↑2 = (cexp z + cexp (-z)) / 2
Theorem: RuesN2EqualsCosh
Proof state before:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ (∑ m ∈ range ↑2, cexp (z * cexp (2 * ↑π * (↑m / ↑↑2) * I))) / ↑↑2 = (cexp z + cexp (-z)) / 2
Tactic:
simp_rw [h₀, Finset.sum]
Proof state after:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ (Multiset.map (fun x => cexp (z * cexp (2 * ↑π * (↑x / ↑↑2) * I))) {0, 1}.val).sum / ↑↑2 = (cexp z + cexp (-z)) / 2
Theorem: RuesN2EqualsCosh
Proof state before:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ (Multiset.map (fun x => cexp (z * cexp (2 * ↑π * (↑x / ↑↑2) * I))) {0, 1}.val).sum / ↑↑2 = (cexp z + cexp (-z)) / 2
Tactic:
simp only [mem_singleton, insert_val, singleton_val, Multiset.mem_singleton, not_false_eq_true,
  Multiset.ndinsert_of_not_mem, Multiset.map_cons, CharP.cast_eq_zero, zero_div, mul_zero,
  zero_mul, Complex.exp_zero, mul_one, Multiset.map_singleton, Nat.cast_one, one_div,
  Multiset.sum_cons, Multiset.sum_singleton]
Proof state after:
case h
z : ℂ
h₀ : range ↑2 = {0, 1}
⊢ (cexp z + cexp (z * cexp (2 * ↑π * (↑↑2)⁻¹ * I))) / ↑↑2 = (cexp z + cexp (-z)) / 2