internlm/Lean-Github huggingface dataset:
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ cexp (↑π * I * (3 / 2)) = -I
Tactic:
have h₁b := ExpToNatPowersOfI 3
Proof state after:
z : ℂ
h₁b : cexp (↑π * I * ↑3 / 2) = I ^ 3
⊢ cexp (↑π * I * (3 / 2)) = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₁b : cexp (↑π * I * ↑3 / 2) = I ^ 3
⊢ cexp (↑π * I * (3 / 2)) = -I
Tactic:
simp only [Nat.cast_ofNat] at h₁b
Proof state after:
z : ℂ
h₁b : cexp (↑π * I * 3 / 2) = I ^ 3
⊢ cexp (↑π * I * (3 / 2)) = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₁b : cexp (↑π * I * 3 / 2) = I ^ 3
⊢ cexp (↑π * I * (3 / 2)) = -I
Tactic:
have h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2) := by
  ring
Proof state after:
z : ℂ
h₁b : cexp (↑π * I * 3 / 2) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ cexp (↑π * I * (3 / 2)) = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₁b : cexp (↑π * I * 3 / 2) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ cexp (↑π * I * (3 / 2)) = -I
Tactic:
rw [h₁b₁] at h₁b
Proof state after:
z : ℂ
h₁b : cexp (↑π * I * (3 / 2)) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ cexp (↑π * I * (3 / 2)) = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₁b : cexp (↑π * I * (3 / 2)) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ cexp (↑π * I * (3 / 2)) = -I
Tactic:
rw [h₁b]
Proof state after:
z : ℂ
h₁b : cexp (↑π * I * (3 / 2)) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ I ^ 3 = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₁b : cexp (↑π * I * (3 / 2)) = I ^ 3
h₁b₁ : ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
⊢ I ^ 3 = -I
Tactic:
clear h₁b h₁b₁
Proof state after:
z : ℂ
⊢ I ^ 3 = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ I ^ 3 = -I
Tactic:
have h₅ : I ^ (3 : ℕ) = I ^ (3 : ℤ) := by
  exact rfl
Proof state after:
z : ℂ
h₅ : I ^ 3 = I ^ 3
⊢ I ^ 3 = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₅ : I ^ 3 = I ^ 3
⊢ I ^ 3 = -I
Tactic:
clear h₅
Proof state after:
z : ℂ
⊢ I ^ 3 = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ I ^ 3 = -I
Tactic:
have h₆ : (3 : ℤ) = 2 + 1 := by
  exact rfl
Proof state after:
z : ℂ
h₆ : 3 = 2 + 1
⊢ I ^ 3 = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₆ : 3 = 2 + 1
⊢ I ^ 3 = -I
Tactic:
rw [h₆]
Proof state after:
z : ℂ
h₆ : 3 = 2 + 1
⊢ I ^ (2 + 1) = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₆ : 3 = 2 + 1
⊢ I ^ (2 + 1) = -I
Tactic:
clear h₆
Proof state after:
z : ℂ
⊢ I ^ (2 + 1) = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ I ^ (2 + 1) = -I
Tactic:
rw [zpow_add₀ I_ne_zero]
Proof state after:
z : ℂ
⊢ I ^ 2 * I ^ 1 = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ I ^ 2 * I ^ 1 = -I
Tactic:
have h₇ : (2 : ℤ) = 1 + 1 := by
  exact rfl
