How to resolve sorry in a Lean proof involving complex expon

Stream: new members

[Yiran Wang]

Hi all,

I'm trying to prove the following lemmas about roots of unity defined via zeta r := exp(2πi / r) in Lean. The first lemma is for the case r ∣ s, and the second for r ∤ s. I've completed most of the proof, but I'm stuck on the final step involving complex division and contradiction with the divisibility assumption.

import Mathlib

open Complex BigOperators Nat Finset Set

noncomputable def zeta (r : ℕ) : ℂ := exp (2 * Real.pi * I / r)

lemma zeta_one(r s k : ℕ)(h₁ : r ∣ s)(h:r>0):zeta r ^ (s * k) = 1:= by
  rcases h₁ with ⟨m, hm⟩
  have h₂:zeta r ^ (s * k)= exp (2 * Real.pi * I / r)^(s*k):= by
    exact rfl
  rw [h₂]
  have h₃:exp (2 * Real.pi * I / r)^(s*k) = exp (s*k*(2 * Real.pi * I / r)):=by
    rw [← exp_nat_mul]
    rw [cast_mul]
  rw [h₃]
  have h₄:exp (s*k*(2 * Real.pi * I / r))=exp (s*k/r*(2 * Real.pi * I)):=by
    simp [← mul_assoc, ← mul_div_assoc]
    simp [mul_div_right_comm]
  rw [h₄]
  have h₆:exp (s*k/r*(2 * Real.pi * I)) = 1 := by
    have l₁₁ : (s * k) % r = 0 := by
      rw [hm]
      have b₁:r * m * k = (m * k) * r := by
        exact mul_rotate r m k
      rw [b₁]
      rw [mul_mod_left]
    rw [exp_eq_one_iff]
    have l₂: ∃n :ℤ, ↑s * ↑k / ↑r * (2 * ↑Real.pi * I) = ↑n * (2 * ↑Real.pi * I):= by
      use (m * k)
      simp
      have l₃: (↑s:ℂ) * (↑k:ℂ) / (↑r:ℂ) = (↑m:ℂ) * (↑k:ℂ) ∨ Real.pi = 0 := by
        have l₄:(↑s:ℂ) * (↑k:ℂ) / (↑r:ℂ) = (↑m:ℂ) * (↑k:ℂ):= by
          simp [hm]
          have l₇: (↑r:ℂ) * (↑m:ℂ) * (↑k:ℂ) / (↑r:ℂ) = (↑m:ℂ) * (↑k:ℂ):= by
            simp [Nat.cast_mul, Nat.cast_div, mul_comm,← mul_assoc]
            rw [mul_rotate]
            have l₈: (↑k:ℂ) *  (↑m:ℂ) * (↑r:ℂ) / (↑r:ℂ) =  (↑k:ℂ) *  (↑m:ℂ) * ((↑r:ℂ) / (↑r:ℂ)):=by
              simp [mul_div_assoc']
            rw [l₈]
            have l₉: (↑k:ℂ) *  (↑m:ℂ) * ((↑r:ℂ) / (↑r:ℂ))= (↑k:ℂ) *  (↑m:ℂ) * (1:ℂ):= by
              have h₉:(↑r:ℂ) / (↑r:ℂ) = (1:ℂ):= by
                norm_cast
                rw [div_self]
                have h₇:(↑r:ℂ)≠ 0:= by
                  norm_cast
                  exact not_eq_zero_of_lt h
                exact h₇
              rw [h₉]
            rw [l₉]
            ring
          exact l₇
        rw [l₄]
        have l₅:(↑m:ℂ) * (↑k:ℂ) = (↑m:ℂ) * (↑k:ℂ) ∨ Real.pi = 0:= by
          exact Or.symm (Or.inr rfl)
        exact l₅
      exact l₃
    exact l₂
  rw [h₆]

lemma zeta_not_one(r s k : ℕ)(h₁ : ¬r∣s)(h:r>0):zeta r ^ s ≠ 1:= by
  have l₁:zeta r ^ s = exp (2 * Real.pi * I / r)^s:= by rw [zeta]
  rw [l₁]
  rw [← exp_nat_mul]
  simp
  have l₂:exp (↑s * (2 * ↑Real.pi * I / ↑r)) = exp (↑s * 2 * ↑Real.pi * I / ↑r):=by
    ring_nf
  rw [l₂]
  have l₃:exp (↑s * 2 * ↑Real.pi * I / ↑r) = exp (↑s / ↑r * 2 * ↑Real.pi * I):= by
    ring_nf
  rw [l₃]
  rw [exp_eq_one_iff]
  have l₄:↑s / ↑r * 2 * ↑Real.pi * I =↑s / ↑r * (2 * ↑Real.pi * I):= by
    ring
  rw [l₄]
  have l₅:¬∃ n:ℤ, ↑s / ↑r * (2 * ↑Real.pi * I) = ↑n * (2 * ↑Real.pi * I) := by
    sorry
  exact l₅

[Ruben Van de Velde]

  have l₅:¬∃ n:ℤ, ↑s / ↑r * (2 * ↑Real.pi * I) = ↑n * (2 * ↑Real.pi * I) := by
    rintro ⟨n, hn⟩ -- Assume such an n exists
    simp [Real.pi_ne_zero] at hn -- cancel out the 2πI
    rw [div_eq_iff] at hn -- bring the denominator to the other side
    norm_cast at hn -- move to ℤ
    apply h₁ -- we will find a contradiction with the divisibility
    rw [← Int.ofNat_dvd] -- the divisibility is about ℕ, move to ℤ
    use n -- `n` is the divisor
    rw [hn, mul_comm] -- arithmetic