Proof state after:
z : ℂ
h₇ : 2 = 1 + 1
⊢ I ^ 2 * I ^ 1 = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₇ : 2 = 1 + 1
⊢ I ^ 2 * I ^ 1 = -I
Tactic:
rw [h₇]
Proof state after:
z : ℂ
h₇ : 2 = 1 + 1
⊢ I ^ (1 + 1) * I ^ 1 = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₇ : 2 = 1 + 1
⊢ I ^ (1 + 1) * I ^ 1 = -I
Tactic:
clear h₇
Proof state after:
z : ℂ
⊢ I ^ (1 + 1) * I ^ 1 = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ I ^ (1 + 1) * I ^ 1 = -I
Tactic:
rw [zpow_add₀ I_ne_zero]
Proof state after:
z : ℂ
⊢ I ^ 1 * I ^ 1 * I ^ 1 = -I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ I ^ 1 * I ^ 1 * I ^ 1 = -I
Tactic:
simp only [zpow_one, I_mul_I, neg_mul, one_mul]
Proof state after:
no goals
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
h₁b : cexp (↑π * I * 3 / 2) = I ^ 3
⊢ ↑π * I * 3 / 2 = ↑π * I * (3 / 2)
Tactic:
ring
Proof state after:
no goals
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ I ^ 3 = I ^ 3
Tactic:
exact rfl
Proof state after:
no goals
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ 3 = 2 + 1
Tactic:
exact rfl
Proof state after:
no goals
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ 2 = 1 + 1
Tactic:
exact rfl
Proof state after:
no goals
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ cexp (↑π * I * 2⁻¹) = I
Tactic:
nth_rw 2 [←ExpPiMulIHalf]
Proof state after:
z : ℂ
⊢ cexp (↑π * I * 2⁻¹) = cexp (↑(π / 2) * I)
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ cexp (↑π * I * 2⁻¹) = cexp (↑(π / 2) * I)
Tactic:
congr 1
Proof state after:
case e_z
z : ℂ
⊢ ↑π * I * 2⁻¹ = ↑(π / 2) * I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
case e_z
z : ℂ
⊢ ↑π * I * 2⁻¹ = ↑(π / 2) * I
Tactic:
simp only [ofReal_div, ofReal_ofNat]
Proof state after:
case e_z
z : ℂ
⊢ ↑π * I * 2⁻¹ = ↑π / 2 * I
Theorem: RuesN4EqualsCoshCosh
Proof state before:
case e_z
z : ℂ
⊢ ↑π * I * 2⁻¹ = ↑π / 2 * I
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ (1 + I)⁻¹ = (1 - I) / 2
Tactic:
rw [Inv.inv, Complex.instInv, normSq]
Proof state after:
z : ℂ
⊢ {
          inv := fun z =>
            (starRingEnd ℂ) z *
              ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
                      map_mul' := normSq.proof_3 }
                    z)⁻¹ }.1
      (1 + I) =
    (1 - I) / 2
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ {
          inv := fun z =>
            (starRingEnd ℂ) z *
              ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
                      map_mul' := normSq.proof_3 }
                    z)⁻¹ }.1
      (1 + I) =
    (1 - I) / 2
Tactic:
simp only [MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, ofReal_inv, ofReal_add, ofReal_mul,
  map_add, map_one, conj_I, add_re, one_re, I_re, add_zero, ofReal_one, mul_one, add_im, one_im,
  I_im, zero_add]
Proof state after:
z : ℂ
⊢ (1 + -I) * (1 + 1)⁻¹ = (1 - I) / 2
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ (1 + -I) * (1 + 1)⁻¹ = (1 - I) / 2
Tactic:
ring_nf
Proof state after:
no goals
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ (1 - I)⁻¹ = (1 + I) / 2
Tactic:
rw [Inv.inv, Complex.instInv, normSq]
Proof state after:
z : ℂ
⊢ {
          inv := fun z =>
            (starRingEnd ℂ) z *
              ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
                      map_mul' := normSq.proof_3 }
                    z)⁻¹ }.1
      (1 - I) =
    (1 + I) / 2
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ {
          inv := fun z =>
            (starRingEnd ℂ) z *
              ↑({ toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1, map_one' := normSq.proof_2,
                      map_mul' := normSq.proof_3 }
                    z)⁻¹ }.1
      (1 - I) =
    (1 + I) / 2
Tactic:
simp only [MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, ofReal_inv, ofReal_add, ofReal_mul,
  map_sub, map_one, conj_I, sub_neg_eq_add, sub_re, one_re, I_re, sub_zero, ofReal_one, mul_one,
  sub_im, one_im, I_im, zero_sub, ofReal_neg, mul_neg, neg_neg]
Proof state after:
z : ℂ
⊢ (1 + I) * (1 + 1)⁻¹ = (1 + I) / 2
Theorem: RuesN4EqualsCoshCosh
Proof state before:
z : ℂ
⊢ (1 + I) * (1 + 1)⁻¹ = (1 + I) / 2
Tactic:
ring_nf
Proof state after:
no goals
Theorem: ExpSumOfRuesDiff
Proof state before:
k : ℕ+
z : ℂ
⊢ cexp z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Tactic:
rw [←RuesN1EqualsExp, ←RuesDiffM0EqualsRues]
Proof state after:
k : ℕ+
z : ℂ
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Theorem: ExpSumOfRuesDiff
Proof state before:
k : ℕ+
z : ℂ
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Tactic:
have h₀ := RuesDiffSumOfRuesDiff 1 k 0 z
Proof state after:
k : ℕ+
z : ℂ
h₀ : RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff (1 * k) (↑↑1 * ↑k₀ + 0) z
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Theorem: ExpSumOfRuesDiff
Proof state before:
k : ℕ+
z : ℂ
h₀ : RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff (1 * k) (↑↑1 * ↑k₀ + 0) z
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Tactic:
simp only [one_mul, PNat.val_ofNat, Nat.cast_one, add_zero] at h₀
Proof state after:
k : ℕ+
z : ℂ
h₀ : RuesDiff 1 0 z = ∑ x ∈ range ↑k, RuesDiff k (↑x) z
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Theorem: ExpSumOfRuesDiff
Proof state before:
k : ℕ+
z : ℂ
h₀ : RuesDiff 1 0 z = ∑ x ∈ range ↑k, RuesDiff k (↑x) z
⊢ RuesDiff 1 0 z = ∑ k₀ ∈ range ↑k, RuesDiff k (↑k₀) z
Tactic:
assumption
Proof state after:
no goals
Theorem: RouForm
Proof state before:
n : ℕ+
x : ℕ
⊢ cexp (2 * ↑π * (↑x / ↑↑n) * I) ^ ↑n = 1
Tactic:
rw [(Complex.exp_nat_mul _ n).symm, Complex.exp_eq_one_iff]
Proof state after:
n : ℕ+
x : ℕ
⊢ ∃ n_1, ↑↑n * (2 * ↑π * (↑x / ↑↑n) * I) = ↑n_1 * (2 * ↑π * I)
Theorem: RouForm
Proof state before:
n : ℕ+
x : ℕ
⊢ ∃ n_1, ↑↑n * (2 * ↑π * (↑x / ↑↑n) * I) = ↑n_1 * (2 * ↑π * I)
Tactic:
use x
Proof state after:
case h
n : ℕ+
x : ℕ
⊢ ↑↑n * (2 * ↑π * (↑x / ↑↑n) * I) = ↑↑x * (2 * ↑π * I)
Theorem: RouForm
Proof state before:
case h
n : ℕ+
x : ℕ
⊢ ↑↑n * (2 * ↑π * (↑x / ↑↑n) * I) = ↑↑x * (2 * ↑π * I)
Tactic:
field_simp
Proof state after:
case h
n : ℕ+
x : ℕ
⊢ 2 * ↑π * ↑x * I = ↑x * (2 * ↑π * I)
Theorem: RouForm
Proof state before:
case h
n : ℕ+
x : ℕ
⊢ 2 * ↑π * ↑x * I = ↑x * (2 * ↑π * I)
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Sum3Cycle
Proof state before:
M : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommMonoid M
s : Finset α
t : Finset β
u : Finset γ
f : α → β → γ → M
⊢ ∑ a ∈ s, ∑ b ∈ t, ∑ c ∈ u, f a b c = ∑ b ∈ t, ∑ c ∈ u, ∑ a ∈ s, f a b c
Tactic:
rw [sum_comm]
Proof state after:
M : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommMonoid M
s : Finset α
t : Finset β
u : Finset γ
f : α → β → γ → M
⊢ ∑ y ∈ t, ∑ x ∈ s, ∑ c ∈ u, f x y c = ∑ b ∈ t, ∑ c ∈ u, ∑ a ∈ s, f a b c
Theorem: Sum3Cycle
Proof state before:
M : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommMonoid M
s : Finset α
t : Finset β
u : Finset γ
f : α → β → γ → M
⊢ ∑ y ∈ t, ∑ x ∈ s, ∑ c ∈ u, f x y c = ∑ b ∈ t, ∑ c ∈ u, ∑ a ∈ s, f a b c
Tactic:
simp_rw [@sum_comm _ _ γ]
Proof state after:
no goals
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ RuesDiff n m (z₀ + z₁) = ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
rw [RuesDiffEqualsExpSum]
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ k₀ ∈ range ↑n, cexp ((z₀ + z₁) * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑m * 2 * ↑π * (↑k₀ / ↑↑n) * I)) / ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ k₀ ∈ range ↑n, cexp ((z₀ + z₁) * cexp (2 * ↑π * (↑k₀ / ↑↑n) * I) + ↑m * 2 * ↑π * (↑k₀ / ↑↑n) * I)) / ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp_rw [Complex.exp_add, RightDistribClass.right_distrib, Complex.exp_add, ExpSumOfRuesDiff n (z₀ * _), ExpSumOfRuesDiff n (z₁ * _)]
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ((∑ k₀ ∈ range ↑n, RuesDiff n (↑k₀) (z₀ * cexp (2 * ↑π * (↑x / ↑↑n) * I))) *
            ∑ k₀ ∈ range ↑n, RuesDiff n (↑k₀) (z₁ * cexp (2 * ↑π * (↑x / ↑↑n) * I))) *
          cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ((∑ k₀ ∈ range ↑n, RuesDiff n (↑k₀) (z₀ * cexp (2 * ↑π * (↑x / ↑↑n) * I))) *
            ∑ k₀ ∈ range ↑n, RuesDiff n (↑k₀) (z₁ * cexp (2 * ↑π * (↑x / ↑↑n) * I))) *
          cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp_rw [RuesDiffRotationallySymmetric n _ _ _ (RouForm n _), Finset.sum_mul, Finset.mul_sum, Finset.sum_mul, ←Complex.exp_int_mul]
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          ∑ x_2 ∈ range ↑n,
            cexp (↑(-↑x_1) * (2 * ↑π * (↑x / ↑↑n) * I)) * RuesDiff n (↑x_1) z₀ *
                (cexp (↑(-↑x_2) * (2 * ↑π * (↑x / ↑↑n) * I)) * RuesDiff n (↑x_2) z₁) *
              cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          ∑ x_2 ∈ range ↑n,
            cexp (↑(-↑x_1) * (2 * ↑π * (↑x / ↑↑n) * I)) * RuesDiff n (↑x_1) z₀ *
                (cexp (↑(-↑x_2) * (2 * ↑π * (↑x / ↑↑n) * I)) * RuesDiff n (↑x_2) z₁) *
              cexp (↑m * 2 * ↑π * (↑x / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
rw [Sum3Cycle]
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ b ∈ range ↑n,
        ∑ c ∈ range ↑n,
          ∑ a ∈ range ↑n,
            cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
                (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
              cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ b ∈ range ↑n,
        ∑ c ∈ range ↑n,
          ∑ a ∈ range ↑n,
            cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
                (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
              cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
have h₀ : ∀ (a b c : ℕ), cexp (↑(-(b : ℤ)) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ * (cexp (↑(-(c : ℤ)) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) * cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
    RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ * (cexp (↑(-(b : ℤ)) * (2 * ↑π * (↑a / ↑↑n) * I)) * (cexp (↑(-(c : ℤ)) * (2 * ↑π * (↑a / ↑↑n) * I))) * cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I)) := by
  intros a b c
  ring_nf
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₀ :
  ∀ (a b c : ℕ),
    cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
          (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
      RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
        (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
          cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
⊢ (∑ b ∈ range ↑n,
        ∑ c ∈ range ↑n,
          ∑ a ∈ range ↑n,
            cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
                (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
              cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₀ :
  ∀ (a b c : ℕ),
    cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
          (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
      RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
        (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
          cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
⊢ (∑ b ∈ range ↑n,
        ∑ c ∈ range ↑n,
          ∑ a ∈ range ↑n,
            cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
                (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
              cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp_rw [h₀, ←Complex.exp_add, ←Finset.mul_sum]
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₀ :
  ∀ (a b c : ℕ),
    cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
          (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
      RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
        (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
          cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ i ∈ range ↑n,
              cexp
                (↑(-↑x) * (2 * ↑π * (↑i / ↑↑n) * I) + ↑(-↑x_1) * (2 * ↑π * (↑i / ↑↑n) * I) +
                  ↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₀ :
  ∀ (a b c : ℕ),
    cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑b) z₀ *
          (cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) * RuesDiff n (↑c) z₁) *
        cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I) =
      RuesDiff n (↑b) z₀ * RuesDiff n (↑c) z₁ *
        (cexp (↑(-↑b) * (2 * ↑π * (↑a / ↑↑n) * I)) * cexp (↑(-↑c) * (2 * ↑π * (↑a / ↑↑n) * I)) *
          cexp (↑m * 2 * ↑π * (↑a / ↑↑n) * I))
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ i ∈ range ↑n,
              cexp
                (↑(-↑x) * (2 * ↑π * (↑i / ↑↑n) * I) + ↑(-↑x_1) * (2 * ↑π * (↑i / ↑↑n) * I) +
                  ↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
clear h₀
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ i ∈ range ↑n,
              cexp
                (↑(-↑x) * (2 * ↑π * (↑i / ↑↑n) * I) + ↑(-↑x_1) * (2 * ↑π * (↑i / ↑↑n) * I) +
                  ↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ i ∈ range ↑n,
              cexp
                (↑(-↑x) * (2 * ↑π * (↑i / ↑↑n) * I) + ↑(-↑x_1) * (2 * ↑π * (↑i / ↑↑n) * I) +
                  ↑m * 2 * ↑π * (↑i / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp only [Int.cast_neg, Int.cast_natCast, neg_mul]
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n,
              cexp
                (-(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) +
                  ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n,
              cexp
                (-(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) +
                  ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
have h₁ : ∀ (x x_1 x_2 : ℕ), -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
    (2 * ↑π * (((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n) * I)) := by
  intros x x_1 x_2
  ring_nf
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₁ :
  ∀ (x x_1 x_2 : ℕ),
    -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
      2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n,
              cexp
                (-(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) +
                  ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₁ :
  ∀ (x x_1 x_2 : ℕ),
    -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
      2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n,
              cexp
                (-(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) +
                  ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I)) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp_rw [h₁]
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₁ :
  ∀ (x x_1 x_2 : ℕ),
    -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
      2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₁ :
  ∀ (x x_1 x_2 : ℕ),
    -(↑x * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + -(↑x_1 * (2 * ↑π * (↑x_2 / ↑↑n) * I)) + ↑m * 2 * ↑π * (↑x_2 / ↑↑n) * I =
      2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
clear h₁
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
have h₂ : ∀ (x x_1 : ℕ), (m : ℂ) - (x : ℂ) - (x_1 : ℂ) = @Int.cast ℂ Ring.toIntCast (m - (x : ℤ) - (x_1 : ℤ)) := by
  intros x x_1
  norm_cast
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₂ : ∀ (x x_1 : ℕ), ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₂ : ∀ (x x_1 : ℕ), ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n,
          RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ *
            ∑ x_2 ∈ range ↑n, cexp (2 * ↑π * ((↑m - ↑x - ↑x_1) * ↑x_2 / ↑↑n * I))) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
simp_rw [h₂, RouGeometricSumEqIte]
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₂ : ∀ (x x_1 : ℕ), ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n, RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ * if ↑↑n ∣ m - ↑x - ↑x_1 then ↑↑n else 0) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Theorem: RuesDiffArgumentSumRule
Proof state before:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
h₂ : ∀ (x x_1 : ℕ), ↑m - ↑x - ↑x_1 = ↑(m - ↑x - ↑x_1)
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n, RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ * if ↑↑n ∣ m - ↑x - ↑x_1 then ↑↑n else 0) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁
Tactic:
clear h₂
Proof state after:
n : ℕ+
m : ℤ
z₀ z₁ : ℂ
⊢ (∑ x ∈ range ↑n,
        ∑ x_1 ∈ range ↑n, RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ * if ↑↑n ∣ m - ↑x - ↑x_1 then ↑↑n else 0) /
      ↑↑n =
    ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